Neural Network Verification

Follow this topic Ask about this topic

Neural network verification asks whether a model satisfies precise properties, such as resisting bounded input perturbations or keeping a controller within a safe region. Common approaches include interval and linear bound propagation, abstract interpretation, reachability analysis, and solver-based methods such as mixed-integer programming and branch-and-bound. Researchers are extending these techniques from feed-forward classifiers to transformers, recurrent and graph networks, and closed-loop control systems, while also developing benchmarks, proof systems, and tools for trustworthy execution. A central challenge is balancing sound guarantees and tight bounds against the time and memory required, especially for large models and realistic arithmetic.

Latest papers

126 papers16 papers in the last four weeks, up 7% on the four weeks before. 0.1% of all new papers.

Apr 23, 2026

Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

The problem of probabilistic verification of a neural network investigates the probability of satisfying the safe constraints in the output space when the input is given by a probability distribution. It is significant to answer this problem when the input is affected by disturbances often modeled by probabilistic variables. In the paper, we propose a novel neural network probabilistic verification framework which computes a guaranteed range for the safe probability by efficiently finding safe and unsafe probabilistic hulls. Our approach consists of three main innovations: (1) a state space subdivision strategy using regression trees to produce probabilistic hulls, (2) a boundary-aware sampling method which identifies the safety boundary in the input space using samples that are later used for building regression trees, and (3) iterative refinement with probabilistic prioritization for computing a guaranteed range for the safe probability. The accuracy and efficiency of our approach are evaluated on various benchmarks including ACAS Xu and a rocket lander controller. The result shows an obvious advantage over the state of the art.

Jingyang Li, Xin Chen, Hongfei Fu +1

Shanghai Jiao Tong University, Shanghai 200240, China · University of New Mexico, Albuquerque, NM 87106, USA

Neural Network Verification

Apr 20, 2026

The Cost of Relaxation: Evaluating the Error in Convex Neural Network Verification

Many neural network (NN) verification systems represent the network's input-output relation as a constraint program. Sound and complete, representations involve integer constraints, for simulating the activations. Recent works convexly relax the integer constraints, improving performance, at the cost of soundness. Convex relaxations consider outputs that are unreachable by the original network. We study the worst case divergence between the original network and its convex relaxations; both qualitatively and quantitatively. The relaxations' space forms a lattice, where the top element corresponds to a full relaxation, with every neuron linearized. The bottom element corresponds to the original network. We provide analytical upper and lower bounds for the

\ell_\infty

-distance between the fully relaxed and original outputs. This distance grows exponentially, w.r.t. the network's depth, and linearly w.r.t. the input's radius. The misclassification probability exhibits a step-like behavior, w.r.t. input radius. Our results are supported by experiments on MNIST, Fashion MNIST and random networks.

Merkouris Papamichail, Konstantinos Varsos, Giorgos Flouris +1

Foundation for Research and Technology – Hellas, Heraklion, Greece · University of Crete, Heraklion, Greece · Catalan Institution for Research and Advanced Studies, Barcelona, Spain +1

Neural Network Verification Certified Robustness Convex Relaxation

Apr 20, 2026

FUSE: Ensembling Verifiers with Zero Labeled Data

Verification of model outputs is rapidly emerging as a key primitive for both training and real-world deployment of large language models (LLMs). In practice, this often involves using imperfect LLM judges and reward models since ground truth acquisition can be time-consuming and expensive. We introduce Fully Unsupervised Score Ensembling (FUSE), a method for improving verification quality by ensembling verifiers without access to ground truth correctness labels. The key idea behind FUSE is to control conditional dependencies between verifiers in a manner that improves the unsupervised performance of a class of spectral algorithms from the ensembling literature. Despite requiring zero ground truth labels, FUSE typically matches or improves upon semi-supervised alternatives in test-time scaling experiments with diverse sets of generator models, verifiers, and benchmarks. In particular, we validate our method on both conventional academic benchmarks such as GPQA Diamond and on frontier, unsaturated benchmarks such as Humanity's Last Exam and IMO Shortlist questions.

Joonhyuk Lee, Virginia Ma, Sarah Zhao +4

Stanford University · Google

Neural Network Verification LLM Evaluation LLM Answer Verification Language Model Ensembles

Apr 15, 2026

Hardware-Efficient Neuro-Symbolic Networks with the Exp-Minus-Log Operator

Deep neural networks (DNNs) deliver state-of-the-art accuracy on regression and classification tasks, yet two structural deficits persistently obstruct their deployment in safety-critical, resource-constrained settings: (i) opacity of the learned function, which precludes formal verification, and (ii) reliance on heterogeneous, library-bound activation functions that inflate latency and silicon area on edge hardware. The recently introduced Exp-Minus-Log (EML) Sheffer operator, eml(x, y) = exp(x) - ln(y), was shown by Odrzywolek (2026) to be sufficient - together with the constant 1 - to express every standard elementary function as a binary tree of identical nodes. We propose to embed EML primitives inside conventional DNN architectures, yielding a hybrid DNN-EML model in which the trunk learns distributed representations and the head is a depth-bounded, weight-sparse EML tree whose snapped weights collapse to closed-form symbolic sub-expressions. We derive the forward equations, prove computational-cost bounds, analyse inference and training acceleration relative to multilayer perceptrons (MLPs) and physics-informed neural networks (PINNs), and quantify the trade-offs for FPGA/analog deployment. We argue that the DNN-EML pairing closes a literature gap: prior neuro-symbolic and equation-learner approaches (EQL, KAN, AI-Feynman) work with heterogeneous primitive sets and do not exploit a single hardware-realisable Sheffer element. A balanced assessment shows that EML is unlikely to accelerate training, and on commodity CPU/GPU it is also unlikely to accelerate inference; however, on a custom EML cell (FPGA logic block or analog circuit) the asymptotic latency advantage can reach an order of magnitude with simultaneous gain in interpretability and formal-verification tractability.

