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

Vanderbilt University, Nashville TN

Investigators

Abstract

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.