# Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations

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

## Key facts

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

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

- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [CertiFair: A Framework for Certified Global Fairness of Neural Networks](https://mlsanity.com/paper/2205.09927/) (2022)
- [Traversing the Local Polytopes of ReLU Neural Networks: A Unified Approach for Network Verification](https://mlsanity.com/paper/2111.08922/) (2021)
- [Towards Verifying the Geometric Robustness of Large-scale Neural Networks](https://mlsanity.com/paper/2301.12456/) (2023)
- [SyReNN: A Tool for Analyzing Deep Neural Networks](https://mlsanity.com/paper/2101.03263/) (2021)
- [Benchmarking Safe Deep Reinforcement Learning in Aquatic Navigation](https://mlsanity.com/paper/2112.10593/) (2021)
- [Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks](https://mlsanity.com/paper/2111.09293/) (2021)
- [ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks](https://mlsanity.com/paper/2407.01639/) (2024)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [Safety Verification for Neural Networks Based on Set-boundary Analysis](https://mlsanity.com/paper/2210.04175/) (2022)
- [BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic](https://mlsanity.com/paper/2211.14438/) (2022)
- [Reachability Analysis of Convolutional Neural Networks](https://mlsanity.com/paper/2106.12074/) (2021)
- [Safety Verification of Neural Network Control Systems Using Guaranteed Neural Network Model Reduction](https://mlsanity.com/paper/2301.07531/) (2023)
- [Robust Optimization Framework for Training Shallow Neural Networks Using Reachability Method](https://mlsanity.com/paper/2107.12801/) (2021)
- [Vertex-based reachability analysis for verifying ReLU deep neural networks](https://mlsanity.com/paper/2301.12001/) (2023)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)
- [Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool](https://mlsanity.com/paper/2207.06759/) (2022)
- [UR4NNV: Neural Network Verification, Under-approximation Reachability Works!](https://mlsanity.com/paper/2401.12550/) (2024)
- [Lipschitz-Based Robustness Certification for Recurrent Neural Networks via Convex Relaxation](https://mlsanity.com/paper/2509.17898/) (2025)
- [Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solvers](https://mlsanity.com/paper/2603.00408/) (2026)

## Abstract (arXiv)

Neural networks have been widely used to solve complex real-world problems. Due to the complicate, nonlinear, non-convex nature of neural networks, formal safety guarantees for the output behaviors of neural networks will be crucial for their applications in safety-critical systems.In this paper, the output reachable set computation and safety verification problems for a class of neural networks consisting of Rectified Linear Unit (ReLU) activation functions are addressed. A layer-by-layer approach is developed to compute output reachable set. The computation is formulated in the form of a set of manipulations for a union of polyhedra, which can be efficiently applied with the aid of polyhedron computation tools. Based on the output reachable set computation results, the safety verification for a ReLU neural network can be performed by checking the intersections of unsafe regions and output reachable set described by a union of polyhedra. A numerical example of a randomly generated ReLU neural network is provided to show the effectiveness of the approach developed in this paper.