Eymen Ipek

Institute of Automotive Engineering, Graz University of Technology, Austria

Neurosymbolic Learning Efficient Neural Network Inference Neural Network Interpretability FPGA-Based Neural Network Acceleration Neural Network Verification

Apr 13, 2026

Exact Certification of Neural Networks and Partition Aggregation Ensembles against Label Poisoning

Label-flipping attacks, which corrupt training labels to induce misclassifications at inference, remain a major threat to supervised learning models. This drives the need for robustness certificates that provide formal guarantees about a model's robustness under adversarially corrupted labels. Existing certification frameworks rely on ensemble techniques such as smoothing or partition-aggregation, but treat the corresponding base classifiers as black boxes, yielding overly conservative guarantees. We introduce EnsembleCert, the first certification framework for partition-aggregation ensembles that utilizes white-box knowledge of the base classifiers. Concretely, EnsembleCert yields tighter guarantees than black-box approaches by aggregating per-partition white-box certificates to compute ensemble-level guarantees in polynomial time. To extract white-box knowledge from the base classifiers efficiently, we develop ScaLabelCert, a method that leverages the equivalence between sufficiently wide neural networks and kernel methods using the neural tangent kernel. ScaLabelCert yields the first exact, polynomial-time calculable certificate for neural networks against label-flipping attacks. EnsembleCert is either on par, or significantly outperforms the existing partition-based black box certificates. Exemplary, on CIFAR-10, our method can certify upto +26.5% more label flips in median over the test set compared to the existing black-box approach while requiring 100 times fewer partitions, thus, challenging the prevailing notion that heavy partitioning is a necessity for strong certified robustness.

Ajinkya Mohgaonkar, Lukas Gosch, Mahalakshmi Sabanayagam +2

School of Computation, Information and Technology, Technical University of Munich, Germany · Munich Data Science Institute, Technical University of Munich · Munich Center for Machine Learning, Germany +1

Certified Robustness Neural Network Verification Adversarial Attacks Ensemble Learning

Apr 9, 2026

Interval Certifications for Multilayered Perceptrons via Lattice Traversal

In this work we present a rigorous theoretical framework to a foundational problem of AI safety, namely adversarial robustness. In particular, we show that the adversarial robustness problem can be reduced to a lattice traversal problem. Each element of this lattice corresponds to an interval, i.e., an axis-aligned hyper-rectangle, containing an input point

\mathbf{x}

. Consider a multilayered perceptron classifier (MLP). An interval

I

constitutes a sound certification if

\mathbf{x} \in I

and

\mathbf{x}

can be freely perturbed in

I

without changing the MLP's prediction. Complementarily, an interval

I

constitutes a complete certification if

\mathbf{x} \in I

and when

\mathbf{x}

moves outside of

I

the MLP's prediction is guaranteed to change. While the sound certification problem corresponds to the well-studied adversarial robustness, complete certifications have not been examined in the literature. We develop lattice traversal operators, which we apply in a refine & verify iterative scheme. Using formal MLP verifiers, sound maximality and complete minimality are guaranteed. Moreover, we examine objective optimization problems. There we discover some interesting asymmetries. For complete certifications, the minimum solution is obtained in polynomial oracle calls. This does not hold for sound certifications, where we prove strong intractability results. Additionally, we examine optimization problems in symmetric intervals (i.e.,

\ell_\infty

-spheres), where we provide logarithmic algorithms. Finally, we present an empirical evaluation, using the novel ParallelepipedoNN system.

Merkouris Papamichail, Konstantinos Varsos, Giorgos Flouris +1

Foundation for Reasearch and Technology - Hellas, Heraklion, Greece · University of Crete, Heraklion, Greece · Catalan Institution for Research and Advanced Studies, Barcelona, Spain +1

Adversarial Robustness Certified Robustness Neural Network Verification Multilayer Perceptrons

Apr 6, 2026

Analyzing Symbolic Properties for DRL Agents in Systems and Networking

Deep reinforcement learning (DRL) has shown remarkable performance on complex control problems in systems and networking, including adaptive video streaming, wireless resource management, and congestion control. For safe deployment, however, it is critical to reason about how agents behave across the range of system states they encounter in practice. Existing verification-based methods in this domain primarily focus on point properties, defined around fixed input states, which offer limited coverage and require substantial manual effort to identify relevant input-output pairs for analysis. In this paper, we study symbolic properties, that specify expected behavior over ranges of input states, for DRL agents in systems and networking. We present a generic formulation for symbolic properties, with monotonicity and robustness as concrete examples, and show how they can be analyzed using existing DNN verification engines. Our approach encodes symbolic properties as comparisons between related executions of the same policy and decomposes them into practically tractable sub-properties. These techniques serve as practical enablers for applying existing verification tools to symbolic analysis. Using our framework, diffRL, we conduct an extensive empirical study across three DRL-based control systems, adaptive video streaming, wireless resource management, and congestion control. Through these case studies, we analyze symbolic properties over broad input ranges, examine how property satisfaction evolves during training, study the impact of model size on verifiability, and compare multiple verification backends. Our results show that symbolic properties provide substantially broader coverage than point properties and can uncover non-obvious, operationally meaningful counterexamples, while also revealing practical solver trade-offs and limitations.

