NNV3: Expanding Neural Network Verification to New Architectures and Domains
cs.AI
Submitted: 2026-09-24
Updated: 2026-09-24
Code: https://github.com/verivital/nnv
Project page: https://verivital.github.io/nnv
License: http://creativecommons.org/licenses/by/4.0/
The gist: We present NNV3, the latest version of the Neural Network Verification (NNV) tool, a MATLAB framework for formal verification of deep learning models and learning-enabled cyber-physical systems.
Terminology
Abstract
We present NNV3, the latest version of the Neural Network Verification (NNV) tool, a MATLAB framework for formal verification of deep learning models and learning-enabled cyber-physical systems. Building on the set-based reachability foundation of NNV 1.0 (FFNNs, CNNs, NNCS) and NNV 2.0 (RNNs, SSNNs, neural ODEs), NNV3 introduces new members of the Star-set family: ModelStar for verifying networks under weight perturbation, VolumeStar for video and 3D volumetric inputs, and GraphStar for graph neural networks. A conformal-inference-based probabilistic reachability mode complements sound analysis for problems where deterministic verification is intractable, while FairNNV certifies counterfactual and individual fairness properties over continuous input regions. NNV3 introduces new benchmarks for malware detection, graph-based power-system models, medical imaging, variable-length time series data, and action recognition. NNV3 also incorporates tutorials and developer guides through a unified documentation site. This paper details these major updates, demonstrating NNV's maturation into a comprehensive, robust, and accessible verification tool for a diverse range of AI systems.
Sources
- The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results
- The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results
- A DPLL(T) Framework for Verifying Deep Neural Networks
- A Survey on Methods and Theories of Quantized Neural Networks
- Probabilistic Robustness Analysis in High Dimensional Space: Application to Semantic Segmentation Network
- The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results
- VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification
Related papers
- MAVEN-T: Reinforced Heterogeneous Distillation for Real-Time Multi-Agent Trajectory Prediction
- Model Discovery Agent: LLM-assisted Bayesian experiment design for data-efficient discovery of mechanistic world models
- Agents' Last Exam
- The Clinician's Veto: Navigating Trust, Liability, and Uncertainty in Autonomous AI Prescribing
- MindHelper: Closed-Loop Embodied Mental-State Reasoning for Precision Intervention
- Incumbent Advantage: Brand Bias and Cognitive Manipulation Dynamics in LLM Recommendation Systems