# ReachNN: Reachability Analysis of Neural-Network Controlled Systems

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

## Key facts

- Cited by 26 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Jun 2019.

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

- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Reachability Analysis of a General Class of Neural Ordinary Differential Equations](https://mlsanity.com/paper/2207.06531/) (2022)
- [Risk-averse autonomous systems: A brief history and recent developments from the perspective of optimal control](https://mlsanity.com/paper/2109.08947/) (2021)
- [Joint Differentiable Optimization and Verification for Certified Reinforcement Learning](https://mlsanity.com/paper/2201.12243/) (2022)
- [Efficient Reachability Analysis of Closed-Loop Systems with Neural Network Controllers](https://mlsanity.com/paper/2101.01815/) (2021)
- [Backward Reachability Analysis for Neural Feedback Loops](https://mlsanity.com/paper/2204.08319/) (2022)
- [Data-Driven Reachability Analysis of Stochastic Dynamical Systems with Conformal Inference](https://mlsanity.com/paper/2309.09187/) (2023)
- [A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops](https://mlsanity.com/paper/2210.07918/) (2022)
- [Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning](https://mlsanity.com/paper/2104.10219/) (2021)
- [Safety Verification for Neural Networks Based on Set-boundary Analysis](https://mlsanity.com/paper/2210.04175/) (2022)
- [Generating Probabilistic Safety Guarantees for Neural Network Controllers](https://mlsanity.com/paper/2103.01203/) (2021)
- [Repairing Deep Neural Networks Based on Behavior Imitation](https://mlsanity.com/paper/2305.03365/) (2023)
- [A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems](https://mlsanity.com/paper/2303.05394/) (2023)
- [Verification of Neural Network Control Systems using Symbolic Zonotopes and Polynotopes](https://mlsanity.com/paper/2306.14619/) (2023)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [Neural Abstraction-Based Controller Synthesis and Deployment](https://mlsanity.com/paper/2307.03783/) (2023)
- [Verification of Neural Network Control Systems in Continuous Time](https://mlsanity.com/paper/2406.00157/) (2024)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)
- [Learning Verifiable Control Policies Using Relaxed Verification](https://mlsanity.com/paper/2504.16879/) (2025)
- [Failing with Grace: Learning Neural Network Controllers that are Boundedly Unsafe](https://mlsanity.com/paper/2106.11881/) (2021)
- [Towards Global Neural Network Abstractions with Locally-Exact Reconstruction](https://mlsanity.com/paper/2210.12054/) (2022)

## Abstract (arXiv)

Applying neural networks as controllers in dynamical systems has shown great promises. However, it is critical yet challenging to verify the safety of such control systems with neural-network controllers in the loop. Previous methods for verifying neural network controlled systems are limited to a few specific activation functions. In this work, we propose a new reachability analysis approach based on Bernstein polynomials that can verify neural-network controlled systems with a more general form of activation functions, i.e., as long as they ensure that the neural networks are Lipschitz continuous. Specifically, we consider abstracting feedforward neural networks with Bernstein polynomials for a small subset of inputs. To quantify the error introduced by abstraction, we provide both theoretical error bound estimation based on the theory of Bernstein polynomials and more practical sampling based error bound estimation, following a tight Lipschitz constant estimation approach based on forward reachability analysis. Compared with previous methods, our approach addresses a much broader set of neural networks, including heterogeneous neural networks that contain multiple types of activation functions. Experiment results on a variety of benchmarks show the effectiveness of our approach.