Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures

Samuel I. Akinwande, Chelsea Sidrane, Mykel J. Kochenderfer, Clark Barrett

TL;DR

The paper presents OvertPoly, a forward-reachability verification framework for nonlinear neural feedback systems that leverages tight polyhedral enclosures to bound multivariate nonlinear dynamics. By encoding these enclosures and the neural controller as MILPs, the method achieves sound over-approximations of forward reachable sets, with both concrete and symbolic reachability to mitigate conservatism. The approach generalizes OVERT’s combinatorial strengths to nonlinear dynamics via a structured, grid-based, decomposition-based enclosure strategy that can outperform state-of-the-art propagation-based tools like CORA and combinatorial tools like OVERTVerify on representative benchmarks (e.g., Single Pendulum, ACC, TORA, Unicycle). Implemented in Julia and evaluated on realistic neural-feedback models, OvertPoly demonstrates order-of-magnitude improvements in runtime and precision, enabling scalable verification for safety-critical systems. Overall, the work advances formal verification of nonlinear neural feedback loops by delivering a scalable, exact-enclosure MILP framework with practical impact for safer autonomous systems.

Abstract

As dynamical systems equipped with neural network controllers (neural feedback systems) become increasingly prevalent, it is critical to develop methods to ensure their safe operation. Verifying safety requires extending control theoretic analysis methods to these systems. Although existing techniques can efficiently handle linear neural feedback systems, relatively few scalable methods address the nonlinear case. We propose a novel algorithm for forward reachability analysis of nonlinear neural feedback systems. The approach leverages the structure of the nonlinear transition functions of the systems to compute tight polyhedral enclosures (i.e., abstractions). These enclosures, combined with the neural controller, are then encoded as a mixed-integer linear program (MILP). Optimizing this MILP yields a sound over-approximation of the forward-reachable set. We evaluate our algorithm on representative benchmarks and demonstrate an order of magnitude improvement over the current state of the art.

Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures

TL;DR

The paper presents OvertPoly, a forward-reachability verification framework for nonlinear neural feedback systems that leverages tight polyhedral enclosures to bound multivariate nonlinear dynamics. By encoding these enclosures and the neural controller as MILPs, the method achieves sound over-approximations of forward reachable sets, with both concrete and symbolic reachability to mitigate conservatism. The approach generalizes OVERT’s combinatorial strengths to nonlinear dynamics via a structured, grid-based, decomposition-based enclosure strategy that can outperform state-of-the-art propagation-based tools like CORA and combinatorial tools like OVERTVerify on representative benchmarks (e.g., Single Pendulum, ACC, TORA, Unicycle). Implemented in Julia and evaluated on realistic neural-feedback models, OvertPoly demonstrates order-of-magnitude improvements in runtime and precision, enabling scalable verification for safety-critical systems. Overall, the work advances formal verification of nonlinear neural feedback loops by delivering a scalable, exact-enclosure MILP framework with practical impact for safer autonomous systems.

Abstract

As dynamical systems equipped with neural network controllers (neural feedback systems) become increasingly prevalent, it is critical to develop methods to ensure their safe operation. Verifying safety requires extending control theoretic analysis methods to these systems. Although existing techniques can efficiently handle linear neural feedback systems, relatively few scalable methods address the nonlinear case. We propose a novel algorithm for forward reachability analysis of nonlinear neural feedback systems. The approach leverages the structure of the nonlinear transition functions of the systems to compute tight polyhedral enclosures (i.e., abstractions). These enclosures, combined with the neural controller, are then encoded as a mixed-integer linear program (MILP). Optimizing this MILP yields a sound over-approximation of the forward-reachable set. We evaluate our algorithm on representative benchmarks and demonstrate an order of magnitude improvement over the current state of the art.

Paper Structure

This paper contains 61 sections, 3 theorems, 45 equations, 12 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Notation
  4. Polyhedra
  5. Bounding Convex Functions
  6. ReLU Functions as Mixed Integer Constraints
  7. Neural Feedback Systems
  8. Running Example: Unicycle Car Model
  9. Polyhedral Enclosures
  10. Polyhedral Enclosures of Univariate Functions
  11. Composing Polyhedral Enclosures
  12. The OvertPoly Algorithm
  13. Computing Tight Enclosures for Nonlinear Dynamics
  14. Generating an Efficient Optimization Model for the Enclosures
  15. Generating an exact representation of the neural network controller
  16. ...and 46 more sections

Key Result

Theorem 1

If a bounding set $\mathcal{B}\xspace=\langle k,P\xspace,L,U\rangle$ encloses a function $f$, then for every $n>k$, $S \subset [1..n]$ with $|S|=k$, and $\vec{p}^{\:l},\vec{p}^{\:u}\in\mathbb{R}\xspace^n$, with $\vec{p}^{\:l}_i < \vec{p}^{\:u}_i$ for $i\in[1..n]\setminus S$,$\mathcal{B}\xspace\!\!\u

Figures (12)

  • Figure 1: Overview of bounding algorithm for example problem. We bound $\cos(\mathbf{x}_3)$ and $\mathbf{x}_4$ , yielding a polyhedral enclosure
  • Figure 3: A visualization of Equations \ref{['eq:cc1']} -- \ref{['eq:cc2']} for a lower dimensional projection of our running example. \ref{['eq:cc3']} is implicitly defined here as well because $\vec{x}$ is the union of these points.
  • Figure 4: Dependency graph for Unicycle example. The green vertices represent state variables, while the blue vertex represents the neural network controller. Note that each variable is connected to the controller because the neural network depends on the full state.
  • Figure 5: Symbolic dependency graph for the Unicycle car model. The state dependency graphs are identical at each time step (since the transition functions are time invariant), but there are edges connecting models across time steps.
  • Figure 6: OvertPoly($G,s$)
  • ...and 7 more figures

Theorems & Definitions (44)

  • Definition 1: $k$-Simplex
  • Definition 2: $k$-Simplex
  • Definition 3: Simplicial $k$-Complex
  • Definition 4: Full-Dimensional
  • Definition 5: Point Set Triangulation
  • Definition 6: Bounding Set
  • Example 1
  • Definition 7: Polyhedron formed by Bounding Set
  • Definition 8: Polyhedral Enclosure
  • Example 2
  • ...and 34 more