# Vertex-based reachability analysis for verifying ReLU deep neural networks

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

## Key facts

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

## Builds on (most cited first, 17 of 17)

- [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)
- [Ensemble Adversarial Training: Attacks and Defenses](https://mlsanity.com/paper/1705.07204/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [PixelDefend: Leveraging Generative Models to Understand and Defend against Adversarial Examples](https://mlsanity.com/paper/1710.10766/) (2017)
- [On Detecting Adversarial Perturbations](https://mlsanity.com/paper/1702.04267/) (2017)
- [On the (Statistical) Detection of Adversarial Examples](https://mlsanity.com/paper/1702.06280/) (2017)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [SafetyNet: Detecting and Rejecting Adversarial Examples Robustly](https://mlsanity.com/paper/1704.00103/) (2017)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations](https://mlsanity.com/paper/1712.08163/) (2017)
- [Efficient edge-skeleton computation for polytopes defined by oracles](https://mlsanity.com/paper/1412.3987/) (2014)

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

- [Causal Explanations from the Geometric Properties of ReLU Neural Networks](https://mlsanity.com/paper/2605.10396/) (2026)

## Abstract (arXiv)

Neural networks achieved high performance over different tasks, i.e. image identification, voice recognition and other applications. Despite their success, these models are still vulnerable regarding small perturbations, which can be used to craft the so-called adversarial examples. Different approaches have been proposed to circumvent their vulnerability, including formal verification systems, which employ a variety of techniques, including reachability, optimization and search procedures, to verify that the model satisfies some property. In this paper we propose three novel reachability algorithms for verifying deep neural networks with ReLU activations. The first and third algorithms compute an over-approximation for the reachable set, whereas the second one computes the exact reachable set. Differently from previously proposed approaches, our algorithms take as input a V-polytope. Our experiments on the ACAS Xu problem show that the Exact Polytope Network Mapping (EPNM) reachability algorithm proposed in this work surpass the state-of-the-art results from the literature, specially in relation to other reachability methods.