NNV3: Expanding Neural Network Verification to New Architectures and Domains

• NNV uses set-based reachability to compute possible outputs for input sets, building on support for feed-forward, convolutional, and control-system networks.Source: §1 · pp. 1–2
• NNV 2.0 added neural ODEs, recurrent networks, and semantic-segmentation networks, alongside relaxed methods and ONNX and VNNLIB support.Source: §1 · p. 2
• NNV3 adds verification for parameter perturbations, spatio-temporal and graph-structured models, probabilistic guarantees, fairness, and variable-length time-dependent networks.Its application domains include video, medical imaging, power systems, malware detection, and ethical decision-making; it also consolidates documentation.Source: §1 · p. 2

• The computation engine parses ONNX and MATLAB models and performs layer-by-layer set-based reachability; the analyzer checks robustness, VNNLIB safety, and fairness properties.The analyzer can use reachable sets or evaluation traces and supports visualization and counterexample generation.Source: §2 · p. 2
• The updated pipeline supports both sound and probabilistic reachability analysis.Source: Figure 1 · p. 3
• NNV3 extends support to graph neural networks and video models, and addresses fairness, parameter perturbations, and probabilistic guarantees beyond conventional robustness analysis.Source: §2 · p. 3
• NNV3 integrates previously independent capabilities through a common Star-set abstraction, shared specification interface, and documented developer API.The source identifies the set representations and analysis modes as having been introduced in prior work.Source: §2 · p. 3

3.1 Feature Highlights

• ModelStar represents interval-bounded weight perturbations and analyzes simultaneous input and parameter uncertainty, exactly for a single perturbed layer with singleton inputs and by sound over-approximation for multiple layers.It supports fully connected and 2D convolutional layers; quantized-compression rounding can be modeled, but fixed-point inference arithmetic is not yet modeled.Source: §3.1 · pp. 4–5
• VolumeStar represents spatio-temporal inputs for reachability through 3D convolutional and pooling layers, supporting video and 3D medical-imaging models.It can certify classification robustness within a specified input set; time-dependent networks can also be analyzed over a bounded, variable horizon.Source: §3.1 · p. 5
• GraphStar captures graph connectivity and uncertainty in node and edge features, exactly propagating affine message-passing operations and soundly over-approximating ReLU nonlinearities.Supported examples include GCN and GINE architectures, with power-system case studies.Source: §3.1 · p. 5
• Conformal-inference-based probabilistic verification uses sampling instead of exhaustive propagation to provide probabilistic coverage guarantees for models beyond practical exact analysis.The approach is model-agnostic and scales with inference cost.Source: §3.1 · p. 5
• FairNNV verifies counterfactual and individual fairness specifications over continuous input regions, with Verified Fairness measuring the proportion of inputs formally certified.Source: §3.1 · pp. 5–6

3.2 Core Upgrades & Extensibility

• VolumeStar, GraphStar, and ModelStar instantiate a shared Star-set template, with each representation defining its tensor space and generator semantics while reusing the propagation kernel.For VolumeStar, generators encode spatio-temporal variation and polyhedral constraints bound perturbations; GraphStar carries adjacency, while ModelStar generators represent perturbed weights.Source: §3.2 · p. 6
• Engine upgrades connect GNN message passing, 4D tensors, symbolic tracking of weight perturbations, and probabilistic analysis to the existing reachability framework.The probabilistic mode composes with sound reachability, so features implemented for the sound mode are also usable probabilistically.Source: §3.2 · p. 6
• A unified documentation site and developer API provide guidance for adding layer types, set representations, and verification properties.The documentation consolidates user and developer guides, API reference, theory background, and tutorials.Source: §3.2 · p. 7

• The malware benchmark evaluates static-feature classifier robustness to realistic functionality-preserving changes, including modifications to non-executable sections and appended benign bytes.Source: §4 · p. 7
• Graph verification supports power-flow, optimal-power-flow, and cascading-failure models with uncertainty in both node and edge features.The passage describes this as the first general-purpose framework for reachability analysis of topology-aware models of this kind.Source: §4 · p. 7
• NNV3’s probabilistic pipeline analyzes large lung-X-ray segmentation networks with dense pixel-level outputs, providing coverage guarantees and reducing conservatism relative to exact methods.Source: §4 · p. 7
• FairNNV reasons about bias in credit approval and loan-risk systems over continuous input regions, including input perturbations and counterfactual scenarios.Source: §4 · p. 7

Verification of Graph Neural Networks

• On IEEE-24 power flow, GraphStar evaluates GCN, SAGE, and GINE-Conv across four perturbation levels and 10 instances per architecture, as a feasibility demonstration rather than a scalability study.The common specification and reachability configuration is used across architectures; unverified nodes may be proven violations or unknown outcomes.Source: Figure 3 · p. 9, §5 · p. 9

