cs.AISep 24, 2026

NNV3: Expanding Neural Network Verification to New Architectures and Domains

Authors: Anne M. Tumlin, Samuel Sasaki, Ben Wooding, Diego Manzanas Lopez, Muhammad Usama Zubair, Navid Hashemi, Hongchao Zhang, Waseem Abbas, +3 more

Organizations: Vanderbilt University, USA · The University of Texas at Dallas, USA

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Figures & tables

FeatureSupported (NNV 1.0, NNV 2.0 , NNV3 )
Neural Network TypeFFNN, CNN, NeuralODE , SSNN , RNN , GNN , TDNN , 3D CNN
LayersMaxPool, Conv, BN, AvgPool, FC, MaxUnpool , TC , DC , NODE , GCN , GINE , Conv3D
Activation functionsReLU, Satlin, Sigmoid, Tanh, Leaky ReLU , Satlins
Plant dynamics (NNCS)Linear ODE, Nonlinear ODE, Continuous & Discrete Time, HA
Set RepresentationPolyhedron, Zonotope, Star, ImageStar, VolumeStar , ModelStar , GraphStar
Star Reach methodsexact, approx, abs-dom, relax-*
Table 1 : Overview of major features available in NNV. Items in regular weight are NNV 1.0 baseline; blue italics denote additions introduced in NNV 2.0; purple bold denote new capabilities introduced in NNV3.
ϵ\epsilonVer.Unk.Avg. Time (s)
1/2551/2557335.54
2/2552/2557337.88
3/2553/2557336.49
Table 2 : VolumeStar verification on ZoomIn-4f under L∞L_{\infty} perturbations (10 samples per ϵ\epsilon , 30-min timeout). Ver. verified robust; Unk. unknown due to over-approximation.
  CFIF ( ϵ\epsilon )
Modelmetric( ϵ=0\epsilon{=}0 )0.010.020.030.050.070.10
SmallVF (%)89878481695022
 Time (s)0.780.891.061.402.173.415.53
MediumVF (%)87868482715027
 Time (s)0.722.645.7610.1021.7539.7398.70
Table 4 : FairNNV verification on Adult Census: Verified Fairness (VF, %) and per-sample verification time (s). Counterfactual fairness (CF) perturbs only the sensitive attribute ( ϵ=0\epsilon{=}0 ); individual fairness (IF) additionally perturbs non-sensitive features at radius ϵ\epsilon .
 ACAS p3 ( N=20N{=}20 )ACAS p4 ( N=20N{=}20 )RL ( N=50N{=}50 )
 VXUTSVXUTSVXUTS
AIVL031700.06011900.0720111900.04
exact830958.23930883.993215125.36
approx103700.6993800.903214400.14
r-50121700.30121700.303214400.08
Table 5 : Tool comparison on fully-connected VNNLIB benchmarks. Per cell: V verified, X violated, U unknown, T timeout, S mean per-instance time (seconds). Timeout cap: 900 s. AIVL uses est-bnds ; r-50 is NNV3’s relax-star-range-50 . Bold marks NNV3’s strongest verification count per benchmark.
 NNV3AIVL [ 63 ]α,β\alpha,\beta -Crown [ 86 , 79 ]CORA [ 3 , 2 , 43 ]FastBATLLNN [ 19 ]JuliaReach [ 8 , 58 ]Marabou [ 38 , 83 , 82 ]NeuralSAT [ 17 , 16 ]NeVer2 [ 15 ]nnenum [ 5 ]ReachNN [ 33 , 18 ]Reluplex [ 37 ]SobolBox [ 14 ]StarV [ 66 ]Verinet [ 28 ]Verisig [ 34 ] 
FFNN✓\checkmark✓\checkmark✓\checkmark✓\checkmark✓\checkmark✓\checkmark✓\checkmark✓\checkmark✓\checkmark✓\checkmark×\times✓\checkmark✓\checkmark✓\checkmark✓\checkmark×\times 
CNN✓\checkmark✓\checkmark✓\checkmark✓\checkmark×\times✓∗\checkmark*✓\checkmark✓\checkmark✓\checkmark✓\checkmark×\times×\times✓\checkmark✓\checkmark✓\checkmark×\times 
RNN✓\checkmark×\times✓\checkmark×\times×\times×\times×\times×\times×\times×\times×\times×\times×\times✓\checkmark×\times×\times 
SSNN✓\checkmark×\times✓∗\checkmark^{*}×\times×\times×\times×\times×\times×\times×\times×\times×\times×\times✓\checkmark×\times×\times 
TDNNs✓\checkmark×\times×\times×\times×\times×\times×\times×\times×\times×\times×\times×\times×\times×\times×\times×\times 
GNNs✓\checkmark×\times×\times✓\checkmark×\times×\times✓∗\checkmark^{*}×\times×\times×\times×\times×\times×\times×\times×\times×\times 
Table 8 : Comparison of neural network verification tools by supported architectures and applications, with ✓\checkmark meaning supported by a tool and ×\times not supported. We use ∗ to indicate partial support. In purple italics , the newly supported architecture/applications by NNV3 . WPP signifies model perturbations.

Explore similar work

CardsList

  1. VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification

    May 8, 2026Ann Roy, Allen Antony, Andrea Gimelli +1Neural Network VerificationFormal Verification

    University of Western Australia, Perth, Australia · University of Genoa, Genoa, Italy

  2. TNODEV: Toolbox for Neural ODE Verification

    Jun 15, 2026Abdelrahman Sayed Sayed, Pierre-Jean Meyer, Mohamed GhazelNeural Network VerificationNeural Ordinary Differential Equations

    Univ Gustave Eiffel, COSYS-ESTAS, F-59657 Villeneuve d’Ascq, France

  3. Stress-Testing Neural Network Verifiers with Provably Robust Instances

    May 16, 2026David Troxell, Yulia Alexandr, Sofia Hunt +2Neural Network VerificationVerification Framework

    Department of Statistics & Data Science, University of California, Los Angeles · Department of Mathematics, University of California, Los Angeles · Max Planck Institute for Mathematics in the Sciences, Leipzig