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

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

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.