NNV3: Expanding Neural Network Verification to New... | AI Research

What the paper is about

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. The same ai evaluation question is explored in Learning Cardiac Features, which adds a research perspective.

What it covers

NNV3 : Expanding Neural Network Verification to New Architectures and Domains Thanks: A.Tumlin and S.Sasaki are co-first authors. Anne M. Tumlin Affiliation: Vanderbilt University, USA Samuel Sasaki Affiliation: Vanderbilt University, USA Ben Wooding Affiliation: Vanderbilt University, USA Diego Manzanas Lopez Affiliation: Vanderbilt University, USA Muhammad Usama Zubair Affiliation: The University of Texas at Dallas, USA Navid Hashemi Affiliation: Vanderbilt University, USA Hongchao Zhang Affiliation: Vanderbilt University, USA Waseem Abbas Affiliation: The University of Texas at Dallas, USA Ipek Oguz Affiliation: Vanderbilt University, USA Meiyi Ma Affiliation: Vanderbilt University, USA Taylor T. Johnson Affiliation: Vanderbilt University, USA 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. 1 Introduction Deep neural networks (DNNs) have become integral to solving complex problems across various domains, from image classification to autonomous control. However, their deployment in safety-critical applications is hindered by their opaque nature and susceptibility to adversarial perturbations. Formal verification provides a means to analyze and rigorously guarantee the behavior of these models, which is essential for establishing trust in AI-powered systems. The Neural Network Verification ( NNV ) 1 1 1 https://github.com/verivital/nnv/ tool [ 72 ] was introduced as a comprehensive, open-source MATLAB toolbox to tackle this challenge. NNV is built around a powerful computation engine that performs set-based reachability analysis, computing the set of all possible outputs for a given set of inputs. The initial release of NNV focused on providing exact and over-approximate reachability for feed-forward neural networks (FFNNs), convolutional neural networks (CNNs), and neural network control systems (NNCS) using a variety of set representations like polyhedra, zonotopes, and the novel star set. Building on this foundation, NNV 2.0 [ 47 ] expanded the tool’s scope to handle a wider array of complex and dynamic network architectures. It introduced verification support for neural ordinary differential equations (neural ODEs), recurrent neural networks (RNNs), and semantic segmentation neural networks (SSNNs). This version also improved scalability with new relaxed reachability methods [ 71 ] and enhanced usability by supporting standard community formats like ONNX [ 50 ] and VNNLIB [ 54 ] . This paper presents NNV3 , an evolution of the NNV tool that addresses emerging challenges in AI verification and broadens the tool’s applicability to new domains and data types. While previous versions focused on expanding architectural support, NNV3 introduces verification techniques for new classes of properties and extends reachability analysis to previously intractable data modalities. The contributions span three categories. Algorithmic and model improvements introduce reachability-based verification for parameter perturbations (ModelStar [ 90 , 91 ] ), spatio-temporal data (VolumeStar [ 55 ] ), graph-structured models (GNNV with GraphStar [ 75 ] ), probabilistic guarantees via conformal inference [ 27 ] , fairness properties (FairNNV [ 74 ] ), and variable-length time-dependent networks [ 51 ] . New application domains unlocked by these algorithms include video classification [ 55 ] , medical-image segmentation [ 26 ] , power-system analysis [ 75 ] , malware detection [ 53 ] , ethical decision-making [ 74 ] , and deployment-uncertainty robustness [ 90 , 91 ] . System upgrades include a unified documentation site 2 2 2 https://verivital.github.io/nnv/ that consolidates the user guide, developer guide, API reference, etc. These advancements solidify NNV ’s position as one of the most comprehensive and versatile verification frameworks available to the research community. 2 NNV3 vs. NNV 2.0 The core architecture of NNV , illustrated in Fig. 1 , is composed of two primary modules: the Computation Engine and the Analyzer . The Computation Engine parses neural network and system models ( ONNX and MATLAB formats) and performs layer-by-layer reachability analysis using set-based abstractions, including Star sets [ 70 ] , ImageStar [ 65 ] , and newly introduced representations such as VolumeStar ( a.k.a VideoStar) [ 55 ] , ModelStar [ 90 , 91 ] , and GraphStar [ 75 ] . In NNV3 , the computation engine supports both sound reachability and a probabilistic reachability mode [ 27 ] , the latter enabling scalable verification via sampling-based uncertainty quantification. The Analyzer consumes the resulting reachable sets or evaluation traces to verify system-level properties — including robustness, safety specifications expressed in VNNLIB , and fairness constraints — and supports visualization, verification, and counterexample generation. Together, these extensions broaden the scope of verifiable models while preserving the modular structure of the NNV framework. Figure 1 : Updated NNV verification pipeline, composed of a computation engine and analyzer, and extended to support both sound and probabilistic reachability analysis. Practitioners working with heterogeneous, real-world AI systems require a unified and extensible verification framework. This drives the continued evolution of NNV . Table 1 illustrates that NNV and its prior iterations support a broad spectrum of architectures and applications, including feedforward and convolutional networks (FFNNs and CNNs), recurrent models (RNNs), semantic segmentation (SSNNs), neural ODEs, and neural network control systems (NNCSs). With the release of NNV3 , we expand the tool to emerging and increasingly important model classes, including graph neural networks (GNNs) and video classification architectures (VolumeStar). NNV3 addresses a broader class of deployment-relevant properties, including algorithmic fairness, parameter and weight perturbations, and probabilistic guarantees. These capabilities enable verification beyond conventional robustness analysis and reflect practical concerns encountered in real-world deployment. NNV has been evaluated consistently in community benchmarks such as VNN-COMP [ 39 ] and ARCH-COMP [ 46 , 56 ] , and has served as the foundation for tutorials at DESTION [ 67 ] , EMSOFT [ 69 ] , DSN [ 36 ] , SPIE, IAVVC, AAAI, etc. , underscoring its maturity and continued relevance to the verification community (see the user guide 3 3 3 https://verivital.github.io/nnv/user-guide/index.html and the tutorials index 4 4 4 https://verivital.github.io/nnv/examples/index.html for further details). Relation to prior publications. The set representations and analysis modes incorporated into NNV3 were introduced individually in prior work [ 91 , 55 , 75 , 27 , 74 ] . This work contributes their systematic integration into a unified verification framework. Previously, these capabilities were implemented as independent prototypes with distinct interfaces, dispatch mechanisms, and evaluation pipelines. NNV3 consolidates these developments through a common Star-set abstraction, a shared specification interface, and a documented developer API, enabling verification specifications and reachability procedures to be used consistently across supported representations. The resulting framework is further supported by continuous integration testing, unified documentation for the full representation family, and reproducibility packages for each experiment reported in Section 5 . The remainder of the paper is organized as follows. Section 3 summarizes major new features and capabilities. Section 4 introduces the extended domain applications. We then validate new features in Section 5 and refresh the comparison with the MathWorks AI Verification Library. Finally, we discuss related works in Section 6 , and conclude the paper in Section 7 . 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. Feature Supported (NNV 1.0, NNV 2.0 , NNV3 ) Neural Network Type FFNN, CNN, NeuralODE , SSNN , RNN , GNN , TDNN , 3D CNN Layers MaxPool, Conv, BN, AvgPool, FC, MaxUnpool , TC , DC , NODE , GCN , GINE , Conv3D Activation functions ReLU, Satlin, Sigmoid, Tanh, Leaky ReLU , Satlins Plant dynamics (NNCS) Linear ODE, Nonlinear ODE, Continuous & Discrete Time, HA Set Representation Polyhedron, Zonotope, Star, ImageStar, VolumeStar , ModelStar , GraphStar Star Reach methods exact, approx, abs-dom, relax-* Reachable set visualization exact and over-approximation Verification Safety, Robustness, VNNLIB , Fairness , Weight Perturbation , Probabilistic Miscellaneous Parallel computing, counterexample generation, ONNX , CI/CD 3 Overview and Features This section summarizes the major features introduced in NNV3 and in Table 1 . These additions extend the reachability-based verification capabilities of prior versions of NNV to new model classes, data modalities, and verification objectives, while preserving soundness guarantees and compatibility with existing analysis pipelines. Section 3.1 presents the per-feature highlights; Section 3.2 describes the underlying engine and extensibility upgrades. 3.1 Feature Highlights ModelStar [ 90 , 91 ] : Neural networks deployed in practice are subject to parameter uncertainty arising from quantization, numerical imprecision, and hardware faults [ 61 , 88 , 24 ] . To address this, NNV3 introduces ModelStar, a star-set–based representation for interval-bounded weight perturbations. ModelStar enables reachability analysis under simultaneous input and parameter uncertainty. For networks with a single perturbed layer and singleton inputs, the reachable set of the perturbed layer is computed exactly; for multi-layer perturbations, sound over-approximations are constructed using Star sets. ModelStar is currently implemented for fully-connected and 2D convolutional layers and can be readily implemented for verification against weight perturbations in any linear layer. Rounding errors introduced by quantized compression can be modeled as interval-bounded specifications for ModelStar — as demonstrated in the experiments in Section 5 --- but fixed-point inference arithmetic (discrete operations) is not yet modeled. 5 5 5 https://verivital.github.io/nnv/theory/weight-perturbation.html VolumeStar (VideoStar) [ 55 ] : NNV can formally verify the robustness of video classifiers. Verification of neural networks operating on spatio-temporal data, such as videos and volumetric medical images, presents significant scalability challenges due to input dimensionality. NNV3 extends the Star and ImageStar representations [ 70 , 65 ] to VolumeStar, a set abstraction for spatio-temporal inputs, e.g. , an image at each time step. VolumeStar supports reachability analysis of architectures with 3D convolutional and pooling layers, including video classification networks (such as C3D [ 64 ] and I3D [ 12 ] ), as well as 3D medical imaging models [ 89 ] . Using VolumeStar reachability, NNV can formally certify classification robustness for all admissible spatio-temporal perturbations within a specified input set. In addition, NNV3 extends star-based reachability analysis to time-dependent neural networks (TDNNs) by allowing the analysis horizon to vary over a bounded temporal range, generalizing prior support for fixed-length recurrent models. 6 6 6 https://verivital.github.io/nnv/theory/imagestar-volumestar.html GraphStar [ 75 ] : Graph neural networks (GNNs) are increasingly used as surrogates for numerical solvers in domains such as molecular modeling, traffic forecasting, and power-system analysis [ 85 ] . NNV3 introduces GNNV, extending reachability-based verification to graph-structured learning models. GNNV implements GraphStar, a generalization of Star sets that captures both graph connectivity and uncertainty in node and edge features. This abstraction enables exact propagation of affine message-passing operations and sound over-approximation of ReLU nonlinearities in common GNN architectures, including graph convolutional networks (GCNs) [ 40 ] and graph isomorphism networks with edge features (GINE) [ 32 ] . GraphStar reachability is demonstrated on power-system case studies, including power flow, optimal power flow, and cascading failure analysis [ 77 ] . 7 7 7 https://verivital.github.io/nnv/theory/gnn-reachability.html Probabilistic Verification [ 27 ] : Exact reachability analysis can become intractable for large networks due to exponential complexity in the number of unstable nonlinear activations. To address this limitation, NNV3 integrates a probabilistic, model-agnostic verification approach based on conformal inference. Given an input set, a neural network, and a specification, verification is performed via sampling rather than exhaustive propagation. This approach scales with inference cost and is independent of network architecture, providing probabilistic coverage guarantees for models that are beyond the practical reach of exact methods. 8 8 8 https://verivital.github.io/nnv/theory/probabilistic.html Fairness Verification [ 74 ] : As machine learning systems are deployed in high-stakes decision-making settings, verification of fairness properties has become increasingly important [ 48 ] . NNV3 integrates FairNNV, a reachability-based framework for formally validating fairness specifications over continuous input regions. FairNNV verifies specifications corresponding to counterfactual fairness [ 42 ] , which requires predictions to remain invariant under changes to sensitive attributes, and individual fairness, which enforces similar outcomes for inputs within a bounded neighborhood. Fairness is quantified using the Verified Fairness (VF) score, defined as the proportion of inputs for which fairness properties are formally certified. 9 9 9 https://verivital.github.io/nnv/theory/fairness.html 3.2 Core Upgrades & Extensibility Star-set family unification. VolumeStar, GraphStar, and ModelStar are not disjoint abstractions but instances of a common Star-set template, parameterized by an anchor, a generator basis, and a polyhedral constraint on the generator coefficients. Definition 1 (Star-set template) A star set over a tensor space 𝒯 \mathcal{T} is a tuple ⟨ c , V , P , q ⟩ \langle c,V,P,q\rangle consisting of an anchor c ∈ 𝒯 c\in\mathcal{T} , a generator basis V = { v 1 , … , v m } ⊂ 𝒯 V={v_{1},\dots,v_{m}}\subset\mathcal{T} , and a polyhedral constraint ( P , q ) ∈ ℝ p × m × ℝ p (P,q)\in\mathbb{R}^{p\times m}\times\mathbb{R}^{p} on the predicate variables α = [ α 1 , … , α m ] ⊤ \alpha=[\alpha_{1},\dots,\alpha_{m}]^{\top} . It denotes the set Θ = { x ∈ 𝒯 | x = c + ∑ i = 1 m α i v i , P α ≤ q } . \Theta=\Big{,x\in\mathcal{T};\Big|;x=c+\textstyle\sum_{i=1}^{m}\alpha_{i}v_{i},;P\alpha\leq q,\Big}. Each member of the family instantiates Definition 1 by fixing 𝒯 \mathcal{T} and the semantics of the generators, and inherits the shared propagation kernel unchanged. VolumeStar, for example, takes 𝒯 = ℝ H × W × C × F \mathcal{T}=\mathbb{R}^{H\times W\times C\times F} for a volume of height H H , width W W , C C channels, and F F frames: the anchor is the nominal video, each generator is a volume encoding one direction of admissible spatio-temporal variation, and P ​ α ≤ q P\alpha\leq q bounds the perturbation, e.g. , | α i | ≤ ϵ |\alpha_{i}|\leq\epsilon for an L ∞ L_{\infty} bound applied across all frames. Star and ImageStar differ from it only in the rank of 𝒯 \mathcal{T} ( ℝ n \mathbb{R}^{n} and ℝ H × W × C \mathbb{R}^{H\times W\times C} , respectively), whereas GraphStar carries the adjacency structure alongside the node- and edge-feature tensors, and ModelStar draws its generators from perturbed weight entries rather than from input dimensions. Extending NNV to a new modality therefore reduces to instantiating Definition 1 and implementing layer-specific dispatch over the shared propagation kernel. Engine-level changes. Several core-engine upgrades support the new abstractions: a GNN wrapper that maps message-passing layers onto Star-set affine operations and routes adjacency through GraphStar; a 4D-tensor extension of the ImageStar reach kernels that lets VolumeStar inherit existing 3D-conv and pooling implementations; perturbation tracking in ModelStar that maintains symbolic dependencies between input generators and weight-perturbation generators across linear layers; and a probabilistic reachability mode that composes with sound reachability so that any feature implemented for the sound mode is automatically usable in the probabilistic mode. Continuous Integration and Deployment (CI/CD). To improve reliability and maintainability, NNV3 adopts a continuous integration and continuous deployment pipeline based on GitHub Actions. The pipeline automatically builds and tests the codebase for each commit and pull request, including unit tests for core reachability methods and regression tests on established benchmarks. This ensures backward compatibility and supports sustained development of NNV as an open-source verification tool. Extensibility and developer API. NNV3 ’s engine and analyzer modules are documented as a stable developer-facing API 10 10 10 https://verivital.github.io/nnv/api/index.html with guidance for adding new layer types, set representations, and verification properties. 11 11 11 https://verivital.github.io/nnv/developer/index.html The unified documentation site now provides the user guide, developer guide, API reference, theory background, and the tutorials index as a single entry point. Together, these resources lower the barrier for contributors extending NNV to architectures and properties beyond those listed in Table 1 . 4 New Domains NNV3 ’s new abstractions and probabilistic mode unlock application domains previously out of reach for reachability-based methods, characterized by high-dimensional inputs, structured representations, or deployment-driven threat models that exceed traditional L p L_{p} -bounded robustness analysis. Below we highlight four such domains. Malware Detection [ 53 ] : DNN malware classifiers are vulnerable to adversarial evasion, where attackers apply small functionality-preserving modifications to bypass detection. NNV3 introduces a benchmark for verifying robustness of static-feature classifiers under realistic feature-space perturbations (e.g., modifying non-executable sections, appending benign bytes), enabling formal assessment of classifier resilience under a well-defined threat model. Power-System Analysis [ 75 ] : Power flow, optimal power flow, and cascading failure analysis are naturally graph-structured and increasingly use GNN surrogates [ 77 ] , yet prediction errors carry severe operational consequences. Through GNN verification, NNV3 provides the first general-purpose framework supporting reachability analysis of such topology-aware models with both node- and edge-feature uncertainty. Medical Imaging Classification [ 27 , 26 ] : High-dimensional semantic segmentation defeats exact verification. NNV3 ’s probabilistic pipeline analyzes large segmentation networks on lung X-ray datasets [ 35 , 11 ] with dense pixel-level outputs, providing coverage guarantees while substantially reducing conservatism relative to exact methods [ 27 ] . Financial Predictions [ 74 ] : FairNNV extends NNV3 to consequential decision making systems such as credit approval and loan risk assessment [ 7 , 30 , 49 ] . Unlike statistical auditing over finite datasets, reachability-based fairness analysis certifies properties over continuous input regions, formally reasoning about bias under input perturbations and counterfactual scenarios. 5 Evaluation NNV3 ’s primary contribution is its breadth of supported architectures, specifications, and threat models, many of which lack a direct comparison, as summarized in Table 8 . Accordingly, the evaluations presented here are intended as feasibility demonstrations of the integrated framework across domains rather than exhaustive scalability studies of individual features. The per-feature suites are intentionally compact, allowing the full evaluation to be reproduced within several hours while exercising each supported analysis pipeline. More extensive feature-specific comparisons are reported in the corresponding prior works, including GraphStar against CORA [ 75 ] and the conformal verification pipeline [ 27 ] . We summarize the relevant results below and additionally refresh the NNV 2.0 head-to-head evaluation [ 47 ] against the MathWorks AI Verification Library (AIVL) [ 63 ] for FFNN and CNN models supported by both tools. All experiments were conducted using the MATLAB 2025b Docker container on a machine equipped with an Intel 24 Core i9-285K CPU, 64 GB RAM, and an NVIDIA RTX 5090 GPU with 32 GB VRAM. 12 12 12 The evaluation artifact (v3.0-atva26) is archived at https://doi.org/10.5281/zenodo.20433720 ; the live repository is available at https://github.com/verivital/nnv . Figure 2 : Single-layer weight-perturbation verification on the MNIST MLP. (Top) fraction of images verified safe; (bottom) average execution time per image, both vs. the L ∞ L_{\infty} -norm perturbation magnitude. Verification Under Weight and Parameter Perturbations. We evaluate ModelStar [ 90 , 91 ] on an MNIST MLP (5 hidden layers: 1024, 512, 256, 256, 256) against Certificated-Robust [ 81 ] and Formal-Robust [ 73 ] (Fig. 2 ). Perturbations are L ∞ L_{\infty} bounds on each layer’s weight range, with magnitudes 0.05%/0.1%/0.2%/0.4% corresponding to 10-/9-/8-/7-bit quantization rounding error. While ModelStar supports independently varying perturbations for individual weights [ 91 ] , the baselines support only uniform row-wise [ 81 ] or matrix-wise [ 73 ] perturbations. To ensure a fair comparison, we use a common perturbation magnitude for all weights in each perturbed layer and evaluate one layer’s robustness against one perturbation magnitude at a time. On 100 MNIST test images, ModelStar consistently matches or exceeds prior bounds: at 0.2% perturbation on fc_4 , it verifies the safe classification of 69/100 images versus 13 for Certificated-Robust (an absolute gain of 56 percentage points). For all three approaches, the classification safety of the NN for the unverified images is unknown due to over-approximation. The scalability of ModelStar is limited by the width and number of perturbed layers: perturbing wide or multiple layers substantially increases Star-set dimensionality, leading to higher LP-solving times in subsequent nonlinear layers. These results demonstrate that the ModelStar extension allows NNV3 to certify network robustness under quantization or hardware-induced weight uncertainty, addressing a deployment threat model beyond the reach of input-only verifiers. Figure 3 : GNNV verification on IEEE-24 power flow across three architectures (GCN, SAGE, GINE-Conv) vs. node-feature perturbation ϵ \epsilon (log axis). (Left) percentage of voltage-magnitude nodes verified. (Right) average verification time per graph instance (log scale). Verification of Graph Neural Networks. We evaluate GraphStar [ 75 ] on AC power flow (PF) for the IEEE-24 bus system using 10 graph instances each for GCN, SAGE, and GINE-Conv models under the ML4ACOPF perturbation scheme [ 39 ] . We consider L ∞ L_{\infty} perturbations to active and reactive power node features for ϵ ∈ { 10 − 5 , 10 − 4 , 10 − 3 , 10 − 2 } \epsilon\in{10^{-5},10^{-4},10^{-3},10^{-2}} , with voltage magnitude as the safety constraint. A common specification and reachability configuration is applied across all three architectures, demonstrating GraphStar’s ability to verify differing message-passing architectures under a consistent threat model. Figure 3 summarizes this evaluation by reporting the percentage of voltage-magnitude nodes verified and the average verification time per graph instance for each architecture; the remaining nodes correspond to either proven violations or unknown outcomes. As GraphStar’s computational complexity depends on graph size and network depth, this evaluation serves as a feasibility demonstration on a representative power-grid system rather than a comprehensive scalability study. This demonstrates reachability-based verification of GNN surrogates and supports formal analysis of GNN-based estimators. Verification of Spatio-Temporal and Volumetric Data. We evaluate VolumeStar [ 55 ] on the ZoomIn-4f benchmark, a 4-frame MNIST-video classifier, under L ∞ L_{\infty} perturbations ϵ ∈ { 1 / 255 , 2 / 255 , 3 / 255 } \epsilon\in{1/255,2/255,3/255} with a 30-minute timeout per sample. VolumeStar verifies 7/10 (70%) of cases at every ϵ \epsilon tested (Table 2 ); the remaining three are unknown due to over-approximation. The scalability of VolumeStar is limited by frame count and volume: additional frames and larger spatial dimensions enlarge the generator basis, increasing memory and reachability cost per sample. This delivers the first reachability-based robustness certification for 3D-convolutional video classifiers, a modality where ImageStar-based propagation is intractable. Probabilistic Verification. We evaluate NNV3 ’s probabilistic verification pipeline [ 27 ] on the TinyYOLO object detector from VNN-COMP 2023 [ 9 ] . The approach combines randomized falsification with conformal prediction–based reachability analysis. A surrogate model is trained to approximate the network, and conformal inference over a calibration set bounds its error, yielding a reachable set (Table 3 ). The guarantee is two-level: with confidence at least 99.9 % 99.9% over the draw of the calibration set, a fresh input from the sampling distribution has its output inside the reachable set with probability at least 99.9 % 99.9% , where the confidence follows from the calibration size and rank through a Beta tail bound [ 27 ] . We evaluate three randomly selected VNNLIB property specifications from the benchmark’s 72 instances. All three properties are verified as UNSAT (specification holds), with GPU-accelerated verification requiring 111–132 s per property. As in the sound mode, UNSAT means that the reachable set does not intersect the unsafe region. The set is not an over-approximation, however, and may omit the outputs of some inputs, so the verdict holds with the coverage and confidence stated above. Since the result is an ordinary Star set, the same specification routine checks it as in sound reachability, and any pipeline containing a CP-Star step yields a probabilistic verdict with that step’s coverage and confidence. The dominant costs are the calibration size, which grows with the requested coverage and confidence, and property complexity, since the memory of the inflated set grows with the output dimension and every output constraint requires an LP over it. The evaluation therefore serves as a feasibility demonstration on a perception-scale model rather than a scalability study. This extends NNV to instances for which sound reachability is intractable—for example, when the network is too large for the analysis to complete—since the probabilistic mode’s cost scales with inference rather than with the number of unstable neurons. ϵ \epsilon Ver. Unk. Avg. Time (s) 1 / 255 1/255 7 3 35.54 2 / 255 2/255 7 3 37.88 3 / 255 3/255 7 3 36.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. Property ϵ \epsilon Time (s) Result Prop 101 1 / 255 1/255 131.86 UNSAT Prop 277 1 / 255 1/255 111.92 UNSAT Prop 356 1 / 255 1/255 111.26 UNSAT Table 3 : Probabilistic verification on TinyYOLO (CP-Star, local Docker build with GPU). Coverage and confidence of 0.999 0.999 each require m = 9,230 m=9{,}230 calibration samples per property. 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 . CF IF ( ϵ \epsilon ) Model metric ( ϵ = 0 \epsilon{=}0 ) 0.01 0.02 0.03 0.05 0.07 0.10 Small VF (%) 89 87 84 81 69 50 22 Time (s) 0.78 0.89 1.06 1.40 2.17 3.41 5.53 Medium VF (%) 87 86 84 82 71 50 27 Time (s) 0.72 2.64 5.76 10.10 21.75 39.73 98.70 Fairness Verification. We evaluate FairNNV [ 74 ] on the A The same ai safety question is explored in Finite-Sample Probabilistic Safety Certification for AI-Based..., which adds a research perspective. as detailed in the full paper on Arxiv The same ai evaluation question is explored in LLM-Generated Feature Pools for Time Series..., which adds a research perspective.