Mohammad Zangooei, Jannis Weil, Amr Rizk +2

University of Waterloo, Waterloo, Canada · Leibniz University Hannover, Hannover, Germany

Reinforcement Learning Neural Network Verification

Apr 6, 2026

Fine-Tuning Integrity for Modern Neural Networks: Structured Drift Proofs via Norm, Rank, and Sparsity Certificates

Fine-tuning is the dominant paradigm for adapting large machine learning models, yet current deployment pipelines provide no way to verify how a released model was updated. In particular, a model provider or auditor cannot check whether a fine-tuned model adheres to a claimed update procedure without access to its parameters. We introduce fine-tuning integrity (FTI), a cryptographic objective for verifying that a deployed model differs from a trusted base model only within a declared class of admissible updates. We construct succinct model difference proofs (SMDPs), zero-knowledge protocols that certify structured parameter drift without revealing model weights. Our framework supports three fundamental update classes: norm-bounded, low-rank, and sparse drift, covering common fine-tuning methods such as regularized training, LoRA, and prefix tuning. In all cases, proof size and verification cost depend on the structure of the update rather than the number of parameters. We prove soundness, zero-knowledge, and succinctness for each construction, and establish a matching

Ω(n)

lower bound showing that structural assumptions are necessary for succinct verification. A prototype evaluation on synthetic benchmarks and GPT-2 fine-tuning demonstrates that proofs remain compact and verification is efficient at realistic scales.

Zhenhang Shang, Yingzhe Yu, Kani Chen

The Hong Kong University of Science and Technology, Hong Kong, China

Neural Network Verification LLM Auditing Zero-Knowledge Proofs

Apr 5, 2026

Towards Verified and Targeted Explanations through Formal Methods

As deep neural networks are deployed in safety-critical domains such as autonomous driving and medical diagnosis, stakeholders need explanations that are interpretable but also trustworthy with formal guarantees. Existing XAI methods fall short: heuristic attribution techniques (e.g., LIME, Integrated Gradients) highlight influential features but offer no mathematical guarantees about decision boundaries, while formal methods verify robustness yet remain untargeted, analyzing the nearest boundary regardless of whether it represents a critical risk. In safety-critical systems, not all misclassifications carry equal consequences; confusing a "Stop" sign for a "60 kph" sign is far more dangerous than confusing it with a "No Passing" sign. We introduce ViTaX (Verified and Targeted Explanations), a formal XAI framework that generates targeted semifactual explanations with mathematical guarantees. For a given input (class y) and a user-specified critical alternative (class t), ViTaX: (1) identifies the minimal feature subset most sensitive to the y->t transition, and (2) applies formal reachability analysis to guarantee that perturbing these features by epsilon cannot flip the classification to t. We formalize this through Targeted epsilon-Robustness, certifying whether a feature subset remains robust under perturbation toward a specific target class. ViTaX is the first method to provide formally guaranteed explanations of a model's resilience against user-identified alternatives. Evaluations on MNIST, GTSRB, EMNIST, and TaxiNet demonstrate over 30% fidelity improvement with minimal explanation cardinality.

Hanchen David Wang, Diego Manzanas Lopez, Preston K. Robinette +3

Vanderbilt University, Nashville, Tennessee, USA

Explainable Artificial Intelligence Counterfactual Explanations Neural Network Verification

Mar 31, 2026

Empirical Validation of the Classification-Verification Dichotomy for AI Safety Gates

Can classifier-based safety gates maintain reliable oversight as AI systems improve over hundreds of iterations? We provide comprehensive empirical evidence that they cannot. On a self-improving neural controller (d=240), eighteen classifier configurations -- spanning MLPs, SVMs, random forests, k-NN, Bayesian classifiers, and deep networks -- all fail the dual conditions for safe self-improvement. Three safe RL baselines (CPO, Lyapunov, safety shielding) also fail. Results extend to MuJoCo benchmarks (Reacher-v4 d=496, Swimmer-v4 d=1408, HalfCheetah-v4 d=1824). At controlled distribution separations up to delta_s=2.0, all classifiers still fail -- including the NP-optimal test and MLPs with 100% training accuracy -- demonstrating structural impossibility. We then show the impossibility is specific to classification, not to safe self-improvement itself. A Lipschitz ball verifier achieves zero false accepts across dimensions d in {84, 240, 768, 2688, 5760, 9984, 17408} using provable analytical bounds (unconditional delta=0). Ball chaining enables unbounded parameter-space traversal: on MuJoCo Reacher-v4, 10 chains yield +4.31 reward improvement with delta=0; on Qwen2.5-7B-Instruct during LoRA fine-tuning, 42 chain transitions traverse 234x the single-ball radius with zero safety violations across 200 steps. A 50-prompt oracle confirms oracle-agnosticity. Compositional per-group verification enables radii up to 37x larger than full-network balls. At d<=17408, delta=0 is unconditional; at LLM scale, conditional on estimated Lipschitz constants.

