# Reachability Analysis of Deep Neural Networks with Provable Guarantees

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

## Key facts

- Cited by 93 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 May 2018.

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

- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [Building Guardrails for Large Language Models](https://mlsanity.com/paper/2402.01822/) (2024)
- [On Guaranteed Optimal Robust Explanations for NLP Models](https://mlsanity.com/paper/2105.03640/) (2021)
- [A Simple Approach to Improve Single-Model Deep Uncertainty via Distance-Awareness](https://mlsanity.com/paper/2205.00403/) (2022)
- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [A review on data-driven constitutive laws for solids](https://mlsanity.com/paper/2405.03658/) (2024)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [Training robust and generalizable quantum models](https://mlsanity.com/paper/2311.11871/) (2023)
- [PRoA: A Probabilistic Robustness Assessment against Functional Perturbations](https://mlsanity.com/paper/2207.02036/) (2022)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [A Survey on AI Assurance](https://mlsanity.com/paper/2111.07505/) (2021)
- [Attack as Defense: Characterizing Adversarial Examples using Robustness](https://mlsanity.com/paper/2103.07633/) (2021)
- [Minimal Multi-Layer Modifications of Deep Neural Networks](https://mlsanity.com/paper/2110.09929/) (2021)
- [On Recurrent Neural Networks for learning-based control: recent results and ideas for future developments](https://mlsanity.com/paper/2111.13557/) (2021)
- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)
- [From Robustness to Explainability and Back Again](https://mlsanity.com/paper/2306.03048/) (2023)
- [Infinite Time Horizon Safety of Bayesian Neural Networks](https://mlsanity.com/paper/2111.03165/) (2021)
- [Reachability Analysis of a General Class of Neural Ordinary Differential Equations](https://mlsanity.com/paper/2207.06531/) (2022)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/2304.01218/) (2023)
- [Sparse Adversarial Video Attacks with Spatial Transformations](https://mlsanity.com/paper/2111.05468/) (2021)
- [On the Impact of Hard Adversarial Instances on Overfitting in Adversarial Training](https://mlsanity.com/paper/2112.07324/) (2021)
- [Curriculum Learning for Safe Mapless Navigation](https://mlsanity.com/paper/2112.12490/) (2021)
- [Towards Verifying the Geometric Robustness of Large-scale Neural Networks](https://mlsanity.com/paper/2301.12456/) (2023)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [A Survey on Verification and Validation, Testing and Evaluations of Neurosymbolic Artificial Intelligence](https://mlsanity.com/paper/2401.03188/) (2024)
- [ProTIP: Probabilistic Robustness Verification on Text-to-Image Diffusion Models against Stochastic Perturbation](https://mlsanity.com/paper/2402.15429/) (2024)
- [Embodied Foundation Models at the Edge: A Survey of Deployment Constraints and Mitigation Strategies](https://mlsanity.com/paper/2603.16952/) (2026)

## Abstract (arXiv)

Verifying correctness of deep neural networks (DNNs) is challenging. We study a generic reachability problem for feed-forward DNNs which, for a given set of inputs to the network and a Lipschitz-continuous function over its outputs, computes the lower and upper bound on the function values. Because the network and the function are Lipschitz continuous, all values in the interval between the lower and upper bound are reachable. We show how to obtain the safety verification problem, the output range analysis problem and a robustness measure by instantiating the reachability problem. We present a novel algorithm based on adaptive nested optimisation to solve the reachability problem. The technique has been implemented and evaluated on a range of DNNs, demonstrating its efficiency, scalability and ability to handle a broader class of networks than state-of-the-art verification approaches.