# Safety Verification of Deep Neural Networks

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

## Key facts

- Cited by 263 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Oct 2016.

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

- [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)
- [Orthogonalizing Convolutional Layers with the Cayley Transform](https://mlsanity.com/paper/2104.07167/) (2021)
- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [Explainability of deep vision-based autonomous driving systems: Review and challenges](https://mlsanity.com/paper/2101.05307/) (2021)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Software Engineering for AI-Based Systems: A Survey](https://mlsanity.com/paper/2105.01984/) (2021)
- [How Deep Learning Sees the World: A Survey on Adversarial Attacks & Defenses](https://mlsanity.com/paper/2305.10862/) (2023)
- [Building Guardrails for Large Language Models](https://mlsanity.com/paper/2402.01822/) (2024)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Guidance on the Assurance of Machine Learning in Autonomous Systems (AMLAS)](https://mlsanity.com/paper/2102.01564/) (2021)
- [Provable Repair of Deep Neural Networks](https://mlsanity.com/paper/2104.04413/) (2021)
- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [Robust Machine Learning Systems: Challenges, Current Trends, Perspectives, and the Road Ahead](https://mlsanity.com/paper/2101.02559/) (2021)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review](https://mlsanity.com/paper/2107.12045/) (2021)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [A review on data-driven constitutive laws for solids](https://mlsanity.com/paper/2405.03658/) (2024)
- [Towards Robust and Secure Embodied AI: A Survey on Vulnerabilities and Attacks](https://mlsanity.com/paper/2502.13175/) (2025)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Deep Learning-Based Autonomous Driving Systems: A Survey of Attacks and Defenses](https://mlsanity.com/paper/2104.01789/) (2021)
- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [Low Curvature Activations Reduce Overfitting in Adversarial Training](https://mlsanity.com/paper/2102.07861/) (2021)
- [Towards quantum enhanced adversarial robustness in machine learning](https://mlsanity.com/paper/2306.12688/) (2023)
- [The Role of Explainability in Assuring Safety of Machine Learning in Healthcare](https://mlsanity.com/paper/2109.00520/) (2021)
- [Taxonomy of Machine Learning Safety: A Survey and Primer](https://mlsanity.com/paper/2106.04823/) (2021)
- [Efficient Certified Defenses Against Patch Attacks on Image Classifiers](https://mlsanity.com/paper/2102.04154/) (2021)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)

## Abstract (arXiv)

Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the network to misclassify it. With potential applications including perception modules and end-to-end controllers for self-driving cars, this raises concerns about their safety. We develop a novel automated verification framework for feed-forward multi-layer neural networks based on Satisfiability Modulo Theory (SMT). We focus on safety of image classification decisions with respect to image manipulations, such as scratches or changes to camera angle or lighting conditions that would result in the same class being assigned by a human, and define safety for an individual decision in terms of invariance of the classification within a small neighbourhood of the original image. We enable exhaustive search of the region by employing discretisation, and propagate the analysis layer by layer. Our method works directly with the network code and, in contrast to existing methods, can guarantee that adversarial examples, if they exist, are found for the given region and family of manipulations. If found, adversarial examples can be shown to human testers and/or used to fine-tune the network. We implement the techniques using Z3 and evaluate them on state-of-the-art networks, including regularised and deep learning networks. We also compare against existing techniques to search for adversarial examples and estimate network robustness.