Arsenios Scrivens

AI Agent Safety AI Safety Evaluation Runtime Enforcement for AI Agents Self-Improving Agents Neural Network Verification

Mar 30, 2026

Information-Theoretic Limits of Safety Verification for Self-Improving Systems

Can a safety gate permit unbounded beneficial self-modification while maintaining bounded cumulative risk? We formalize this question through dual conditions -- requiring sum delta_n < infinity (bounded risk) and sum TPR_n = infinity (unbounded utility) -- and establish a theory of their (in)compatibility. Classification impossibility (Theorem 1): For power-law risk schedules delta_n = O(n^{-p}) with p > 1, any classifier-based gate under overlapping safe/unsafe distributions satisfies TPR_n <= C_alpha * delta_n^beta via Holder's inequality, forcing sum TPR_n < infinity. This impossibility is exponent-optimal (Theorem 3). A second independent proof via the NP counting method (Theorem 4) yields a 13% tighter bound without Holder's inequality. Universal finite-horizon ceiling (Theorem 5): For any summable risk schedule, the exact maximum achievable classifier utility is U*(N, B) = N * TPR_NP(B/N), growing as exp(O(sqrt(log N))) -- subpolynomial. At N = 10^6 with budget B = 1.0, a classifier extracts at most U* ~ 87 versus a verifier's ~500,000. Verification escape (Theorem 2): A Lipschitz ball verifier achieves delta = 0 with TPR > 0, escaping the impossibility. Formal Lipschitz bounds for pre-LayerNorm transformers under LoRA enable LLM-scale verification. The separation is strict. We validate on GPT-2 (d_LoRA = 147,456): conditional delta = 0 with TPR = 0.352. Comprehensive empirical validation is in the companion paper [D2].

Arsenios Scrivens

LLM Safety Neural Network Verification

Mar 30, 2026

Demystifying Lipschitz verification: positive matrices, negative results

The global Lipschitz constant of a neural network is related to robustness and generalization, yet unlike in many classical models, it is not plainly legible from the parameters. This has motivated sophisticated verification algorithms, especially semidefinite programming (SDP) based on incremental quadratic constraints on the activation functions, to improve on the fast but often loose product of layerwise Lipschitz constants (the trivial bound). We ask why Lipschitz verification is a problem in the first place. Our answer is that the difficulty is structural: estimating a network's Lipschitz constant requires knowing which hidden states are reachable, and reachability is NP-hard. If P!=NP, then reachability is a barrier to any polynomial-time algorithm. Through explicit constructions, we show that this blindness can force SDP-based bounds to inherit the same qualitative failures as the trivial bound, including but not limited to polynomial per-layer conservatism. We show that the difficulties of NP-hard questions are not isolated to worst-case computational reductions, but actually afflict every instance of the verification problem. Thus SDP is not sufficient for Lipschitz verification. We also argue that it is not necessary: several apparent failures of the trivial bound arise from removable parameterization pathologies, and can be mitigated by optimizing or regularizing the trivial bound itself. We demonstrate this claim via a "spherical cow" linear model and numerical proofs of concept. While the main contribution is theoretical and negative, we finally motivate a novel form of trigonometric layers that do not need biases for universal approximation. Combined with trivial bound regularization, they make the trivial bound provably and practically tight.

Simon Kuang, Yuezhu Xu, S. Sivaranjani +1

Department of Mechanical and Aerospace Engineering University of California, Davis · Edwardson School of Industrial Engineering Purdue University

Neural Network Verification Lipschitz Neural Networks Semidefinite Programming

Mar 26, 2026

Distribution and Clusters Approximations as Abstract Domains in Probabilistic Abstract Interpretation to Neural Network Analysis

The probabilistic abstract interpretation framework of neural network analysis analyzes a neural network by analyzing its density distribution flow of all possible inputs. The grids approximation is one of abstract domains the framework uses which abstracts concrete space into grids. In this paper, we introduce two novel approximation methods: distribution approximation and clusters approximation. We show how these two methods work in theory with corresponding abstract transformers with help of illustrations of some simple examples.

Zhuofan Zhang, Herbert Wiklicky

Department of Computing, Imperial College London, London, UK

Abstract Interpretation Neural Network Verification Formal Verification

Mar 26, 2026

Probabilistic Abstract Interpretation on Neural Networks via Grids Approximation

Probabilistic abstract interpretation is a theory used to extract particular properties of a computer program when it is infeasible to test every single inputs. In this paper we apply the theory on neural networks for the same purpose: to analyse density distribution flow of all possible inputs of a neural network when a network has uncountably many or countable but infinitely many inputs. We show how this theoretical framework works in neural networks and then discuss different abstract domains and corresponding Moore-Penrose pseudo-inverses together with abstract transformers used in the framework. We also present experimental examples to show how this framework helps to analyse real world problems.

Zhuofan Zhang, Herbert Wiklicky

Imperial College London, 180 Queen’s Gate, South Kensington, London SW7 2AZ

Neural Network Verification Formal Verification

Mar 25, 2026

The Luna Bound Propagator for Formal Analysis of Neural Networks

