Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems

Chelsea Sidrane, Jana Tumova

TL;DR

This work tackles the problem of verifying reachability properties for learning-enabled, nonlinear neural feedback loop systems by developing an algorithm for underapproximate k-step backward reachability. The core idea is to overapproximate the nonlinear dynamics with a multivalued piecewise-linear hatf and to compute a union of norm balls that underapproximate the backward reachable sets via solving MILPs over a horizon k. The authors provide a rigorous soundness analysis, a numerical demonstration on a 2D robot navigation task, and a method to check goal reaching by testing polytope inclusion within unions of convex sets, enabling verification of reach properties for nonlinear NFLs. The results contribute a principled, verifiable approach to safety guarantees for learning-enabled control, albeit with scalability limits that motivate future hybrid symbolic techniques for longer horizons.

Abstract

Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based on overapproximating the system dynamics function to enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems.

BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems

TL;DR

This work tackles the problem of verifying reachability properties for learning-enabled, nonlinear neural feedback loop systems by developing an algorithm for underapproximate k-step backward reachability. The core idea is to overapproximate the nonlinear dynamics with a multivalued piecewise-linear hatf and to compute a union of norm balls that underapproximate the backward reachable sets via solving MILPs over a horizon k. The authors provide a rigorous soundness analysis, a numerical demonstration on a 2D robot navigation task, and a method to check goal reaching by testing polytope inclusion within unions of convex sets, enabling verification of reach properties for nonlinear NFLs. The results contribute a principled, verifiable approach to safety guarantees for learning-enabled control, albeit with scalability limits that motivate future hybrid symbolic techniques for longer horizons.

Abstract

Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based on overapproximating the system dynamics function to enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems.
Paper Structure (19 sections, 6 theorems, 14 equations, 7 figures, 1 table, 2 algorithms)

This paper contains 19 sections, 6 theorems, 14 equations, 7 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction & Related Work
  2. Related Work
  3. Contributions
  4. Preliminaries
  5. Problem Setting
  6. Problem Statement
  7. Method
  8. Encoding a Nonlinear NFL into an MILP
  9. Backward Reachability Algorithm
  10. Computation of a Single Norm Ball
  11. Showing the subset property.
  12. Showing the Boundary Intersection Property.
  13. Generalization to Multiple Underapproximate Sets
  14. Input and Output Constraints
  15. Encoding a Union of Convex Sets
  16. ...and 4 more sections

Key Result

Lemma III.4

Computing underapproximate backward reachable sets $\mathcal{R}^{f_{cl}}_{(-t)_{\text{under}}}(\mathcal{G}) \subseteq \mathcal{R}^{f_{cl}}_{(-t)}(\mathcal{G})$ allows for the sound verification of goal-reaching properties.

Figures (7)

  • Figure 1: Visual illustration of algorithm
  • Figure 2: Illustration of sets relevant to proof of \ref{['lem:touch']}.
  • Figure 3: Comparison of two figures side by side
  • Figure 4: Visual illustration of \ref{['lem:oa1']}, which demonstrates how we are able to compute underapproximate backward reachable sets from function overapproximations.
  • Figure 5: Underapproximate backward reachable sets for seven steps and $n_{samp}=15$, showing two possible starting sets, one safe and one unsafe.
  • ...and 2 more figures

Theorems & Definitions (21)

  • Definition II.1
  • Definition II.2
  • Definition II.3
  • Definition III.1
  • Definition III.2
  • Definition III.3
  • Lemma III.4
  • proof
  • Definition IV.1
  • Definition IV.2
  • ...and 11 more