# Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 38 references that are in the map.
- First posted on arXiv 14 Dec 2022.

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

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [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)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming](https://mlsanity.com/paper/2004.07876/) (2020)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems](https://mlsanity.com/paper/2108.01220/) (2021)
- [Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components](https://mlsanity.com/paper/2011.11609/) (2020)
- [Lagrangian Decomposition for Neural Network Verification](https://mlsanity.com/paper/2002.10410/) (2020)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [One-Shot Reachability Analysis of Neural Network Dynamical Systems](https://mlsanity.com/paper/2209.11827/) (2022)
- [Safety Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2011.05174/) (2020)
- [DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting](https://mlsanity.com/paper/2106.09117/) (2021)
- [ReachLipBnB: A branch-and-bound method for reachability analysis of neural autonomous systems using Lipschitz bounds](https://mlsanity.com/paper/2211.00608/) (2022)
- [Reachability Analysis and Safety Verification of Neural Feedback Systems via Hybrid Zonotopes](https://mlsanity.com/paper/2210.03244/) (2022)
- [BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic](https://mlsanity.com/paper/2211.14438/) (2022)

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

- [Value Approximation for Two-Player General-Sum Differential Games with State Constraints](https://mlsanity.com/paper/2311.16520/) (2023)
- [Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis](https://mlsanity.com/paper/2406.04476/) (2024)

## Abstract (arXiv)

Over-approximating the reachable sets of dynamical systems is a fundamental problem in safety verification and robust control synthesis. The representation of these sets is a key factor that affects the computational complexity and the approximation error. In this paper, we develop a new approach for over-approximating the reachable sets of neural network dynamical systems using adaptive template polytopes. We use the singular value decomposition of linear layers along with the shape of the activation functions to adapt the geometry of the polytopes at each time step to the geometry of the true reachable sets. We then propose a branch-and-bound method to compute accurate over-approximations of the reachable sets by the inferred templates. We illustrate the utility of the proposed approach in the reachability analysis of linear systems driven by neural network controllers.