The parameterized CROWN analysis, a.k.a., alpha-CROWN has emerged as a practically successful abstract interpretation method for neural network verification. However, existing implementations of alpha-CROWN are limited to Python, which complicates integration into existing DNN verifiers and long-term production-level systems. We introduce Luna, a new abstract-interpretation-based bound propagator implemented in C++. Luna supports Interval Bound Propagation, the DeepPoly/CROWN analysis, and the alpha-CROWN analysis over a general computational graph. We describe the architecture of Luna and show that it outperforms the state-of-the-art alpha-CROWN implementation in terms of both bound tightness and computational efficiency on supported benchmarks from VNN-COMP 2025. Luna is publicly available at https://github.com/ai-ar-research/luna.

Henry LeCates, Haoze Wu

Amherst College, USA

Abstract Interpretation Neural Network Verification Neural Network Robustness

Mar 20, 2026

Hawkeye: Reproducing GPU-Level Non-Determinism

We present Hawkeye, a system for analyzing and reproducing GPU-level arithmetic operations. Using our framework, anyone can re-execute on a CPU the exact matrix multiplication operations underlying a machine learning model training or inference workflow that was executed on an NVIDIA GPU, without any precision loss. This is in stark contrast to prior approaches to verifiable machine learning, which either introduce significant computation overhead to the original model owner, or suffer from non-robustness and quality degradation. The main technical contribution of Hawkeye is a systematic sequence of carefully crafted tests that study rounding direction, subnormal number handling, and order of (non-associative) accumulation during matrix multiplication on NVIDIA's Tensor Cores. We test and evaluate our framework on multiple NVIDIA GPU architectures ( Ampere, Hopper, and Lovelace) and precision types (FP16, BFP16, FP8). In all test cases, Hawkeye enables perfect reproduction of matrix multiplication on a CPU, paving the way for efficient and trustworthy third-party auditing of ML model training and inference. We provide source code for Hawkeye at https://github.com/badasherez/gpu-simulator.

Erez Badash, Dan Boneh, Ilan Komargodski +1

Pearl Research Labs · Department of Computer Science, Stanford University

ML Reproducibility Neural Network Verification

Mar 19, 2026

Towards Verifiable AI with Lightweight Cryptographic Proofs of Inference

When large AI models are deployed as cloud-based services, clients have no guarantee that responses are correct or were produced by the intended model. Rerunning inference locally is infeasible for large models, and existing cryptographic proof systems -- while providing strong correctness guarantees -- introduce prohibitive prover overhead (e.g., hundreds of seconds per query for billion-parameter models). We present a verification framework and protocol that replaces full cryptographic proofs with a lightweight, sampling-based approach grounded in statistical properties of neural networks. We formalize the conditions under which trace separation between functionally dissimilar models can be leveraged to argue the security of verifiable inference protocols. The prover commits to the execution trace of inference via Merkle-tree-based vector commitments and opens only a small number of entries along randomly sampled paths from output to input. This yields a protocol that trades soundness for efficiency, a tradeoff well-suited to auditing, large-scale deployment settings where repeated queries amplify detection probability, and scenarios with rationally incentivized provers who face penalties upon detection. Our approach reduces proving times by several orders of magnitude compared to state-of-the-art cryptographic proof systems, going from the order of minutes to the order of milliseconds, with moderately larger proofs. Experiments on ResNet-18 classifiers and Llama-2-7B confirm that common architectures exhibit the statistical properties our protocol requires, and that natural adversarial strategies (gradient-descent reconstruction, inverse transforms, logit swapping) fail to produce traces that evade detection. We additionally present a protocol in the refereed delegation model, where two competing servers enable correct output identification in a logarithmic number of rounds.

Pranay Anchuri, Matteo Campanelli, Paul Cesaretti +4

Offchain Labs · University of Tartu, Estonia · CUNY Graduate Center +1

Verifiable Outsourced Computation Neural Network Verification Reasoning Verification

Mar 16, 2026

SimCert: Probabilistic Certification for Behavioral Similarity in Deep Neural Network Compression

Deploying Deep Neural Networks (DNNs) on resource-constrained embedded systems requires aggressive model compression techniques like quantization and pruning. However, ensuring that the compressed model preserves the behavioral fidelity of the original design is a critical challenge in the safety-critical system design flow. Existing verification methods often lack scalability or fail to handle the architectural heterogeneity introduced by pruning. In this work, we propose SimCert, a probabilistic certification framework for verifying the behavioral similarity of compressed neural networks. Unlike worst-case analysis, SimCert provides quantitative safety guarantees with adjustable confidence levels. Our framework features: (1) A dual-network symbolic propagation method supporting both quantization and pruning; (2) A variance-aware bounding technique using Bernstein's inequality to tighten safety certificates; and (3) An automated verification toolchain. Experimental results on ACAS Xu and computer vision benchmarks demonstrate that SimCert outperforms state-of-the-art baselines.

Jingyang Li, Fu Song, Guoqiang Li

Shanghai Jiao Tong University, Shanghai 200240, China · Institute of Software, Chinese Academy of Sciences, Beijing 100190, China

Neural Network Verification Neural Network Compression

Mar 12, 2026

Incremental Neural Network Verification via Learned Conflicts

