Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops

Nicholas Rober, Jonathan P. How

TL;DR

Constraint-Aware Refinement for Verification (CARV) is presented, an efficient refinement strategy that reduces the conservativeness of RSOAs by explicitly using the safety constraints on the NFL.

Abstract

Neural networks (NNs) are becoming increasingly popular in the design of control pipelines for autonomous systems. However, since the performance of NNs can degrade in the presence of out-of-distribution data or adversarial attacks, systems that have NNs in their control pipelines, i.e., neural feedback loops (NFLs), need safety assurances before they can be applied in safety-critical situations. Reachability analysis offers a solution to this problem by calculating reachable sets that bound the possible future states of an NFL and can be checked against dangerous regions of the state space to verify that the system does not violate safety constraints. Since exact reachable sets are generally intractable to calculate, reachable set over approximations (RSOAs) are typically used. The problem with RSOAs is that they can be overly conservative, making it difficult to verify the satisfaction of safety constraints, especially over long time horizons or for highly nonlinear NN control policies. Refinement strategies such as partitioning or symbolic propagation are typically used to limit the conservativeness of RSOAs, but these approaches come with a high computational cost and often can only be used to verify safety for simple reachability problems. This paper presents Constraint-Aware Refinement for Verification (CARV): an efficient refinement strategy that reduces the conservativeness of RSOAs by explicitly using the safety constraints on the NFL to refine RSOAs only where necessary. We demonstrate that CARV can verify the safety of an NFL where other approaches either fail or take up to 60x longer and 40x the memory.

Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops

TL;DR

Constraint-Aware Refinement for Verification (CARV) is presented, an efficient refinement strategy that reduces the conservativeness of RSOAs by explicitly using the safety constraints on the NFL.

Abstract

Neural networks (NNs) are becoming increasingly popular in the design of control pipelines for autonomous systems. However, since the performance of NNs can degrade in the presence of out-of-distribution data or adversarial attacks, systems that have NNs in their control pipelines, i.e., neural feedback loops (NFLs), need safety assurances before they can be applied in safety-critical situations. Reachability analysis offers a solution to this problem by calculating reachable sets that bound the possible future states of an NFL and can be checked against dangerous regions of the state space to verify that the system does not violate safety constraints. Since exact reachable sets are generally intractable to calculate, reachable set over approximations (RSOAs) are typically used. The problem with RSOAs is that they can be overly conservative, making it difficult to verify the satisfaction of safety constraints, especially over long time horizons or for highly nonlinear NN control policies. Refinement strategies such as partitioning or symbolic propagation are typically used to limit the conservativeness of RSOAs, but these approaches come with a high computational cost and often can only be used to verify safety for simple reachability problems. This paper presents Constraint-Aware Refinement for Verification (CARV): an efficient refinement strategy that reduces the conservativeness of RSOAs by explicitly using the safety constraints on the NFL to refine RSOAs only where necessary. We demonstrate that CARV can verify the safety of an NFL where other approaches either fail or take up to 60x longer and 40x the memory.
Paper Structure (12 sections, 1 theorem, 10 equations, 8 figures, 1 table, 3 algorithms)

This paper contains 12 sections, 1 theorem, 10 equations, 8 figures, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. NFL System Dynamics
  4. Computational Graph Robustness Verification
  5. Symbolic vs. Concrete Reachability
  6. Constraint-Aware Refinement for Verification
  7. Numerical Results
  8. Double Integrator
  9. Ground Robot
  10. Varying the Maximum Symbolic Horizon
  11. Verification Analysis
  12. Conclusion

Key Result

Theorem 2.1

Given a CG $\bm{G}$ and a hyper-rectangular set of possible inputs $\mathcal{I}$, there exist two explicit functions such that the inequality $\underline{\bm{G}}(\mathbf{z}) \leq \bm{G}(\mathbf{z}) \leq \overline{\bm{G}}(\mathbf{z})$ holds element-wise for all $\mathbf{z} \in \mathcal{I}$, with $\bm{\Psi}, \bm{\Phi} \in \mathbb{R}^{n_o \times n_i}$ and $\bm{\alpha}, \bm{\beta} \in \mathbb{R}^{n_o

Figures (8)

  • Figure 1: To verify that the robot avoids the obstacles (gray), CARV makes fast but conservative reachable set over-approximations (blue) unless they conflict with an obstacle, which prompts CARV to refine them with slower but less conservative approximations (green).
  • Figure 2: Concrete RSOA calculations (top) are subject to the wrapping effect le2009reachability. The concrete RSOA ${\bar{\mathcal{R}}^c(\bar{\mathcal{R}}^c(\mathcal{X}_0))}$ (orange) is an over-approximation of the true reachable set (blue, $t=2$) of the concrete RSOA at $t=1$. Symbolic RSOA calculations (bottom) use multiple self-compositions of $f_{cl}$ to calculate the RSOA at time $t=2$ (green) without having to calculate an RSOA at $t=1$, thus avoiding the wrapping effect.
  • Figure 3: Successive frames of CARV's solution to $\mathsf{DI}$ showing how CARV detects a collision (\ref{['fig:double_integrator:conflict']}), fixes it with refinement (\ref{['fig:double_integrator:resolved']}), and repeats until the problem is successfully verified (\ref{['fig:double_integrator:final']}).
  • Figure 4: CARV (ours) outperforms part, symb, and hybr in computation time and ability to verify safety for $\mathsf{GR}$.
  • Figure 5: CARV verifies $\mathsf{GR}$ as safe for all tested $k_{max} \geq 8$.
  • ...and 3 more figures

Theorems & Definitions (1)

  • Theorem 2.1: CG Robustness xu2020automatic