Table of Contents
Fetching ...

Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops

Saber Jafarpour, Akash Harapanahalli, Samuel Coogan

Abstract

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.

Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops

Abstract

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 state dimensions.
Paper Structure (19 sections, 10 theorems, 46 equations, 8 figures, 4 tables)

This paper contains 19 sections, 10 theorems, 46 equations, 8 figures, 4 tables.

Key Result

Theorem 1

Consider the function $g:\mathbb{R}^n\to \mathbb{R}^m$ and the mapping $\mathsf{G}^{\min} = \left[\right]$ defined by eq:tight. Then, for every ${x}\le \widehat{x}$, we have

Figures (8)

  • Figure 1: Left:npinterval is used to generate interval approximations for a function $g(x_1,x_2) = [(x_1 + x_2)^2, 4\sin((x_1 - x_2)/4)]^{\top}$ using two different natural inclusion functions. Blue: using the inclusion functions for elementary functions $x\mapsto x^2$ and $x\mapsto \sin(x)$ in AH-SJ-SC:23b, Green: rewriting $g(x_1,x_2) = [x_2^2 + 2x_1x_2 + x_2^2, 4\sin(x_1/4)\cos(x_2/4) - 4\cos(x_1/4)\sin(x_2/4)]^{\top}$ and obtaining a different natural inclusion function based on composition of elementary inclusion functions in AH-SJ-SC:23b. The approximations are generated using the initial set $[-1,1]\times[-1,1]$, and 2000 uniformly sampled ouptuts are shown in red. Right: The same function is analyzed, with the same two natural inclusion functions, but the initial set is partitioned into 1024 uniform sections, and the union of the interval approximations are shown.
  • Figure 2: Pictorial comparison between the minimal (equation \ref{['eq:tight']}), the Jacobian-based centered (LJ-MK-OD-EW:01), and the Jacobian-based cornered (Proposition \ref{['thm:jacobian-basedIF']}) inclusion functions for $f(x)=x^2$ and $f(x)=x^3$ on the interval $[-1,1]$. Note that, for the monotone function $f(x)=x^3$, the intersection of the two Jacobian-based cornered inclusion functions (shown by blue and red dashed lines) leads to the minimal inclusion function.
  • Figure 3: Accuracy and runtime comparison between different reachability approaches for the bicycle model \ref{['eq:vehicle']} from the initial set $[7.95,8.05]\times[6.95,7.05]\times[-2\pi/3 - 0.01, -2\pi/3 + 0.01]\times[1.99,2.01]$ for the period $t\in [0,1.5]$: (a) a naive input-output approach combining the natural inclusion function for the open-loop dynamics and the affine inclusion function for the neural network, (b) the interconnection-based approach with the closed-loop inclusion function $\mathsf{F}^{\mathrm{con}}$ defined in \ref{['eq:int-inclusion']} constructed from the natural inclusion function for the open loop dynamics and affine inclusion function for the neural network, (c) the interaction-based approach with Jacobian-based cornered inclusion function $\mathsf{F}^{\mathrm{act}}$ defined in \ref{['eq:jac-inclusion']}, (d) the intersection of the interconnection-based inclusion and interaction-based approach $\mathsf{F}^{\mathrm{con}}\wedge \mathsf{F}^{\mathrm{act}}$, (e) the interaction-based approach with mixed states Jacobian-based cornered inclusion function defined in \ref{['eq:jac-inclusion']} and Remark \ref{['rem:important']}\ref{['p2:important']}, and (f) the interaction-based approach with mixed states and control Jacobian-based cornered inclusion function defined \ref{['eq:jac-inclusion']} and Remark \ref{['rem:important']}\ref{['p2:important']}. The blue boxes are hyper-rectangular over-approximation of reachable sets, $100$ simulated trajectories of the system are shown in red, and the salmon colored region represents a circular obstacle.
  • Figure 4: The over-approximated reachable sets of the closed-loop double integrator model \ref{['eq:doubleintegrator']} are compared for three different algorithms on two different runtime regimes, for the initial set $[2.5,3]\times[-0.25,0.25]$ and final time $T=5$. The experiment setup and performances are reported in Table \ref{['tab:DI_table']}. 200 true trajectories are shown in red. The horizontal axis is $x_1$ and the vertical axis is $x_2$.
  • Figure 5: The interval estimates of the safety specifications for the Adaptive Cruise Control benchmark obtained from the inclusion function $\mathsf{F}^{\mathrm{con}}$. The upper bound and lower bound on $D_\text{rel}$ are shown in blue and the upper and lower bounds on $D_\text{safe}$ are shown in red. Our approach ensures that $D_\text{red}\geq D_\text{safe}$ for $t\in [0,5]$.
  • ...and 3 more figures

Theorems & Definitions (32)

  • Definition 1: Inclusion function LJ-MK-OD-EW:01
  • Theorem 1: Minimal inclusion functions
  • proof
  • Proposition 1: Jacobian-based cornered inclusion function
  • proof
  • Remark 1
  • Proposition 2: Mixed Jacobian-based cornered inclusion function
  • proof
  • Example 1: Cornered inclusion functions
  • Definition 2: Decomposition function
  • ...and 22 more