NNV

NNV verifies safety and robustness properties of deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS) using set-based reachability analysis.

Key Features:

• Set-Based Verification Framework: Employs set representations to model reachable sets for analysis of DNNs and CPS.
• Polyhedra: Uses polyhedral sets to represent feasible regions in high-dimensional spaces for reachability computations.
• Star Sets: Utilizes star sets to approximate nonlinear functions and represent controller-induced sets for FFNNs.
• Zonotopes: Applies zonotopes for efficient representation and propagation under linear transformations and nonlinear dynamics approximations.
• Abstract-Domain Representations: Incorporates abstract-domain approximations to simplify complex reachable sets.
• Reachability Algorithms (Exact and Over-Approximate): Supports exact (sound and complete) algorithms for precise verification and over-approximate (sound) algorithms for computationally feasible conservative analysis.
• Feed-Forward Neural Network (FFNN) Verification: Verifies FFNNs with various activation functions, including piecewise-linear activations such as ReLUs, for safety and robustness properties.
• Learning-Enabled CPS Analysis — Linear Plants: Performs reachability analysis for linear plant models controlled by FFNN controllers, including piecewise-linear activation cases.
• Learning-Enabled CPS Analysis — Nonlinear Plants: Combines star set analysis for FFNN controllers with zonotope-based analysis for nonlinear dynamics, building on the CORA framework.

Scientific Applications:

• ACAS Xu Networks: Safety verification of neural networks used in airborne collision avoidance systems (ACAS Xu).
• Adaptive Cruise Control Systems: Safety verification of deep learning–based adaptive cruise control systems for vehicles.

Methodology:

NNV uses a set-based verification approach and reachability algorithms (exact sound-and-complete and over-approximate sound variants) with polyhedra, star sets, zonotopes, and abstract-domain representations; it analyzes FFNNs with various activation functions (including ReLUs) and, for nonlinear plant models, combines star set analysis for controllers with zonotope-based analysis of dynamics using the CORA framework.