# ReluDiff: Differential Verification of Deep Neural Networks

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

## Key facts

- Cited by 29 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Jan 2020.

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

- [DeepPayload: Black-box Backdoor Attack on Deep Learning Models through Neural Payload Injection](https://mlsanity.com/paper/2101.06896/) (2021)
- [Fairify: Fairness Verification of Neural Networks](https://mlsanity.com/paper/2212.06140/) (2022)
- [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)
- [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)
- [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)
- [Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning](https://mlsanity.com/paper/2104.10219/) (2021)
- [Relational DNN Verification With Cross Executional Bound Refinement](https://mlsanity.com/paper/2405.10143/) (2024)
- [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)
- [ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs](https://mlsanity.com/paper/2106.05325/) (2021)
- [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)
- [VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification](https://mlsanity.com/paper/2605.07451/) (2026)
- [Understanding the Complexity and Its Impact on Testing in ML-Enabled Systems](https://mlsanity.com/paper/2301.03837/) (2023)
- [Verifying Global Neural Network Specifications using Hyperproperties](https://mlsanity.com/paper/2306.12495/) (2023)
- [Patch Synthesis for Property Repair of Deep Neural Networks](https://mlsanity.com/paper/2404.01642/) (2024)
- [Formal Local Implication Between Two Neural Networks](https://mlsanity.com/paper/2409.16726/) (2024)
- [Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision](https://mlsanity.com/paper/2507.22760/) (2025)
- [Lipschitz-Based Robustness Certification Under Floating-Point Execution](https://mlsanity.com/paper/2603.13334/) (2026)
- [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 deep neural networks are increasingly being deployed in practice, their efficiency has become an important issue. While there are compression techniques for reducing the network's size, energy consumption and computational requirement, they only demonstrate empirically that there is no loss of accuracy, but lack formal guarantees of the compressed network, e.g., in the presence of adversarial examples. Existing verification techniques such as Reluplex, ReluVal, and DeepPoly provide formal guarantees, but they are designed for analyzing a single network instead of the relationship between two networks. To fill the gap, we develop a new method for differential verification of two closely related networks. Our method consists of a fast but approximate forward interval analysis pass followed by a backward pass that iteratively refines the approximation until the desired property is verified. We have two main innovations. During the forward pass, we exploit structural and behavioral similarities of the two networks to more accurately bound the difference between the output neurons of the two networks. Then in the backward pass, we leverage the gradient differences to more accurately compute the most beneficial refinement. Our experiments show that, compared to state-of-the-art verification tools, our method can achieve orders-of-magnitude speedup and prove many more properties than existing tools.