# Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 62 references that are in the map.
- First posted on arXiv 10 Feb 2023.

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

- [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)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [A Statistical Approach to Assessing Neural Network Robustness](https://mlsanity.com/paper/1811.07209/) (2018)
- [Feature-Guided Black-Box Safety Testing of Deep Neural Networks](https://mlsanity.com/paper/1710.07859/) (2017)
- [Causality-based Neural Network Repair](https://mlsanity.com/paper/2204.09274/) (2022)
- [Probabilistic Safety for Bayesian Neural Networks](https://mlsanity.com/paper/2004.10281/) (2020)
- [Provable Repair of Deep Neural Networks](https://mlsanity.com/paper/2104.04413/) (2021)
- [Robustness of Neural Networks: A Probabilistic and Practical Approach](https://mlsanity.com/paper/1902.05983/) (2019)
- [Statistical Guarantees for the Robustness of Bayesian Neural Networks](https://mlsanity.com/paper/1903.01980/) (2019)
- [A Game-Based Approximate Verification of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1807.03571/) (2018)
- [Scalable Quantitative Verification For Deep Neural Networks](https://mlsanity.com/paper/2002.06864/) (2020)
- [DeepAbstract: Neural Network Abstraction for Accelerating Verification](https://mlsanity.com/paper/2006.13735/) (2020)
- [Improving Neural Network Verification through Spurious Region Guided Refinement](https://mlsanity.com/paper/2010.07722/) (2020)
- [Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification](https://mlsanity.com/paper/1902.09866/) (2019)
- [NNrepair: Constraint-based Repair of Neural Network Classifiers](https://mlsanity.com/paper/2103.12535/) (2021)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks](https://mlsanity.com/paper/1907.10662/) (2019)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)

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

- [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)

## Abstract (arXiv)

Constraint solving is an elementary way for verification of deep neural networks (DNN). In the domain of AI safety, a DNN might be modified in its structure and parameters for its repair or attack. For such situations, we propose the incremental DNN verification problem, which asks whether a safety property still holds after the DNN is modified. To solve the problem, we present an incremental satisfiability modulo theory (SMT) algorithm based on the Reluplex framework. We simulate the most important features of the configurations that infers the verification result of the searching branches in the old solving procedure (with respect to the original network), and heuristically check whether the proofs are still valid for the modified DNN. We implement our algorithm as an incremental solver called DeepInc, and exerimental results show that DeepInc is more efficient in most cases. For the cases that the property holds both before and after modification, the acceleration can be faster by several orders of magnitude, showing that DeepInc is outstanding in incrementally searching for counterexamples. Moreover, based on the framework, we propose the multi-objective DNN repair problem and give an algorithm based on our incremental SMT solving algorithm. Our repair method preserves more potential safety properties on the repaired DNNs compared with state-of-the-art.