NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems

This paper presents the Neural Network Verification (NNV) software tool, a\nset-based verification framework for deep neural networks (DNNs) and\nlearning-enabled cyber-physical systems (CPS). The crux of NNV is a collection\nof reachability algorithms that make use of a variety of set representations,\nsuch as polyhedra, star sets, zonotopes, and abstract-domain representations.\nNNV supports both exact (sound and complete) and over-approximate (sound)\nreachability algorithms for verifying safety and robustness properties of\nfeed-forward neural networks (FFNNs) with various activation functions. For\nlearning-enabled CPS, such as closed-loop control systems incorporating neural\nnetworks, NNV provides exact and over-approximate reachability analysis schemes\nfor linear plant models and FFNN controllers with piecewise-linear activation\nfunctions, such as ReLUs. For similar neural network control systems (NNCS)\nthat instead have nonlinear plant models, NNV supports over-approximate\nanalysis by combining the star set analysis used for FFNN controllers with\nzonotope-based analysis for nonlinear plant dynamics building on CORA. We\nevaluate NNV using two real-world case studies: the first is safety\nverification of ACAS Xu networks and the second deals with the safety\nverification of a deep learning-based adaptive cruise control system.\n