# An approach to reachability analysis for feed-forward ReLU neural networks

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

## Key facts

- Cited by 127 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Jun 2017.

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

- [Orthogonalizing Convolutional Layers with the Cayley Transform](https://mlsanity.com/paper/2104.07167/) (2021)
- [Certified Patch Robustness via Smoothed Vision Transformers](https://mlsanity.com/paper/2110.07719/) (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)
- [Partition-based formulations for mixed-integer optimization of trained ReLU neural networks](https://mlsanity.com/paper/2102.04373/) (2021)
- [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)
- [Multi-Label Classification Neural Networks with Hard Logical Constraints](https://mlsanity.com/paper/2103.13427/) (2021)
- [OMLT: Optimization & Machine Learning Toolkit](https://mlsanity.com/paper/2202.02414/) (2022)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Low Curvature Activations Reduce Overfitting in Adversarial Training](https://mlsanity.com/paper/2102.07861/) (2021)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [ANCER: Anisotropic Certification via Sample-wise Volume Maximization](https://mlsanity.com/paper/2107.04570/) (2021)
- [Expressive Losses for Verified Robustness via Convex Combinations](https://mlsanity.com/paper/2305.13991/) (2023)
- [Safe Control with Neural Network Dynamic Models](https://mlsanity.com/paper/2110.01110/) (2021)
- [Pruning and Slicing Neural Networks using Formal Verification](https://mlsanity.com/paper/2105.13649/) (2021)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [CertiFair: A Framework for Certified Global Fairness of Neural Networks](https://mlsanity.com/paper/2205.09927/) (2022)
- [Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding](https://mlsanity.com/paper/2203.14141/) (2022)
- [Mitigating the Curse of Dimensionality for Certified Robustness via Dual Randomized Smoothing](https://mlsanity.com/paper/2404.09586/) (2024)
- [Learning Security Classifiers with Verified Global Robustness Properties](https://mlsanity.com/paper/2105.11363/) (2021)
- [Neural Network Verification in Control](https://mlsanity.com/paper/2110.01388/) (2021)
- [Minimal Multi-Layer Modifications of Deep Neural Networks](https://mlsanity.com/paper/2110.09929/) (2021)
- [Infinite Time Horizon Safety of Bayesian Neural Networks](https://mlsanity.com/paper/2111.03165/) (2021)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [A Unified View of SDP-based Neural Network Verification through Completely Positive Programming](https://mlsanity.com/paper/2203.03034/) (2022)

## Abstract (arXiv)

We study the reachability problem for systems implemented as feed-forward neural networks whose activation function is implemented via ReLU functions. We draw a correspondence between establishing whether some arbitrary output can ever be outputed by a neural system and linear problems characterising a neural system of interest. We present a methodology to solve cases of practical interest by means of a state-of-the-art linear programs solver. We evaluate the technique presented by discussing the experimental results obtained by analysing reachability properties for a number of benchmarks in the literature.