Neural network verification is often used as a core component within larger analysis procedures, which generate sequences of closely related verification queries over the same network. In existing neural network verifiers, each query is typically solved independently, and information learned during previous runs is discarded, leading to repeated exploration of the same infeasible regions of the search space. In this work, we aim to expedite verification by reducing this redundancy. We propose an incremental verification technique that reuses learned conflicts across related verification queries. The technique can be added on top of any branch-and-bound-based neural network verifier. During verification, the verifier records conflicts corresponding to learned infeasible combinations of activation phases, and retains them across runs. We formalize a refinement relation between verification queries and show that conflicts learned for a query remain valid under refinement, enabling sound conflict inheritance. Inherited conflicts are handled using a SAT solver to perform consistency checks and propagation, allowing infeasible subproblems to be detected and pruned early during search. We implement the proposed technique in the Marabou verifier and evaluate it on three verification tasks: local robustness radius determination, verification with input splitting, and minimal sufficient feature set extraction. Our experiments show that incremental conflict reuse reduces verification effort and yields speedups of up to

1.9\times

over a non-incremental baseline.

Raya Elsaleh, Liam Davis, Haoze Wu +1

Hebrew University of Jerusalem, Jerusalem, Israel · Amherst College, Amherst, USA

Neural Network Verification Neural Network Robustness

Mar 12, 2026

Proof-Carrying Materials: Falsifiable Safety Certificates for Machine-Learned Interatomic Potentials

Machine-learned interatomic potentials (MLIPs) are deployed for high-throughput materials screening without formal reliability guarantees. We show that a single MLIP used as a stability filter misses 93% of density functional theory (DFT)-stable materials (recall 0.07) on a 25,000-material benchmark. Proof-Carrying Materials (PCM) closes this gap through three stages: adversarial falsification across compositional space, bootstrap envelope refinement with 95% confidence intervals, and Lean 4 formal certification. Auditing CHGNet, TensorNet and MACE reveals architecture-specific blind spots with near-zero pairwise error correlations (r <= 0.13; n = 5,000), confirmed by independent Quantum ESPRESSO validation (20/20 converged; median DFT/CHGNet force ratio 12x). A risk model trained on PCM-discovered features predicts failures on unseen materials (AUC-ROC = 0.938 +/- 0.004) and transfers across architectures (cross-MLIP AUC-ROC ~ 0.70; feature importance r = 0.877). In a thermoelectric screening case study, PCM-audited protocols discover 62 additional stable materials missed by single-MLIP screening - a 25% improvement in discovery yield.

Abhinaba Basu, Pavan Chakraborty

Indian Institute of Information Technology Allahabad (IIITA), Prayagraj, India · National Institute of Electronics and Information Technology (NIELIT), India

Machine Learning Interatomic Potentials Materials Property Prediction Neural Network Verification

Mar 9, 2026

The FABRIC Strategy for Verifying Neural Feedback Systems

Forward reachability analysis is a dominant approach for verifying reach-avoid specifications in neural feedback systems, i.e., dynamical systems controlled by neural networks, and a number of directions have been proposed and studied. In contrast, far less attention has been given to backward reachability analysis for these systems, in part because of the limited scalability of known techniques. In this work, we begin to address this gap by introducing new algorithms for computing both over- and underapproximations of backward reachable sets for nonlinear neural feedback systems. We also describe and implement an integration of these backward reachability techniques with existing ones for forward analysis. We call the resulting algorithm Forward and Backward Reachability Integration for Certification (FaBRIC). We evaluate our algorithms on a representative set of benchmarks and show that they significantly outperform the prior state of the art.

Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer +1

Department of Aeronautics and Astronautics, Stanford University, Stanford, USA · Department of Computer Science, Stanford University, Stanford, USA

Reachability Analysis Neural Network Verification Feedback Control

Mar 6, 2026

Certified and accurate computation of function space norms of deep neural networks

Neural network methods for PDEs require reliable error control in function space norms. However, trained neural networks can typically only be probed at a finite number of point values. Without strong assumptions, point evaluations alone do not provide enough information to derive tight deterministic and guaranteed bounds on function space norms. In this work, we move beyond a purely black-box setting and exploit the neural network structure directly. We present a framework for the certified and accurate computation of integral quantities of neural networks, including Lebesgue and Sobolev norms, by combining interval arithmetic enclosures on axis-aligned boxes with adaptive marking/refinement and quadrature-based aggregation. On each box, we compute guaranteed lower and upper bounds for function values and derivatives, and propagate these local certificates to global lower and upper bounds for the target integrals. Our analysis provides a general convergence theorem for such certified adaptive quadrature procedures and instantiates it for function values, Jacobians, and Hessians, yielding certified computation of

L^p

,

W^{1,p}

, and

W^{2,p}

norms. We further show how these ingredients lead to practical certified bounds for PINN interior residuals. Numerical experiments illustrate the accuracy and practical behavior of the proposed methods.

Johannes Gründler, Moritz Maibaum, Philipp Petersen

Faculty of Mathematics, University of Vienna, Kolingasse 14–16, 1090 Vienna, Austria

Neural Network Verification Numerical Integration

Mar 6, 2026

Lipschitz-Based Robustness Certification Under Floating-Point Execution

