# Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 32 references that are in the map.
- First posted on arXiv 7 Apr 2023.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [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)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems](https://mlsanity.com/paper/2108.01220/) (2021)
- [Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach](https://mlsanity.com/paper/2004.12273/) (2020)
- [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)
- [Fast Neural Network Verification via Shadow Prices](https://mlsanity.com/paper/1902.07247/) (2019)
- [Non-Euclidean Contraction Theory for Robust Nonlinear Stability](https://mlsanity.com/paper/2103.12263/) (2021)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [Safety Verification of Neural Feedback Systems Based on Constrained Zonotopes](https://mlsanity.com/paper/2204.00903/) (2022)
- [ReachLipBnB: A branch-and-bound method for reachability analysis of neural autonomous systems using Lipschitz bounds](https://mlsanity.com/paper/2211.00608/) (2022)

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

- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis](https://mlsanity.com/paper/2406.04476/) (2024)
- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)

## Abstract (arXiv)

In this paper, we present a contraction-guided adaptive partitioning algorithm for improving interval-valued robust reachable set estimates in a nonlinear feedback loop with a neural network controller and disturbances. Based on an estimate of the contraction rate of over-approximated intervals, the algorithm chooses when and where to partition. Then, by leveraging a decoupling of the neural network verification step and reachability partitioning layers, the algorithm can provide accuracy improvements for little computational cost. This approach is applicable with any sufficiently accurate open-loop interval-valued reachability estimation technique and any method for bounding the input-output behavior of a neural network. Using contraction-based robustness analysis, we provide guarantees of the algorithm's performance with mixed monotone reachability. Finally, we demonstrate the algorithm's performance through several numerical simulations and compare it with existing methods in the literature. In particular, we report a sizable improvement in the accuracy of reachable set estimation in a fraction of the runtime as compared to state-of-the-art methods.