Source-linked AI summary
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson
TL;DR
Safety and robustness verification is difficult for DNNs and learning-enabled CPS because nonlinear behavior and adversarial input perturbations complicate analysis. NNV addresses this with set-based exact and over-approximate reachability across multiple representations, and evaluates the framework on ACAS Xu and adaptive cruise control. The case studies demonstrate its application to real-world verification, while the paper also identifies limits from plant-model mismatch and deferred ImageStar evaluation.
Problem
Safety and robustness assurance for DNNs in safety-critical CPS remains difficult because DNNs have complex nonlinear behavior and can respond unpredictably to slight input perturbations.
Method
NNV combines exact and over-approximate set-based reachability algorithms with polyhedra, star sets, zonotopes, and abstract-domain representations for DNNs and learning-enabled CPS.
Results
NNV is applied to safety verification of ACAS Xu networks and a learning-based adaptive cruise control system, with exact and over-approximate analyses supported for relevant models.
Takeaways & Limitations
NNV provides a toolbox for verifying safety and robustness of real-world DNNs and learning-enabled CPS, including counterexample construction and over-approximate safety analysis.
Takeaways & Limitations
For nonlinear plants, simulation-trained neural-network controllers may lose safety performance under plant-model mismatch between the simulation and real system.
Abstract
from arXiv · showhide
This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collection of reachability algorithms that make use of a variety of set representations, such as polyhedra, star sets, zonotopes, and abstract-domain representations. NNV supports both exact (sound and complete) and over-approximate (sound) reachability algorithms for verifying safety and robustness properties of feed-forward neural networks (FFNNs) with various activation functions. For learning-enabled CPS, such as closed-loop control systems incorporating neural networks, NNV provides exact and over-approximate reachability analysis schemes for linear plant models and FFNN controllers with piecewise-linear activation functions, such as ReLUs. For similar neural network control systems (NNCS) that instead have nonlinear plant models, NNV supports over-approximate analysis by combining the star set analysis used for FFNN controllers with zonotope-based analysis for nonlinear plant dynamics building on CORA. We evaluate NNV using two real-world case studies: the first is safety verification of ACAS Xu networks and the second deals with the safety verification of a deep learning-based adaptive cruise control system.
1 Introduction
NNV is a set-based software framework for verifying DNNs and learning-enabled CPS despite nonlinear behavior and input sensitivity. It combines reachability algorithms and multiple set representations, with case studies demonstrating applications to ACAS Xu and adaptive cruise control.
- Motivation: DNNs improve performance in safety-critical applications but are difficult to verify because of complex nonlinear characteristics and sensitivity to small input perturbations.Such perturbations are described as adversarial perturbations.
- Framework: NNV performs set-based verification of DNNs and neural network control systems using exact and over-approximate reachable-set algorithms.It supports polyhedra, star sets, zonotopes, and abstract-domain representations.
- Framework: NNV declares a system safe when its reachable set does not intersect states satisfying the negation of the safety property.For violations, its exact star-based analysis can construct a complete set of unsafe initial inputs and states.
- Evaluation: NNV is evaluated through safety verification case studies involving ACAS Xu networks and a learning-based adaptive cruise control system.The ACAS Xu study compares verification methods, while the ACC study verifies a learning-based control system.
- Implementation: The toolbox is a Matlab object-oriented implementation using MPT for polytope analysis, CORA for nonlinear-plant zonotopes, NNMT for model transformation, and HyST for plant configuration.Matlab was chosen partly because of Matlab/Simulink’s prevalence in CPS design.
- Architecture: NNV’s computation engine includes FFNN and NNCS constructors, reachability solvers, and an evaluator, alongside an analyzer module.The NNCS constructor combines an FFNN object with a plant configuration describing system dynamics.
3 Set Representations and Reachability Algorithms
NNV supports layered reachability analysis using several set representations, balancing exactness, scalability, and conservativeness across FFNNs and CNNs. Its enhanced star algorithms preserve plant–controller relationships, while ImageStar extends analysis to deep CNNs.
- Sequential network analysis: NNV computes reachable sets layer-by-layer, passing each layer’s output reachable set as the input set for the next layer.This applies to sequential FFNNs and CNNs, as well as NNCSs with FFNN controllers.
- Polyhedra: The polyhedron method computes exact reachable sets for ReLU FFNNs by applying affine mappings followed by successive stepReLU operations.A stepReLU operation can split one polyhedron into two polyhedra.
- Star sets: Star sets make affine mapping and half-space intersection easier than polyhedra, enabling faster and more scalable exact reachability while supporting over-approximation for nonlinear activations.NNV enhances these algorithms by reducing the number of LP optimization problems.
- Star sets: For NNCSs with linear plants, enhanced star analysis preserves relationships between plant states and control inputs through shared predicate variables, avoiding conservativeness explosion in the polyhedron method.The extension also minimizes LP computations by estimating state ranges from predicate-variable ranges.
- Over-approximate methods: Zonotope and abstract-domain methods provide over-approximations, but are more conservative than star sets despite zonotopes being fast and scalable.The abstract-domain method represents the abstract domain as a star set and uses back-tracking to estimate state ranges.
- ImageStar: ImageStar generalizes star sets by replacing anchor and generator vectors with multi-channel images for efficient reachability analysis of deep CNN layers.NNV supports exact and over-approximate ImageStar analysis for serial CNNs, including robustness analysis of VGG16 and VGG19 networks with more than 100 million parameters.
4 Evaluation
NNV is evaluated on ACAS Xu safety verification and learning-based ACC safety verification across linear and nonlinear plant models. The results show strong speed and conservativeness advantages for approximate star analysis, while ACC safety depends on initial conditions and plant-model fidelity.
- ACAS Xu safety verification: NNV evaluates ACAS Xu safety properties φ3 and φ4 across all 45 networks against Reluplex, Marabou, and ReluVal.The experiments use four computation cores, and verification outcomes are labeled SAT, UNSAT, or UNK.
- ACAS Xu safety verification: Approximate star analysis is substantially faster than competing ACAS Xu methods, including 547× over Reluplex and 2151× over Marabou-DnC for φ3.For φ4, it is 625× faster than Reluplex, 445× faster than Marabou, and 1321× faster than Marabou-DnC.
- ACAS Xu safety verification: For φ3, approximate star analysis proves 29/45 networks safe (64.4%), versus 2/45 (4.44%) for zonotopes and 19/45 (42.22%) for abstract domains.The higher coverage is attributed to a tighter over-approximate reachable set.
- ACAS Xu safety verification: For φ4, approximate star analysis proves 32/45 networks safe (71.11%), versus 1/45 (2.22%) for zonotopes and 0/45 (0.00%) for abstract domains.These results are presented as evidence that approximate star analysis is less conservative than the compared methods.
- Adaptive cruise control: For ACC, NNV analyzes both discrete linear and nonlinear continuous plant dynamics, using exact and over-approximate reachability for the linear model and over-approximation for the nonlinear model.The ACC controller has five layers, 20 neurons per layer, ReLU activations, and a 0.1-second control period.
- Adaptive cruise control: ACC safety depends on the lead vehicle’s initial velocity: the discrete plant is unsafe below 27 m/s, while the nonlinear-model verification results are all UNSAFE.The nonlinear model adds a small friction term to the linear model, and the controller was trained using the linear model.
- Adaptive cruise control: The ACC scenarios illustrate both guaranteed safety, with Drel ≥ Dsafe, and safety violation, with Drel < Dsafe during some control steps.The safe scenario uses vlead(0) ∈ [29, 30] m/s, while the violating scenario uses vlead(0) ∈ [24, 25] m/s.
- Adaptive cruise control: Approximate verification of the discrete linear ACC model completes in 84 seconds, and is 22.7× faster on average than verification of the nonlinear model.Exact analysis is computationally expensive because reachable-set splits increase the number of star sets over time.
5 Related Work
NNV is situated within a broad landscape of neural-network and learning-enabled CPS verification methods, spanning open-loop and closed-loop analysis.
- Open-loop DNN verification includes SMT-based, mixed-integer linear programming, set-based, and optimization methods.
- Closed-loop NNCS verification includes approaches targeting nonlinear plants, different activation functions, discrete linear plants, and controllable conservativeness.
- NNV builds on prior research across both neural-network and machine-learning verification.
6 Conclusion and Future Work
The paper presents NNV as a toolbox for verifying DNNs and learning-enabled CPS, with exact and over-approximate analyses across linear and nonlinear closed-loop systems.
- NNV provides reachability algorithms for safety and robustness verification of real-world DNNs and learning-enabled CPS.
- For NNCS with linear plant models, NNV computes both exact and over-approximate reachable sets.
- For NNCS with nonlinear plants, NNV obtains over-approximate reachable sets for safety verification and supports falsification through counterexamples or randomized simulations.
A Appendix: Additional Evaluation Details
The appendix provides detailed ACAS Xu verification results for properties φ3 and φ4, comparing NNV’s star methods with several alternative verification methods.
- The detailed comparisons cover NNV’s approximate and exact star methods, zonotope, abstract domain, Reluplex, Marabou, and Marabou divide-and-conquer methods.
- Detailed verification results are shown for ACAS Xu safety property φ3.
- Detailed verification results are shown for ACAS Xu safety property φ4.