Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems

TL;DR

This work tackles the safety verification of nonlinear systems controlled by neural networks by improving interval reachability estimates. It introduces a contraction-guided adaptive partitioning algorithm (ReachMM-CG) that selectively partitions the state space based on contraction rates, while decoupling neural-network verification from the partitioning process to reduce computational cost. The authors provide contraction-based guarantees for the width of interval over-approximations and demonstrate significant runtime and accuracy improvements on nonlinear vehicle and linear double-integrator benchmarks, outperforming state-of-the-art partitioning methods. The approach is general enough to pair with various interval reachability and NN-verification tools, enabling scalable runtime safety verification for NN-controlled systems in practice.

Abstract

In this paper, we present a contraction-guided adaptive partitioning algorithm for improving interval-valued robust reachable set estimates in a nonlinear feedback loop with a neural network controller and disturbances. Based on an estimate of the contraction rate of over-approximated intervals, the algorithm chooses when and where to partition. Then, by leveraging a decoupling of the neural network verification step and reachability partitioning layers, the algorithm can provide accuracy improvements for little computational cost. This approach is applicable with any sufficiently accurate open-loop interval-valued reachability estimation technique and any method for bounding the input-output behavior of a neural network. Using contraction-based robustness analysis, we provide guarantees of the algorithm's performance with mixed monotone reachability. Finally, we demonstrate the algorithm's performance through several numerical simulations and compare it with existing methods in the literature. In particular, we report a sizable improvement in the accuracy of reachable set estimation in a fraction of the runtime as compared to state-of-the-art methods.

Figures (5)

• Figure 1: A snapshot of Algorithm \ref{['alg:main']} is illustrated for $n=1$. (top) There are two initial partitions that both compute the neural network verification step (filled circles in the graph representation). Both partitions are integrated from $t_{j-1}$ to $t_\gamma=t_{j-1} + \gamma(t_j - t_{j-1})$ to estimate the width of the box at $t_j$. Since the estimated blue partition width violates the user-defined maximum width $\varepsilon$, (bottom) the algorithm returns to $t_{j-1}$ and adds two new partitions to the tree. The maximum neural network verification depth here is $1$, so the new partitions do not recompute the neural network verification and instead use the same $E^c$\ref{['eq:clembsys']} from the initial blue partition.
• Figure 2: A partition tree structure of Algorithm \ref{['alg:main']} for a run on the double integrator system \ref{['eq:doubleintegrator']} for $\varepsilon=0.1$, $D_p=10$, $D_\text{N}=2$. The color represents the algorithm's separation---only nodes filled with red compute the neural network verification step, and all the integrations are performed only on the leaf nodes. The imbalanced structure is a consequence of the algorithm's spatial awareness. As a consequence of the algorithm's temporal awareness, the structure of the partition tree deepens as time increases.
• Figure 3: The over-approximated reachable sets of the closed-loop nonlinear vehicle model \ref{['eq:vehicle']} in the $(p_x,p_y)$ coordinates are shown in blue for the initial set $[7.9,8.1]^2\times[-\frac{2\pi}{3}-0.01, -\frac{2\pi}{3}+0.01]\times[1.99,2.01]$ over the time interval $[0,1.25]$. They are computed using Algorithm \ref{['alg:main']} with $\varepsilon=[0.2,0.2,\infty,\infty]^\mathsf{T}$, $D_p=2$, and $D_\text{N}=1$. The average runtime across 100 runs with standard deviation is reported, as well as the volume of the over-bounding box at the final time $T=1.25$. 200 true trajectories of the system are shown in the time-varying yellow line.
• Figure 4: The over-approximated reachable sets of the closed-loop double integrator model \ref{['eq:doubleintegrator']} are shown in blue for the initial set $[2.5,3]\times[-0.25,0.25]$ and final time $T=5$. They are computed using Algorithm 1 with the specified parameters in the title of each plot. The average runtime and standard deviation across 100 runs is reported, as well as the true area of the final reachable set. 200 true trajectories are shown in red. The horizontal axis is $x_1$ and the vertical axis is $x_2$.
• Figure 5: 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$.

Theorems & Definitions (5)

• Theorem 1: Accuracy guarantees for mixed-monotone reachability
• proof
• Remark 1
• Theorem 2: Upper bound on closed-loop contraction rate
• proof