Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions

Hongchao Zhang, Zhizhen Qin, Sicun Gao, Andrew Clark

TL;DR

A framework for Synthesis with Efficient Exact Verification (SEEV), which consists of an NCBF synthesis algorithm that introduces a novel regularizer to reduce the number of activation regions at the safety boundary and a verification algorithm that exploits tight over-approximations of the safety conditions to reduce the cost of verifying each piecewise-linear segment.

Abstract

Neural Control Barrier Functions (NCBFs) have shown significant promise in enforcing safety constraints on nonlinear autonomous systems. State-of-the-art exact approaches to verifying safety of NCBF-based controllers exploit the piecewise-linear structure of ReLU neural networks, however, such approaches still rely on enumerating all of the activation regions of the network near the safety boundary, thus incurring high computation cost. In this paper, we propose a framework for Synthesis with Efficient Exact Verification (SEEV). Our framework consists of two components, namely (i) an NCBF synthesis algorithm that introduces a novel regularizer to reduce the number of activation regions at the safety boundary, and (ii) a verification algorithm that exploits tight over-approximations of the safety conditions to reduce the cost of verifying each piecewise-linear segment. Our simulations show that SEEV significantly improves verification efficiency while maintaining the CBF quality across various benchmark systems and neural network structures. Our code is available at https://github.com/HongchaoZhang-HZ/SEEV.

SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions

TL;DR

A framework for Synthesis with Efficient Exact Verification (SEEV), which consists of an NCBF synthesis algorithm that introduces a novel regularizer to reduce the number of activation regions at the safety boundary and a verification algorithm that exploits tight over-approximations of the safety conditions to reduce the cost of verifying each piecewise-linear segment.

Abstract

Neural Control Barrier Functions (NCBFs) have shown significant promise in enforcing safety constraints on nonlinear autonomous systems. State-of-the-art exact approaches to verifying safety of NCBF-based controllers exploit the piecewise-linear structure of ReLU neural networks, however, such approaches still rely on enumerating all of the activation regions of the network near the safety boundary, thus incurring high computation cost. In this paper, we propose a framework for Synthesis with Efficient Exact Verification (SEEV). Our framework consists of two components, namely (i) an NCBF synthesis algorithm that introduces a novel regularizer to reduce the number of activation regions at the safety boundary, and (ii) a verification algorithm that exploits tight over-approximations of the safety conditions to reduce the cost of verifying each piecewise-linear segment. Our simulations show that SEEV significantly improves verification efficiency while maintaining the CBF quality across various benchmark systems and neural network structures. Our code is available at https://github.com/HongchaoZhang-HZ/SEEV.

Paper Structure

This paper contains 28 sections, 5 theorems, 25 equations, 3 figures, 5 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. System Model
  4. Neural Network Model and Notations
  5. Guaranteeing Safety via Control Barrier Functions
  6. Synthesis
  7. Overall Formulation
  8. Loss Function Design and NCBF Training
  9. Verification
  10. Enumeration of Hyperplanes and Hinges
  11. Efficient Verification
  12. Experiments
  13. Experiment Setup
  14. Regularizer Efficacy Evaluation
  15. Efficient Verification Evaluation
  16. ...and 13 more sections

Key Result

Theorem 1

A closed set $\mathcal{D}$ is controlled positive invariant if, whenever $x \in \partial \mathcal{D}$, where $\partial \mathcal{D}$ denotes the boundary of $\mathcal{D}$. we have for some $u \in \mathcal{U}$ where $\mathcal{A}_{\mathcal{D}}(x)$ is the tangent cone to $\mathcal{D}$ at $x$.

Figures (3)

  • Figure 1: SEEV: Synthesis with Efficient Exact Verifier for ReLU NCBF
  • Figure 2: Overview of the Efficient Exact Verifier for ReLU NCBFs
  • Figure 3: Effects of boundary regularization ($r$) on activation sets along the boundary. The figures show the results from a neural network with 4 layers of 8 hidden units, applied to the Spacecraft case. The surface represents the first two dimensions with the last four dimensions fixed at 0. Increasing $r$ results in more organized boundary activation sets.

Theorems & Definitions (7)

  • Theorem 1: Nagumo's Theorem blanchini2008set, Section 4.2
  • Proposition 1
  • Lemma 1
  • Proposition 2
  • Theorem 2
  • proof
  • proof