Collaborative Research: FMitF: Track II: Enhancing the Neural Network Verification (NNV) Tool for Industrial Applications

包含机器学习组件的系统的安全性和可靠性是重大挑战。新技术对于在部署这些数据驱动的机器学习组件之前进行严格的分析至关重要，这些组件用于从传感和感知到安全关键领域（如航空航天和汽车系统）的规划和控制等任务。该项目增强了用于深度神经网络和支持学习的自主系统的神经网络验证（NNV）软件工具，通过与航空航天、汽车和设计自动化领域的行业合作伙伴的合作，实现工业应用。该项目的新奇在于为处理时间序列数据的神经网络开发了新的验证技术，以及指定时间行为的新方法。该项目的影响是开发和应用严格的分析方法，以及帮助将这些方法过渡到工业，最终可能用于现实世界的学习系统的工程保证和认证过程。该项目将开发新的神经网络验证方法，用于时间序列数据和架构，然后在NNV软件工具中实现这些方法，并根据具有挑战性的基准和行业案例研究对其进行评估。新的时间序列分析技术结合联合收割机放松星星可达性方法与反例引导的抽象细化（CEGAR）方法，以提高验证的可扩展性，同时保持精度。这些时间序列问题的基于迹的属性将在形式化中指定，例如度量时态逻辑（MTL）和信号时态逻辑（STL），以及这些逻辑的扩展。NNV还将在可用性和文档方面进行改进，并对这些改进进行评估，部分原因是继续在研究人员教授的课程中使用它，以及与行业合作伙伴合作。与行业合作伙伴一起开发的工业规模基准和案例研究将通过神经网络验证竞赛等活动加强更广泛的形式方法和机器学习研究社区的参与（VNN-COMP）和混合系统验证人工智能和神经网络控制系统（AINNCS）该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The safety and reliability of systems incorporating machine-learning components are significant challenges. New techniques are crucial to enable rigorous analysis before deploying these data-driven machine-learning components for tasks ranging from sensing and perception to planning and control in safety-critical domains, such as aerospace and automotive systems. This project enhances the Neural Network Verification (NNV) software tool for deep neural networks and learning-enabled autonomous systems to enable industrial usage through engagement with industry partners in aerospace, automotive, and design automation. The project's novelty is the development of new verification techniques for neural networks that process time-series data and new ways to specify temporal behaviors. The project's impact is developing and applying rigorous analysis methods, as well as helping transition these methods to industry, which may eventually be used in the engineering-assurance and certification processes of real-world learning-enabled systems.This project will develop new neural-network verification methods for time-series data and architectures, then implement these in the NNV software tool, and evaluate them on challenging benchmarks and case studies from industry. The new time-series analysis techniques combine the relaxed star reachability approach with counterexample-guided abstraction refinement (CEGAR) methods to improve verification scalability while maintaining precision. Trace-based properties for these time-series problems will be specified in formalisms such as metric temporal logic (MTL) and signal temporal logic (STL), as well as extensions of these logics. NNV will also be improved for usability and documentation, as well as evaluated for these improvements, in part by continuing to use it within courses taught by the researchers, as well as collaborating with industry partners. Industrial-scale benchmarks and case studies developed with industry partners will strengthen engagement of the broader formal-methods and machine-learning research communities through events such as the Neural Network Verification Competition (VNN-COMP) and the Hybrid Systems Verification (ARCH-COMP) category on Artificial Intelligence and Neural Network Control Systems (AINNCS).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.