# NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation

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

## Key facts

- Cited by 22 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Sep 2020.

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

- [Incremental Verification of Neural Networks](https://mlsanity.com/paper/2304.01874/) (2023)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Shared Certificates for Neural Network Verification](https://mlsanity.com/paper/2109.00542/) (2021)
- [LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions](https://mlsanity.com/paper/2201.13351/) (2022)
- [QEBVerif: Quantization Error Bound Verification of Neural Networks](https://mlsanity.com/paper/2212.02781/) (2022)
- [Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks](https://mlsanity.com/paper/2208.09872/) (2022)
- [Certifying the Fairness of KNN in the Presence of Dataset Bias](https://mlsanity.com/paper/2307.08722/) (2023)
- [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)
- [Optimized Symbolic Interval Propagation for Neural Network Verification](https://mlsanity.com/paper/2212.08567/) (2022)
- [FairQuant: Certifying and Quantifying Fairness of Deep Neural Networks](https://mlsanity.com/paper/2409.03220/) (2024)
- [Revisiting Differential Verification: Equivalence Verification with Confidence](https://mlsanity.com/paper/2410.20207/) (2024)
- [Reliability Assurance for Deep Neural Network Architectures Against Numerical Defects](https://mlsanity.com/paper/2302.06086/) (2023)
- [Finding Deviated Behaviors of the Compressed DNN Models for Image Classifications](https://mlsanity.com/paper/2112.02819/) (2021)
- [Systematic Testing of the Data-Poisoning Robustness of KNN](https://mlsanity.com/paper/2307.08288/) (2023)
- [SimCert: Probabilistic Certification for Behavioral Similarity in Deep Neural Network Compression](https://mlsanity.com/paper/2603.14818/) (2026)
- [Understanding the Complexity and Its Impact on Testing in ML-Enabled Systems](https://mlsanity.com/paper/2301.03837/) (2023)
- [Formal Local Implication Between Two Neural Networks](https://mlsanity.com/paper/2409.16726/) (2024)
- [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)

As neural networks make their way into safety-critical systems, where misbehavior can lead to catastrophes, there is a growing interest in certifying the equivalence of two structurally similar neural networks. For example, compression techniques are often used in practice for deploying trained neural networks on computationally- and energy-constrained devices, which raises the question of how faithfully the compressed network mimics the original network. Unfortunately, existing methods either focus on verifying a single network or rely on loose approximations to prove the equivalence of two networks. Due to overly conservative approximation, differential verification lacks scalability in terms of both accuracy and computational cost. To overcome these problems, we propose NeuroDiff, a symbolic and fine-grained approximation technique that drastically increases the accuracy of differential verification while achieving many orders-of-magnitude speedup. NeuroDiff has two key contributions. The first one is new convex approximations that more accurately bound the difference neurons of two networks under all possible inputs. The second one is judicious use of symbolic variables to represent neurons whose difference bounds have accumulated significant error. We also find that these two techniques are complementary, i.e., when combined, the benefit is greater than the sum of their individual benefits. We have evaluated NeuroDiff on a variety of differential verification tasks. Our results show that NeuroDiff is up to 1000X faster and 5X more accurate than the state-of-the-art tool.