# Introduction to Neural Network Verification

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

## Key facts

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

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

- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [HardNet: Hard-Constrained Neural Networks with Universal Approximation Guarantees](https://mlsanity.com/paper/2410.10807/) (2024)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Double Sampling Randomized Smoothing](https://mlsanity.com/paper/2206.07912/) (2022)
- [Certifying Robustness to Programmable Data Bias in Decision Trees](https://mlsanity.com/paper/2110.04363/) (2021)
- [Neuro-Symbolic Verification of Deep Neural Networks](https://mlsanity.com/paper/2203.00938/) (2022)
- [A Quantitative Geometric Approach to Neural-Network Smoothness](https://mlsanity.com/paper/2203.01212/) (2022)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [Incremental Verification of Neural Networks](https://mlsanity.com/paper/2304.01874/) (2023)
- [Mask in the Mirror: Implicit Sparsification](https://mlsanity.com/paper/2408.09966/) (2024)
- [Systems Security Foundations for Agentic Computing](https://mlsanity.com/paper/2512.01295/) (2025)
- [Certifiable 3D Object Pose Estimation: Foundations, Learning Models, and Self-Training](https://mlsanity.com/paper/2206.11215/) (2022)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [How should AI decisions be explained? Requirements for Explanations from the Perspective of European Law](https://mlsanity.com/paper/2404.12762/) (2024)
- [On Neural Network Equivalence Checking using SMT Solvers](https://mlsanity.com/paper/2203.11629/) (2022)
- [Safe Neurosymbolic Learning with Differentiable Symbolic Execution](https://mlsanity.com/paper/2203.07671/) (2022)
- [Neural Interactive Proofs](https://mlsanity.com/paper/2412.08897/) (2024)
- [Provable Fairness for Neural Network Models using Formal Verification](https://mlsanity.com/paper/2212.08578/) (2022)
- [Value Functions are Control Barrier Functions: Verification of Safe Policies using Control Theory](https://mlsanity.com/paper/2306.04026/) (2023)
- [When to Trust AI: Advances and Challenges for Certification of Neural Networks](https://mlsanity.com/paper/2309.11196/) (2023)
- [No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks](https://mlsanity.com/paper/2506.01054/) (2025)
- [Sonar-based Deep Learning in Underwater Robotics: Overview, Robustness and Challenges](https://mlsanity.com/paper/2412.11840/) (2024)
- [Beyond Benchmarks: On The False Promise of AI Regulation](https://mlsanity.com/paper/2501.15693/) (2025)
- [Faster Verified Explanations for Neural Networks](https://mlsanity.com/paper/2512.00164/) (2025)
- [Verifiable Obstacle Detection](https://mlsanity.com/paper/2208.14403/) (2022)
- [Reliability Assurance for Deep Neural Network Architectures Against Numerical Defects](https://mlsanity.com/paper/2302.06086/) (2023)
- [DelBugV: Delta-Debugging Neural Network Verifiers](https://mlsanity.com/paper/2305.18558/) (2023)
- [Detecting Violations of Differential Privacy for Quantum Algorithms](https://mlsanity.com/paper/2309.04819/) (2023)
- [CEG4N: Counter-Example Guided Neural Network Quantization Refinement](https://mlsanity.com/paper/2207.04231/) (2022)

## Abstract (arXiv)

Deep learning has transformed the way we think of software and what it can do. But deep neural networks are fragile and their behaviors are often surprising. In many settings, we need to provide formal guarantees on the safety, security, correctness, or robustness of neural networks. This book covers foundational ideas from formal verification and their adaptation to reasoning about neural networks and deep learning.