FMitF: Track I: Scalable and Quantitative Verification for Neural Network Analysis and Design

神经网络在计算机视觉、语音识别和自然语言处理等许多领域都取得了成功。然而，由于神经网络越来越多地应用于安全关键和社会敏感领域，如自动驾驶汽车、机器人、计算机安全、刑事司法和医疗诊断，迫切需要开发能够保证神经网络应用可靠性和安全性的验证技术。形式验证技术可以保证正确性；然而，现有的方法在分析现实世界中具有大量神经元和复杂模型结构的神经网络时并不有效。该项目设定了一个全面的研究议程，重点关注神经网络的整体形式验证框架，该框架将为开发可靠和安全的神经网络提供系统和原则性的方法。它旨在使自动驾驶等主要机器学习应用受益，并为美国在软件工程和人工智能方面的领导地位做出贡献。研究结果通过开源软件包、主要会议和期刊的出版物、教学研讨会的教程以及专门的K-12课程广泛传播，使年轻一代接触到软件验证和机器学习研究的前沿。在这个项目上工作的研究团队正在整合经典计算领域的方法，如软件工程、自动验证和形式化方法，以解决神经网络应用的可靠性和安全性方面的独特研究挑战。具体研究方向包括：1)新颖的符号定量分析技术，为建立最先进的神经网络模型的可靠性和安全性提供可靠的结果；2)一组有效的系统级优化，用于计算/内存高效的神经网络验证，具有足够的跨框架可移植性和高验证效率；3)先进的神经架构设计和训练支持，用于探索和开发具有可验证鲁棒性的神经网络模型。该研究议程的成功旨在为提高神经网络验证技术的可扩展性和神经网络应用的鲁棒性提供更完整、更有效的软件堆栈。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Neural Networks (NNs) have been successful in many areas including computer vision, speech recognition, and natural language processing. However, due to the increasing adoption of NNs in safety-critical and socially sensitive domains such as self-driving cars, robotics, computer security, criminal justice, and medical diagnosis, there is a pressing need for developing verification techniques that can provide guarantees about dependability and safety of NN applications. Formal-verification techniques can provide guarantees of correctness; however, existing approaches are not effective in analyzing real-world NNs with large numbers of neurons and complicated model structures. This project sets a comprehensive research agenda focusing on a holistic formal-verification framework for NNs that will provide a systematic and principled approach for developing dependable and safe NNs. It is intended to benefit major machine-learning applications such as autonomous driving and contribute to the leadership of the United States in software engineering and artificial intelligence. The research findings are being widely disseminated through open-source software packages, publications in premier conferences and journals, tutorials at teaching workshops, as well as specialized K-12 programs for exposing the young generation to the frontiers of software verification and machine-learning research. The team of researchers working on this project are integrating methods from the classical computing fields such as software engineering, automated verification, and formal methods to address the unique research challenges in the dependability and safety of NN applications. Specific research directions include 1) novel symbolic quantitative analysis techniques that provide sound results for establishing dependability and safety of the state-of-the-art NN models; 2) a set of effective system-level optimizations for computation/memory efficient NN verification with sufficient cross-framework portability and high verification efficiency; 3) advanced neural architecture design and training support for exploring and developing neural network models with verifiable robustness. The success of this research agenda is intended to enable a more complete and efficient software stack for improving the scalability of NN verification techniques and the robustness of NN applications.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.