# Forward Invariance in Neural Network Controlled Systems

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 25 references that are in the map.
- First posted on arXiv 16 Sep 2023.

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

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Lyapunov-stable neural-network control](https://mlsanity.com/paper/2109.14152/) (2021)
- [Stability Analysis using Quadratic Constraints for Systems with Neural Network Controllers](https://mlsanity.com/paper/2006.07579/) (2020)
- [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)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [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)
- [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)
- [Computing Robustly Forward Invariant Sets for Mixed-Monotone Systems](https://mlsanity.com/paper/2003.05912/) (2020)

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

- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)
- [Certified Robust Invariant Polytope Training in Neural Controlled ODEs](https://mlsanity.com/paper/2408.01273/) (2024)
- [Toward AI Trustworthiness: Finding Analytically Proven Forward-Invariant Sets for AI-Controlled Systems](https://mlsanity.com/paper/2610.05689/) (2026)

## Abstract (arXiv)

We present a framework based on interval analysis and monotone systems theory to certify and search for forward invariant sets in nonlinear systems with neural network controllers. The framework (i) constructs localized first-order inclusion functions for the closed-loop system using Jacobian bounds and existing neural network verification tools; (ii) builds a dynamical embedding system where its evaluation along a single trajectory directly corresponds with a nested family of hyper-rectangles provably converging to an attractive set of the original system; (iii) utilizes linear transformations to build families of nested paralleletopes with the same properties. The framework is automated in Python using our interval analysis toolbox textttnpinterval, in conjunction with the symbolic arithmetic toolbox textttsympy, demonstrated on an 8-dimensional leader-follower system.