# Incremental Verification of Neural Networks

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

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- Builds on 39 of its 77 references that are in the map.
- First posted on arXiv 4 Apr 2023.

## Builds on (most cited first, 30 of 39)

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Optuna: A Next-generation Hyperparameter Optimization Framework](https://mlsanity.com/paper/1907.10902/) (2019)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [A Survey of Quantization Methods for Efficient Neural Network Inference](https://mlsanity.com/paper/2103.13630/) (2021)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [What is the State of Neural Network Pruning?](https://mlsanity.com/paper/2003.03033/) (2020)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Convolutional Neural Networks for Medical Image Analysis: Full Training or Fine Tuning?](https://mlsanity.com/paper/1706.00712/) (2017)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Robust Out-of-distribution Detection for Neural Networks](https://mlsanity.com/paper/2003.09711/) (2020)
- [Neural Network Branching for Neural Network Verification](https://mlsanity.com/paper/1912.01329/) (2019)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Output Range Analysis for Deep Neural Networks](https://mlsanity.com/paper/1709.09130/) (2017)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [Attribute-Guided Adversarial Training for Robustness to Natural Perturbations](https://mlsanity.com/paper/2012.01806/) (2020)
- [NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation](https://mlsanity.com/paper/2009.09943/) (2020)
- [Fast Geometric Projections for Local Robustness Certification](https://mlsanity.com/paper/2002.04742/) (2020)

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

- [Incremental Randomized Smoothing Certification](https://mlsanity.com/paper/2305.19521/) (2023)
- [Is The Watermarking Of LLM-Generated Code Robust?](https://mlsanity.com/paper/2403.17983/) (2024)
- [Faster Verified Explanations for Neural Networks](https://mlsanity.com/paper/2512.00164/) (2025)
- [Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification](https://mlsanity.com/paper/2505.00963/) (2025)
- [BEAVER: An Efficient Deterministic LLM Verifier](https://mlsanity.com/paper/2512.05439/) (2025)
- [Incremental Neural Network Verification via Learned Conflicts](https://mlsanity.com/paper/2603.12232/) (2026)
- [ARQ: A Mixed-Precision Quantization Framework for Accurate and Certifiably Robust DNNs](https://mlsanity.com/paper/2410.24214/) (2024)
- [Mini-Batch Robustness Verification of Deep Neural Networks](https://mlsanity.com/paper/2508.15454/) (2025)
- [Support is All You Need for Certified VAE Training](https://mlsanity.com/paper/2504.11831/) (2025)
- [MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression](https://mlsanity.com/paper/2506.04268/) (2025)
- [Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees](https://mlsanity.com/paper/2507.17453/) (2025)
- [Branch and Bound for Relational Verification of Neural Networks](https://mlsanity.com/paper/2608.13118/) (2026)
- [Uncovering the Limits of Proof Sharing for Neural Networks](https://mlsanity.com/paper/2608.19351/) (2026)
- [Exploring Solver-Level Warmstarting for Neural Network Verification](https://mlsanity.com/paper/2609.25962/) (2026)

## Abstract (arXiv)

Complete verification of deep neural networks (DNNs) can exactly determine whether the DNN satisfies a desired trustworthy property (e.g., robustness, fairness) on an infinite set of inputs or not. Despite the tremendous progress to improve the scalability of complete verifiers over the years on individual DNNs, they are inherently inefficient when a deployed DNN is updated to improve its inference speed or accuracy. The inefficiency is because the expensive verifier needs to be run from scratch on the updated DNN. To improve efficiency, we propose a new, general framework for incremental and complete DNN verification based on the design of novel theory, data structure, and algorithms. Our contributions implemented in a tool named IVAN yield an overall geometric mean speedup of 2.4x for verifying challenging MNIST and CIFAR10 classifiers and a geometric mean speedup of 3.8x for the ACAS-XU classifiers over the state-of-the-art baselines.