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

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