Forward Invariance in Neural Network Controlled Systems
This work addresses the challenge of ensuring safety and stability in neural network-controlled systems, which is critical for applications like robotics and autonomous vehicles, representing an incremental advancement in verification methods.
The authors tackled the problem of certifying and searching for forward invariant sets in nonlinear systems controlled by neural networks, developing a framework based on interval analysis and monotone systems theory that constructs inclusion functions and dynamical embeddings to prove convergence to attractive sets, demonstrated on an 8-dimensional leader-follower system.
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 $\texttt{npinterval}$, in conjunction with the symbolic arithmetic toolbox $\texttt{sympy}$, demonstrated on an $8$-dimensional leader-follower system.