# A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 29 references that are in the map.
- First posted on arXiv 14 Oct 2022.

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

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Adversarial examples in the physical world](https://mlsanity.com/paper/1607.02533/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Adversarial Examples: Attacks and Defenses for Deep Learning](https://mlsanity.com/paper/1712.07107/) (2017)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [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)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [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 Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach](https://mlsanity.com/paper/2004.12273/) (2020)
- [Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components](https://mlsanity.com/paper/2011.11609/) (2020)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Fast Neural Network Verification via Shadow Prices](https://mlsanity.com/paper/1902.07247/) (2019)
- [Backward Reachability Analysis for Neural Feedback Loops](https://mlsanity.com/paper/2204.08319/) (2022)
- [Verifying Low-dimensional Input Neural Networks via Input Quantization](https://mlsanity.com/paper/2108.07961/) (2021)

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

- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Exact Verification of ReLU Neural Control Barrier Functions](https://mlsanity.com/paper/2310.09360/) (2023)
- [DRIP: Domain Refinement Iteration with Polytopes for Backward Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2212.04646/) (2022)
- [Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops](https://mlsanity.com/paper/2410.00145/) (2024)
- [TTT: A Temporal Refinement Heuristic for Tenuously Tractable Discrete Time Reachability Problems](https://mlsanity.com/paper/2407.14394/) (2024)
- [The inverse problem for neural networks](https://mlsanity.com/paper/2308.14093/) (2023)

## Abstract (arXiv)

As neural networks become more integrated into the systems that we depend on for transportation, medicine, and security, it becomes increasingly important that we develop methods to analyze their behavior to ensure that they are safe to use within these contexts. The methods used in this paper seek to certify safety for closed-loop systems with neural network controllers, i.e., neural feedback loops, using backward reachability analysis. Namely, we calculate backprojection (BP) set over-approximations (BPOAs), i.e., sets of states that lead to a given target set that bounds dangerous regions of the state space. The system's safety can then be certified by checking its current state against the BPOAs. While over-approximating BPs is significantly faster than calculating exact BP sets, solving the relaxed problem leads to conservativeness. To combat conservativeness, partitioning strategies can be used to split the problem into a set of sub-problems, each less conservative than the unpartitioned problem. We introduce a hybrid partitioning method that uses both target set partitioning (TSP) and backreachable set partitioning (BRSP) to overcome a lower bound on estimation error that is present when using BRSP. Numerical results demonstrate a near order-of-magnitude reduction in estimation error compared to BRSP or TSP given the same computation time.