Verification Under Weight and Parameter Perturbations

• At 0.2% perturbation on fc 4, ModelStar verifies 69/100 safe classifications versus 13 for Certificated-Robust, an absolute gain of 56 percentage points.Unverified images remain unknown because of over-approximation; wide or multiple perturbed layers increase Star-set dimensionality and later LP-solving time.Source: §5 · pp. 8–9

Verification of Spatio-Temporal and Volumetric Data

• On ZoomIn-4f, VolumeStar verifies 7/10 cases (70%) at every tested ε; the remaining three are unknown due to over-approximation.The evaluation uses a 30-minute timeout per sample; additional frames and larger spatial dimensions increase memory and reachability cost.Source: §5 · pp. 9–10, Table 2 · p. 11

Probabilistic Verification

• All three sampled properties from the TinyYOLO benchmark's 72 instances are UNSAT, with GPU verification taking 111–132 s per property.The probabilistic guarantee is at least 99.9% confidence that a fresh sampled input has its output inside the reachable set with probability at least 99.9%; the evaluation is a feasibility demonstration, not a scalability study.Source: §5 · p. 10, Table 3 · p. 11

Fairness Verification

• On Adult Census, counterfactual fairness reaches 87–89% verified fairness for both models at 0.72–0.78 s per sample; under individual fairness, verified fairness falls as ε grows, more steeply for the small model.The medium model incurs substantially higher verification cost; extending FairNNV to group-fairness specifications is future work.Source: §5 · pp. 10–11, Table 4 · p. 11

Tool Comparison

• Against AIVL, NNV3 verifies roughly half of ACAS Xu instances and more RL instances, matches Collins RUL, finds one extra OVAL21 counterexample, and both tools verify all 25 MNIST-ResNet-8 cases.On MNIST-ResNet-8, NNV3 is faster at smaller perturbation bounds, but its runtime rises with ε while AIVL's stays approximately constant.Source: §5 · pp. 11–13, Table 5 · p. 12, Table 6 · p. 12

Related Work

• Prior verification methods include SMT solving, bound propagation, abstract interpretation, and geometric approaches, often focused on FFNN and CNN robustness to Lp-bounded input perturbations.The paper compares NNV3's architecture and application coverage with existing tools in Table 8.Source: §6 · p. 13

Weight and Parameter Perturbations

• Most prior work assumes fixed weights, while ModelStar supports weight uncertainty and joint propagation of interval perturbations with input uncertainty via Star-set reachability.Related approaches include interval neural-network verification, interval bound propagation, and quantized-network verification.Source: §6 · pp. 13–14

VolumeStar

• Earlier video-classifier verification used a game-theoretic framework over 2D convolutional and LSTM layers, with perturbations restricted to optical flow; VolumeStar extends ImageStar to video-content perturbations and 3D layers.Source: §6 · p. 14

Graph Neural Network Verification

• Earlier formal GNN methods target node classification in a narrow set of architectures, whereas GraphStar generalizes to edge-aware GNNs with joint node and edge uncertainty.Prior approaches include feedforward-network encodings, matrix-polynomial-zonotope reachability, incremental constraint solving, and MILP.Source: §6 · p. 14

Probabilistic Verification

• Probabilistic verification combines scalability with guarantees, and NNV3 integrates conformal inference with set-based reachability to extend coverage guarantees to segmentation.Prior approaches include statistical and importance sampling, randomized smoothing, and conformal inference for classification.Source: §6 · p. 14

Fairness Verification

• FairNNV provides exact fairness certificates through reachability over continuous input regions, alongside prior probabilistic, abstract-interpretation, and SMT approaches with differing guarantees.Source: §6 · p. 14

7 Conclusion

• NNV uniquely supports a broad range of architectures, data modalities, and property classes, though specialized tools may outperform it on specific benchmarks.Its stated coverage includes GNNs, TDNNs, and 3D CNNs; images, video, and time series; and robustness, fairness, probabilistic guarantees, and weight perturbations.Source: §7 · p. 14
• NNV3 does not yet handle attention or autoregressive architectures, and ModelStar covers continuous weight perturbations but not fixed-point inference arithmetic.Source: §7 · p. 14
• Future work targets Python support, extensions to transformers, autoencoders, and temporal graph neural networks, and discrete fixed-point arithmetic for ModelStar.Source: §7 · pp. 14–15
• The planned addition of group-fairness definitions to FairNNV would enable direct comparison with probabilistic and group-fairness certifiers FairSquare and Justicia.Source: §7 · p. 15