# Revisiting Differential Verification: Equivalence Verification with Confidence

arXiv: https://arxiv.org/abs/2410.20207 · HTML: https://mlsanity.com/paper/2410.20207/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 53 references that are in the map.
- First posted on arXiv 26 Oct 2024.

## Builds on (most cited first, 25 of 25)

- [On Calibration of Modern Neural Networks](https://mlsanity.com/paper/1706.04599/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Fast inference of deep neural networks in FPGAs for particle physics](https://mlsanity.com/paper/1804.06913/) (2018)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation](https://mlsanity.com/paper/2009.09943/) (2020)
- [Two Sides of Miscalibration: Identifying Over and Under-Confidence Prediction for Network Calibration](https://mlsanity.com/paper/2308.03172/) (2023)
- [Towards Reliable Neural Specifications](https://mlsanity.com/paper/2210.16114/) (2022)
- [On Neural Network Equivalence Checking using SMT Solvers](https://mlsanity.com/paper/2203.11629/) (2022)
- [QEBVerif: Quantization Error Bound Verification of Neural Networks](https://mlsanity.com/paper/2212.02781/) (2022)
- [Verifying Global Two-Safety Properties in Neural Networks with Confidence](https://mlsanity.com/paper/2405.14400/) (2024)
- [Geometric Path Enumeration for Equivalence Verification of Neural Networks](https://mlsanity.com/paper/2112.06582/) (2021)
- [Relational DNN Verification With Cross Executional Bound Refinement](https://mlsanity.com/paper/2405.10143/) (2024)

## Built on by (most cited first, 4 of 4)

- [TrainVerify: Equivalence-Based Verification for Distributed LLM Training](https://mlsanity.com/paper/2506.15961/) (2025)
- [Encrypted Neural Networks without Overflows](https://mlsanity.com/paper/2605.23096/) (2026)
- [Branch and Bound for Relational Verification of Neural Networks](https://mlsanity.com/paper/2608.13118/) (2026)
- [Reference-Tail Trust:Certified Probability Floors for Learned Updates Inside a Deployed Network](https://mlsanity.com/paper/2609.34904/) (2026)

## Abstract (arXiv)

When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To this end, our paper revisits the idea of differential verification which performs reasoning on differences between NNs: On the one hand, our paper proposes a novel abstract domain for differential verification admitting more efficient reasoning about equivalence. On the other hand, we investigate empirically and theoretically which equivalence properties are (not) efficiently solved using differential reasoning. Based on the gained insights, and following a recent line of work on confidence-based verification, we propose a novel equivalence property that is amenable to Differential Verification while providing guarantees for large parts of the input space instead of small-scale guarantees constructed w.r.t. predetermined input points. We implement our approach in a new tool called VeryDiff and perform an extensive evaluation on numerous old and new benchmark families, including new pruned NNs for particle jet classification in the context of CERN's LHC where we observe median speedups >300x over the State-of-the-Art verifier alpha,beta-CROWN.