# Reachability Analysis of Neural Feedback Loops

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

## Key facts

- Cited by 41 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 58 references that are in the map.
- First posted on arXiv 9 Aug 2021.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [CVXPY: A Python-Embedded Modeling Language for Convex Optimization](https://mlsanity.com/paper/1603.00943/) (2016)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Invertible Residual Networks](https://mlsanity.com/paper/1811.00995/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Certified Defenses against Adversarial Examples](https://mlsanity.com/paper/1801.09344/) (2018)
- [Control Barrier Function Based Quadratic Programs for Safety Critical Systems](https://mlsanity.com/paper/1609.06408/) (2016)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Analyzing Inverse Problems with Invertible Neural Networks](https://mlsanity.com/paper/1808.04730/) (2018)
- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming](https://mlsanity.com/paper/2004.07876/) (2020)
- [Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach](https://mlsanity.com/paper/2004.12273/) (2020)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [Certifiable Robustness to Adversarial State Uncertainty in Deep Reinforcement Learning](https://mlsanity.com/paper/2004.06496/) (2020)
- [Efficient Reachability Analysis of Closed-Loop Systems with Neural Network Controllers](https://mlsanity.com/paper/2101.01815/) (2021)

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

- [The Safety Filter: A Unified View of Safety-Critical Control in Autonomous Systems](https://mlsanity.com/paper/2309.05837/) (2023)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Neural Network Verification in Control](https://mlsanity.com/paper/2110.01388/) (2021)
- [A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis](https://mlsanity.com/paper/2112.05745/) (2021)
- [Backward Reachability Analysis for Neural Feedback Loops](https://mlsanity.com/paper/2204.08319/) (2022)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [Reachability Analysis of Neural Network Control Systems](https://mlsanity.com/paper/2301.12100/) (2023)
- [A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops](https://mlsanity.com/paper/2210.07918/) (2022)
- [DRIP: Domain Refinement Iteration with Polytopes for Backward Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2212.04646/) (2022)
- [DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation](https://mlsanity.com/paper/2305.13508/) (2023)
- [Hybrid Zonotopes Exactly Represent ReLU Neural Networks](https://mlsanity.com/paper/2304.02755/) (2023)
- [Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops](https://mlsanity.com/paper/2410.00145/) (2024)
- [Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems](https://mlsanity.com/paper/2304.03671/) (2023)
- [Forward Invariance in Neural Network Controlled Systems](https://mlsanity.com/paper/2309.09043/) (2023)
- [Value Approximation for Two-Player General-Sum Differential Games with State Constraints](https://mlsanity.com/paper/2311.16520/) (2023)
- [Certified Robust Invariant Polytope Training in Neural Controlled ODEs](https://mlsanity.com/paper/2408.01273/) (2024)
- [Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control](https://mlsanity.com/paper/2411.18235/) (2024)
- [Predictive Uncertainty for Runtime Assurance of a Real-Time Computer Vision-Based Landing System](https://mlsanity.com/paper/2508.09732/) (2025)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems](https://mlsanity.com/paper/2505.03643/) (2025)
- [Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization](https://mlsanity.com/paper/2509.19688/) (2025)
- [Factored Diffusion Policies:Compositionally Generalized Robot Control with a Single Score Network](https://mlsanity.com/paper/2605.22596/) (2026)
- [Learning Verifiable Control Policies Using Relaxed Verification](https://mlsanity.com/paper/2504.16879/) (2025)
- [ECLipsE-Gen-Local: Efficient Compositional Local Lipschitz Estimates for Deep Neural Networks](https://mlsanity.com/paper/2510.05261/) (2025)
- [Scalable Data-Driven Reachability Analysis and Control via Koopman Operators with Conformal Coverage Guarantees](https://mlsanity.com/paper/2601.01076/) (2026)
- [Permissive Safety Through Trusted Inference: Verifiable Belief-Space Neural Safety Filters for Assured Interactive Robotics](https://mlsanity.com/paper/2606.02562/) (2026)
- [Convex Hulls of Reachable Sets](https://mlsanity.com/paper/2303.17674/) (2023)

## Abstract (arXiv)

Neural Networks (NNs) can provide major empirical performance improvements for closed-loop systems, but they also introduce challenges in formally analyzing those systems' safety properties. In particular, this work focuses on estimating the forward reachable set of textitneural feedback loops (closed-loop systems with NN controllers). Recent work provides bounds on these reachable sets, but the computationally tractable approaches yield overly conservative bounds (thus cannot be used to verify useful properties), and the methods that yield tighter bounds are too intensive for online computation. This work bridges the gap by formulating a convex optimization problem for the reachability analysis of closed-loop systems with NN controllers. While the solutions are less tight than previous (semidefinite program-based) methods, they are substantially faster to compute, and some of those computational time savings can be used to refine the bounds through new input set partitioning techniques, which is shown to dramatically reduce the tightness gap. The new framework is developed for systems with uncertainty (e.g., measurement and process noise) and nonlinearities (e.g., polynomial dynamics), and thus is shown to be applicable to real-world systems. To inform the design of an initial state set when only the target state set is known/specified, a novel algorithm for backward reachability analysis is also provided, which computes the set of states that are guaranteed to lead to the target set. The numerical experiments show that our approach (based on linear relaxations and partitioning) gives a 5× reduction in conservatism in 150× less computation time compared to the state-of-the-art. Furthermore, experiments on quadrotor, 270-state, and polynomial systems demonstrate the method's ability to handle uncertainty sources, high dimensionality, and nonlinear dynamics, respectively.