Lipschitz-based robustness certification bounds a network's sensitivity through concrete numerical computation rather than symbolic reasoning, and so scales efficiently. It is increasingly used even where verifiable guarantees matter. Yet, as with most prior work on robustness certification and verification, soundness is typically proved against a semantic model assuming exact real arithmetic. Deployed networks instead execute in floating-point, creating a gap between certified properties and executed behaviour. As motivating evidence, we give counterexamples showing that real arithmetic robustness guarantees can fail under floating-point execution, even for previously verified certifiers. We then develop a formal, compositional theory relating real arithmetic Lipschitz-based sensitivity bounds to floating-point execution under standard rounding-error models for feed-forward ReLU networks. We derive sound conditions for floating-point robustness, including bounds on certificate degradation and sufficient conditions for the absence of overflow. We also give an efficient floating-point Gram iteration algorithm for Lipschitz bounds and prove that it never under-estimates the true norm. Separately, when a model is certified pre-deployment, we show how measuring its actual deviation against a high-precision execution can substantially reduce certificate degradation. We formalise the theory and its soundness, and implement an executable certifier, evaluated across dense networks spanning image, tabular, and many-class classification. To our knowledge, ours is the first method for soundly accounting for floating-point effects in Lipschitz-based robustness certification, and, done efficiently, the first floating-point-sound robustness checking procedure of any kind to certify models' entire test set -- seven those with 500,000 examples -- while retaining enough precision to be practical.

Toby Murray

University of Melbourne, Melbourne, Australia

Neural Network Verification Neural Network Robustness Formal Verification Certified Robustness

Feb 28, 2026

Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solvers

We present an Ising-compatible framework for formal neural-network robustness verification under bounded input perturbations. For piecewise activations (both continuous piecewise-linear and discrete piecewise-constant), the Exact Logarithmic Piecewise Model (Log-PW) provides an exact, sound, and complete formulation with a state-optimal logarithmic encoding, reducing the binary variables per neuron from linear

O(κ)

to information-theoretically minimal logarithmic complexity

O(\lceil \log_2 κ\rceil)

via logarithmic SOS2 (Log-PWL) and SOS1 (Log-PWC) constraints. For general element-wise activations, the Asymptotic Step-Envelope Model (Step-Env) leverages Log-PWC to construct sound, refinable endpoint enclosures. An exact monotonic reduction based on Jordan decomposition further extends this framework to arbitrary non-monotonic activations. We further develop a hybrid Benders solver with output-sensitive iteration bounds, leveraging a Helly-based conflict compression theory to avoid generic exponential cut explosion. In particular, for shallow networks with fixed input dimension, this establishes an unconditionally polynomial Benders iteration complexity in network size. Interval pruning, certificate transfer for pruned networks, and layerwise classical--Ising partitioning further reduce spin requirements. Experiments demonstrate exact certification fidelity for piecewise-linear networks and near-reference accuracy for non-linear activations under compact spin budgets. On MNIST benchmarks, Log-PW halves binary decision spins over One-Hot formulations, while Helly-based cuts achieve up to a

13.41\times

speedup and an

87.6\%

reduction in master queries over standard baselines.

Wenxin Li, Wenchao Liu, Anzhe Jiang +6

Beijing QBoson Quantum Technology Co., Ltd. · Tsinghua University · Beijing Normal University

Neural Network Verification Neural Network Robustness Certified Robustness

Feb 26, 2026

TorchLean: Formalizing Neural Networks in Lean

Neural networks are increasingly deployed in scientific, safety critical, and mission critical pipelines, yet verification and analysis are often performed outside the programming environment that defines and runs the model. This creates a semantic gap between the executed network and the analyzed artifact: guarantees can depend on implicit conventions about operator semantics, tensor layouts, preprocessing, floating-point behavior, graph transformations, accelerated kernels, and external certificates. We present TorchLean, a unified framework for formalizing, executing, and verifying neural networks in Lean 4. TorchLean treats learned models as executable programs and mathematical objects with a shared semantics for computation, verification, and theorem proving. The framework provides a PyTorch style API for typed tensors, layers, objectives, optimizers, automatic differentiation, and graph programs, with eager and compiled execution paths that lower to a common computation-graph representation. TorchLean supports exact and finite-precision tensor semantics, verified reverse-mode differentiation, interval and affine bound propagation, CROWN/LiRPA style certificate checking, import/export workflows, and CUDA-backed execution through explicit FFI boundaries. It also includes semantic layers for attention and FlashAttention, state-space sequence models, diffusion and sampling processes, probability kernels, reinforcement-learning objectives and Markov decision processes, and self-supervised objectives such as masked autoencoding, JEPA-style predictive views, and variance/correlation-based anti-collapse losses. Together, these components provide a semantic foundation for verified machine learning, where executable neural network artifacts, verification procedures, runtime boundaries, and mathematical claims can be stated and related inside one theorem-proving environment.

Robert Joseph George, Jennifer Cruden, Will Adkisson +3

California Institute of Technology · Washington University in St. Louis · University of Illinois Urbana-Champaign

Neural Network Verification

Feb 18, 2026

Exact Certification of Data-Poisoning Attacks Using Mixed-Integer Programming

This work introduces a verification framework that provides both sound and complete guarantees for data poisoning attacks during neural network training. We formulate adversarial data manipulation, model training, and test-time evaluation in a single mixed-integer quadratic programming (MIQCP) problem. Finding the global optimum of the proposed formulation provably yields worst-case poisoning attacks, while simultaneously bounding the effectiveness of all possible attacks on the given training pipeline. Our framework encodes both the gradient-based training dynamics and model evaluation at test time, enabling the first exact certification of training-time robustness. Experimental evaluation on small models confirms that our approach delivers a complete characterization of robustness against data poisoning.

Philip Sosnin, Jodie Knapp, Fraser Kennedy +2

