Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Forward Invariance in Neural Network Controlled Systems

Akash Harapanahalli, Saber Jafarpour, Samuel Coogan

TL;DR

This work addresses safety certification for nonlinear systems controlled by neural networks by constructing forward-invariant sets under disturbances. It introduces a dynamical embedding framework built from localized first-order inclusion functions, enabling single-trajectory evaluation to generate nested invariant hyper-rectangles and extending to paralleletopes via a linear transform. Key contributions include two inclusion-function strategies (natural and Jacobian-based), a monotone embedding dynamics with Nagumo-type invariance guarantees, and a paralleletope extension with practical Python tooling demonstrated on an 8D leader–follower system. The results show converging families of invariant/attracting sets and provide a scalable offline method for searching safe invariant regions around learning-enabled controllers. This framework lays groundwork for robust, safety-aware design of learning-enabled controllers and suggests avenues for online extensions and broader NN architectures.

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.

Forward Invariance in Neural Network Controlled Systems

TL;DR

This work addresses safety certification for nonlinear systems controlled by neural networks by constructing forward-invariant sets under disturbances. It introduces a dynamical embedding framework built from localized first-order inclusion functions, enabling single-trajectory evaluation to generate nested invariant hyper-rectangles and extending to paralleletopes via a linear transform. Key contributions include two inclusion-function strategies (natural and Jacobian-based), a monotone embedding dynamics with Nagumo-type invariance guarantees, and a paralleletope extension with practical Python tooling demonstrated on an 8D leader–follower system. The results show converging families of invariant/attracting sets and provide a scalable offline method for searching safe invariant regions around learning-enabled controllers. This framework lays groundwork for robust, safety-aware design of learning-enabled controllers and suggests avenues for online extensions and broader NN architectures.

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 , in conjunction with the symbolic arithmetic toolbox , demonstrated on an -dimensional leader-follower system.
Paper Structure (9 sections, 4 theorems, 24 equations, 1 figure)

This paper contains 9 sections, 4 theorems, 24 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Problem Statement
  3. Inclusion Functions for Neural Network Controlled Systems
  4. Inclusion Functions
  5. Localized Closed-Loop Inclusion Functions
  6. A Dynamical Approach to Set Invariance
  7. Paralleletope Invariant Sets
  8. Numerical Experiments
  9. Conclusions

Key Result

Proposition 1

Consider the neural network controlled system eq:cldynsys with the disturbance set $\mathcal{W}=[\ul{w},\overline{w}]$ and initial condition $x_0\in[\ul{x}^\star,\overline{x}^\star]$. Given a set $\mathcal{S}\supseteq[\ul{x}^\star,\overline{x}^\star]$, let $\mathsf{F}^{\mathsf{c}}_\mathcal{S}$ be a then $[\ul{x}^\star,\overline{x}^\star]$ is a $[\ul{w},\overline{w}]$-robustly forward invariant se

Figures (1)

  • Figure 1: A family of 93 paralleletope invariant sets for the leader-follower system \ref{['eq:LFdynamics']} are visualized using projections from $\mathbb{R}^8$ onto $4$$\mathbb{R}^2$ planes. Top Left: projection onto leader's position $p_x^\mathrm{L},p_y^\mathrm{L}$; Top Right: projection onto leader's velocity $v_x^\mathrm{L},v_y^\mathrm{L}$; Bottom Left: projection onto follower's position $p_x^\mathrm{F},p_y^\mathrm{F}$; Bottom Right: projection onto follower's velocity $v_x^\mathrm{F},v_y^\mathrm{F}$. After one invariant set $\Phi^{-1}([\ul{y}_0,\overline{y}_0])$ is found (blue line), the transformed embedding system is integrated forwards until approximate convergence, and backwards until Proposition \ref{['prop:invariance']} is violated, yielding a monotonically decreasing collection of nested invariant sets converging to an attractive set (innermost lines).

Theorems & Definitions (10)

  • Remark 1: Interval observer
  • Proposition 1: Forward invariance in hyper-rectangles
  • proof
  • Remark 2: Linear systems with piecewise linear activations
  • Theorem 1: A nested family of invariant sets
  • proof
  • Proposition 2
  • proof
  • Theorem 2: Forward invariance in paralleletopes
  • proof