# Algorithms for Verifying Deep Neural Networks

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

## Key facts

- Cited by 221 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Mar 2019.

## Built on by (most cited first, 30 of 221)

- [Safety-Enhanced Autonomous Driving Using Interpretable Sensor Fusion Transformer](https://mlsanity.com/paper/2207.14024/) (2022)
- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Safety and Liveness Guarantees through Reach-Avoid Reinforcement Learning](https://mlsanity.com/paper/2112.12288/) (2021)
- [Logic-Based Explainability in Machine Learning](https://mlsanity.com/paper/2211.00541/) (2022)
- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems](https://mlsanity.com/paper/2108.01220/) (2021)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [Inspect, Understand, Overcome: A Survey of Practical Methods for AI Safety](https://mlsanity.com/paper/2104.14235/) (2021)
- [HardNet: Hard-Constrained Neural Networks with Universal Approximation Guarantees](https://mlsanity.com/paper/2410.10807/) (2024)
- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [Efficient Neural Network Analysis with Sum-of-Infeasibilities](https://mlsanity.com/paper/2203.11201/) (2022)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [Safe Control with Neural Network Dynamic Models](https://mlsanity.com/paper/2110.01110/) (2021)
- [Double Sampling Randomized Smoothing](https://mlsanity.com/paper/2206.07912/) (2022)
- [Pruning and Slicing Neural Networks using Formal Verification](https://mlsanity.com/paper/2105.13649/) (2021)
- [Physics guided neural networks for modelling of non-linear dynamics](https://mlsanity.com/paper/2205.06858/) (2022)
- [DiffSmooth: Certifiably Robust Learning via Diffusion Models and Local Smoothing](https://mlsanity.com/paper/2308.14333/) (2023)
- [Scaling Up Exact Neural Network Compression by ReLU Stability](https://mlsanity.com/paper/2102.07804/) (2021)
- [POLICE: Provably Optimal Linear Constraint Enforcement for Deep Neural Networks](https://mlsanity.com/paper/2211.01340/) (2022)
- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)

## Abstract (arXiv)

Deep neural networks are widely used for nonlinear function approximation with applications ranging from computer vision to control. Although these networks involve the composition of simple arithmetic operations, it can be very challenging to verify whether a particular network satisfies certain input-output properties. This article surveys methods that have emerged recently for soundly verifying such properties. These methods borrow insights from reachability analysis, optimization, and search. We discuss fundamental differences and connections between existing algorithms. In addition, we provide pedagogical implementations of existing methods and compare them on a set of benchmark problems.