Department of Computing, Imperial College London, United Kingdom · The Alan Turing Institute, United Kingdom

Data Poisoning Attacks Certified Robustness Neural Network Verification

Feb 17, 2026

A Note on Non-Composability of Layerwise Approximate Verification for Neural Inference

A natural and informal approach to verifiable (or zero-knowledge) ML inference over floating-point data is: ``prove that each layer was computed correctly up to tolerance

δ

; therefore the final output is a reasonable inference result''. This short note gives a simple counterexample showing that this inference is false in general: for any neural network, we can construct a functionally equivalent network for which adversarially chosen approximation-magnitude errors in individual layer computations suffice to steer the final output arbitrarily (within a prescribed bounded range).

Or Zamir

Tel Aviv University

Neural Network Verification

Feb 16, 2026

BEACONS: Bounded-Error, Algebraically-Composable Neural Solvers for Partial Differential Equations

The traditional limitations of neural networks in reliably generalizing beyond the convex hulls of their training data present a significant problem for computational physics, in which one often wishes to solve PDEs in regimes far beyond anything which can be experimentally or analytically validated. In this paper, we show how it is possible to circumvent these limitations by constructing formally-verified neural network solvers for PDEs, with rigorous convergence, stability, and conservation properties, whose correctness can therefore be guaranteed even in extrapolatory regimes. By using the method of characteristics to predict the analytical properties of PDE solutions a priori (even in regions arbitrarily far from the training domain), we show how it is possible to construct rigorous extrapolatory bounds on the worst-case L^inf errors of shallow neural network approximations. Then, by decomposing PDE solutions into compositions of simpler functions, we show how it is possible to compose these shallow neural networks together to form deep architectures, based on ideas from compositional deep learning, in which the large L^inf errors in the approximations have been suppressed. The resulting framework, called BEACONS (Bounded-Error, Algebraically-COmposable Neural Solvers), comprises both an automatic code-generator for the neural solvers themselves, as well as a bespoke automated theorem-proving system for producing machine-checkable certificates of correctness. We apply the framework to a variety of linear and non-linear PDEs, including the linear advection and inviscid Burgers' equations, as well as the full compressible Euler equations, in both 1D and 2D, and illustrate how BEACONS architectures are able to extrapolate solutions far beyond the training data in a reliable and bounded way. Various advantages of the approach over the classical PINN approach are discussed.

Jonathan Gorard, Ammar Hakim, James Juno

Princeton University Princeton, NJ 08544, USA · Princeton Plasma Physics Laboratory Princeton, NJ 08540, USA

Neural PDE Solvers Partial Differential Equations Neural Network Generalization Neural Network Verification Neural Network Approximation Theory

Dec 8, 2025

Formalized Hopfield Networks and Boltzmann Machines

Neural networks are widely used, yet their analysis and verification remain challenging. We present a Lean~4 formalization covering both deterministic and stochastic models. We first formalize Hopfield networks -- recurrent networks that store patterns as stable states -- and prove their convergence, and the correctness of Hebbian learning, the rule that updates parameters to encode patterns. We then turn to stochastic networks, whose probabilistic updates converge to a stationary distribution: we formalize the dynamics and learning of Boltzmann machines and prove their ergodicity -- convergence to a unique stationary distribution -- via a new formalization of the Perron--Frobenius theorem.

Matteo Cipollina, Michail Karatarakis, Freek Wiedijk

Axiomatic AI, Barcelona, Spain · Radboud University, Nijmegen, The Netherlands

Neural Network Verification Hopfield Networks

Sep 26, 2025

Parameterized Hardness of Zonotope Containment and Neural Network Verification

Neural networks with ReLU activations are a widely used model in machine learning. It is thus important to have a profound understanding of the properties of the functions computed by such networks. Recently, there has been increasing interest in the (parameterized) computational complexity of determining these properties. In this work, we close several gaps and resolve an open problem posed by Froese et al. [COLT '25] regarding the parameterized complexity of various problems related to network verification. In particular, we prove that, for all

\ell\ge 2

, deciding positivity (and thus surjectivity) of a function

f:\mathbb{R}^d\to\mathbb{R}

computed by an

\ell

-layer ReLU network is W[

\ell-1

]-hard when parameterized by the input dimension

d

. The case

\ell=2

implies that zonotope non-containment (a problem that is of independent interest in computational geometry, control theory, and robotics) is W[1]-hard with respect to the ambient dimension

d

. Moreover, we show that approximating the maximum within any multiplicative factor and computing the

L_p

-Lipschitz constant for

p\in(0,\infty]

in

\ell

-layer networks is NP-hard and W[

\ell-1

]-hard with respect to

d

. For

\ell\ge 3

, approximating the

L_p

-Lipschitz constant is NP- and W[

\ell-2

]-hard. We further show that the above problems are NP- and W[

t

]-hard (for all

t\ge 1

) with respect to

\ell

for constant

d

. Notably, our hardness results imply that the naive enumeration-based methods for these fundamental problems running in

n^{(\ell-1) d}\cdot\operatorname{poly}(N)

time are all essentially optimal under the Exponential Time Hypothesis.

Vincent Froese, Moritz Grillo, Christoph Hertrich +1

Technische Universität Berlin · Max Planck Institute for Mathematics in the Sciences · University of Technology Nuremberg

Neural Network Verification Parameterized Complexity