# A DPLL(T) Framework for Verifying Deep Neural Networks

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

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- Builds on 38 of its 109 references that are in the map.
- First posted on arXiv 17 Jul 2023.

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

- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [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)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Adversarial Attacks on Neural Networks for Graph Data](https://mlsanity.com/paper/1805.07984/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [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)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [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)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Natural Attack for Pre-trained Models of Code](https://mlsanity.com/paper/2201.08698/) (2022)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [CoroNet: A deep neural network for detection and diagnosis of COVID-19 from chest x-ray images](https://mlsanity.com/paper/2004.04931/) (2020)
- [Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability](https://mlsanity.com/paper/1809.03008/) (2018)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [Parallelization Techniques for Verifying Neural Networks](https://mlsanity.com/paper/2004.08440/) (2020)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [An Analysis of ISO 26262: Using Machine Learning Safely in Automotive Software](https://mlsanity.com/paper/1709.02435/) (2017)

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

- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [Out of the Shadows: Exploring a Latent Space for Neural Network Verification](https://mlsanity.com/paper/2505.17854/) (2025)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [Exact Certification of Data-Poisoning Attacks Using Mixed-Integer Programming](https://mlsanity.com/paper/2602.16944/) (2026)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Probabilistic Robustness Analysis in High Dimensional Space: Application to Semantic Segmentation Network](https://mlsanity.com/paper/2509.11838/) (2025)
- [IoUCert: Robustness Verification for Anchor-based Object Detectors](https://mlsanity.com/paper/2603.03043/) (2026)
- [ZonoGPT: Towards An Abstract Domain for Verifying Large GPT Models](https://mlsanity.com/paper/2609.34457/) (2026)
- [A Guide to Failure in Machine Learning: Reliability and Robustness from Foundations to Practice](https://mlsanity.com/paper/2503.00563/) (2025)
- [BoxRL-NNV: Boxed Refinement of Latin Hypercube Samples for Neural Network Verification](https://mlsanity.com/paper/2504.03650/) (2025)
- [Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees](https://mlsanity.com/paper/2507.17453/) (2025)
- [Influence-Guided Concolic Testing of Transformer Robustness](https://mlsanity.com/paper/2509.23806/) (2025)
- [E-Globe: Scalable ε-Global Verification of Neural Networks via Tight Upper Bounds and Pattern-Aware Branching](https://mlsanity.com/paper/2602.05068/) (2026)
- [Lipschitz-Based Robustness Certification Under Floating-Point Execution](https://mlsanity.com/paper/2603.13334/) (2026)
- [Stress-Testing Neural Network Verifiers with Provably Robust Instances](https://mlsanity.com/paper/2605.17153/) (2026)
- [Repurposing CLIP to Localize at Pixel Level](https://mlsanity.com/paper/2607.05253/) (2026)
- [Trustworthy Machine Learning through the Lens of Combinatorial Optimization: Survey and Research Perspectives](https://mlsanity.com/paper/2607.07762/) (2026)
- [A Survey on the Verification of Reinforcement Learning Policies](https://mlsanity.com/paper/2607.16210/) (2026)
- [Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees](https://mlsanity.com/paper/2608.17070/) (2026)
- [NNV3: Expanding Neural Network Verification to New Architectures and Domains](https://mlsanity.com/paper/2609.30050/) (2026)
- [Verifying Neural Networks with Reinforcement Learning](https://mlsanity.com/paper/2609.34553/) (2026)
- [CLAD: Constrained Abstract Domain for Neural Network Verification](https://mlsanity.com/paper/2609.34628/) (2026)
- [Neural Network Verification for Deep Joint Source-Channel Coding](https://mlsanity.com/paper/2610.11994/) (2026)

## Abstract (arXiv)

Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, like human-written software, DNNs can have bugs and can be attacked. To address this, research has explored a wide-range of algorithmic approaches to verify DNN behavior. In this work, we introduce NeuralSAT, a new verification approach that adapts the widely-used DPLL(T) algorithm used in modern SMT solvers. A key feature of SMT solvers is the use of conflict clause learning and search restart to scale verification. Unlike prior DNN verification approaches, NeuralSAT combines an abstraction-based deductive theory solver with clause learning and an evaluation clearly demonstrates the benefits of the approach on a set of challenging verification benchmarks.