SHF: Small: Scalable Formal Verification of ANN controlled Cyber-Physical Systems

人工神经网络（ANN）越来越多地被用于监测和控制信息物理系统（CPS），如自主地面和飞行器。随着这些系统的复杂性和安全关键性的增加，形式验证技术，提供严格的保证是迫切需要的。研究的主要目标是开发新的算法和软件工具，用于人工神经网络控制的CPS（ANN-CPS）的形式化验证。现有技术的主要挑战之一是它们对大量神经元和复杂物理动力学的可扩展性。使用区间神经网络的新概念，再加上形式化方法的想法，如反例指导的抽象细化和近似互模拟，该项目研究了ANN-CPS的可扩展形式验证技术。该项目的结果将使复杂的ANN-CPS的严格分析成为可能，从而提高其在自动驾驶等应用中的可靠性。此外，PI还参与课程开发、本科生和研究生的指导以及K-12学生的推广活动，其更广泛的目标是激励和建立网络物理系统正式分析的劳动力。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

Artificial Neural Networks (ANN) are increasingly being employed to monitor and control Cyber-Physical Systems (CPS), as in autonomous ground and aerial vehicles. With increasing complexity and safety criticality of these systems, formal-verification techniques that provide rigorous guarantees are urgently needed. The broad goal of the research is to develop novel algorithms and software tools for formal verification of ANN-controlled CPS (ANN-CPS). One of the main challenges of existing techniques is their scalability to large number of neurons and complex physical dynamics. Using the novel concept of Interval Neural Networks, coupled with ideas from formal methods such as counter-example guided abstraction refinement and approximate bisimulation, the project investigates scalable formal verification techniques for ANN-CPS. The results of the project will enable rigorous analysis of complex ANN-CPS possible, thereby enhancing their reliability in applications such as autonomous driving. Further, the PI is engaged in course development, mentorship of undergraduate and graduate students, and outreach activities for K-12 students, with the broader aim of motivating and building the workforce for formal analysis of cyber-physical systems.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.