# Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 75 references that are in the map.
- First posted on arXiv 27 Jul 2023.

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

- [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)
- [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)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Motion Planning Networks](https://mlsanity.com/paper/1806.05767/) (2018)
- [Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming](https://mlsanity.com/paper/2004.07876/) (2020)
- [Learning Deep Control Policies for Autonomous Aerial Vehicles with MPC-Guided Policy Search](https://mlsanity.com/paper/1509.06791/) (2015)
- [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)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [TIRA: Toolbox for Interval Reachability Analysis](https://mlsanity.com/paper/1902.05204/) (2019)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [ReachLipBnB: A branch-and-bound method for reachability analysis of neural autonomous systems using Lipschitz bounds](https://mlsanity.com/paper/2211.00608/) (2022)
- [A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2306.15340/) (2023)
- [Tight Decomposition Functions for Continuous-Time Mixed-Monotone Systems with Disturbances](https://mlsanity.com/paper/2003.07975/) (2020)
- [Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems](https://mlsanity.com/paper/2304.03671/) (2023)
- [On sufficient conditions for mixed monotonicity](https://mlsanity.com/paper/1803.04528/) (2018)
- [Tight Remainder-Form Decomposition Functions with Applications to Constrained Reachability and Guaranteed State Estimation](https://mlsanity.com/paper/2103.08638/) (2021)

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

- [textttimmrax: A Parallelizable and Differentiable Toolbox for Interval Analysis and Mixed Monotone Reachability in JAX](https://mlsanity.com/paper/2401.11608/) (2024)
- [Forward Invariance in Neural Network Controlled Systems](https://mlsanity.com/paper/2309.09043/) (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)
- [Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization](https://mlsanity.com/paper/2509.19688/) (2025)
- [Scalable Data-Driven Reachability Analysis and Control via Koopman Operators with Conformal Coverage Guarantees](https://mlsanity.com/paper/2601.01076/) (2026)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Neural Network-assisted Interval Reachability for Systems with Control Barrier Function-Based Safe Controllers](https://mlsanity.com/paper/2504.08249/) (2025)
- [Control Invariant Sets for Neural Network Dynamical Systems and Recursive Feasibility in Model Predictive Control](https://mlsanity.com/paper/2505.11546/) (2025)

## Abstract (arXiv)

In this paper, we propose a computationally efficient framework for interval reachability of systems with neural network controllers. Our approach leverages inclusion functions for the open-loop system and the neural network controller to embed the closed-loop system into a larger-dimensional embedding system, where a single trajectory over-approximates the original system's behavior under uncertainty. We propose two methods for constructing closed-loop embedding systems, which account for the interactions between the system and the controller in different ways. The interconnection-based approach considers the worst-case evolution of each coordinate separately by substituting the neural network inclusion function into the open-loop inclusion function. The interaction-based approach uses novel Jacobian-based inclusion functions to capture the first-order interactions between the open-loop system and the controller by leveraging state-of-the-art neural network verifiers. Finally, we implement our approach in a Python framework called ReachMM to demonstrate its efficiency and scalability on benchmarks and examples ranging to 200 state dimensions.