Forward Invariance in Neural Network Controlled Systems

TL;DR

This paper introduces a novel framework combining interval analysis and monotone systems theory to certify forward invariance in nonlinear systems with neural network controllers, enabling verification and search for invariant sets.

Contribution

It develops an automated method using Jacobian bounds and neural network verification tools to construct invariant sets in neural network controlled systems.

Findings

Successfully applied to an 8-dimensional leader-follower system.

Constructed nested hyper-rectangles converging to an attractive set.

Built families of nested paralleletopes with invariance properties.

Abstract

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.