Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Verification and Falsification of ReLU Neural Barrier Certificates

Dejin Ren, Yiling Xue, Taoran Wu, Bai Xue

TL;DR

This work addresses safety verification for continuous-time systems by introducing ReLU neural barrier certificates and a necessary and sufficient condition for their positive invariance. The condition is formulated on a per-valid-linear-region basis using Bouligand/Clarke tangent cones, avoiding derivative assumptions about ReLUs and enabling both verification and falsification via SMT and optimization. A boundary propagation algorithm efficiently enumerates a limited set of valid regions, and an IBP-based initialization seeds the search for initial regions. Empirical results demonstrate accurate verification and falsification across multiple systems, with improved scalability and reliability over prior methods, making ReLU neural barrier certificates more practical for safety-critical applications.

Abstract

Barrier certificates play an important role in verifying the safety of continuous-time systems, including autonomous driving, robotic manipulators and other critical applications. Recently, ReLU neural barrier certificates -- barrier certificates represented by the ReLU neural networks -- have attracted significant attention in the safe control community due to their promising performance. However, because of the approximate nature of neural networks, rigorous verification methods are required to ensure the correctness of these certificates. This paper presents a necessary and sufficient condition for verifying the correctness of ReLU neural barrier certificates. The proposed condition can be encoded as either an Satisfiability Modulo Theories (SMT) or optimization problem, enabling both verification and falsification. To the best of our knowledge, this is the first approach capable of falsifying ReLU neural barrier certificates. Numerical experiments demonstrate the validity and effectiveness of the proposed method in both verifying and falsifying such certificates.

Efficient Verification and Falsification of ReLU Neural Barrier Certificates

TL;DR

This work addresses safety verification for continuous-time systems by introducing ReLU neural barrier certificates and a necessary and sufficient condition for their positive invariance. The condition is formulated on a per-valid-linear-region basis using Bouligand/Clarke tangent cones, avoiding derivative assumptions about ReLUs and enabling both verification and falsification via SMT and optimization. A boundary propagation algorithm efficiently enumerates a limited set of valid regions, and an IBP-based initialization seeds the search for initial regions. Empirical results demonstrate accurate verification and falsification across multiple systems, with improved scalability and reliability over prior methods, making ReLU neural barrier certificates more practical for safety-critical applications.

Abstract

Barrier certificates play an important role in verifying the safety of continuous-time systems, including autonomous driving, robotic manipulators and other critical applications. Recently, ReLU neural barrier certificates -- barrier certificates represented by the ReLU neural networks -- have attracted significant attention in the safe control community due to their promising performance. However, because of the approximate nature of neural networks, rigorous verification methods are required to ensure the correctness of these certificates. This paper presents a necessary and sufficient condition for verifying the correctness of ReLU neural barrier certificates. The proposed condition can be encoded as either an Satisfiability Modulo Theories (SMT) or optimization problem, enabling both verification and falsification. To the best of our knowledge, this is the first approach capable of falsifying ReLU neural barrier certificates. Numerical experiments demonstrate the validity and effectiveness of the proposed method in both verifying and falsifying such certificates.

Paper Structure

This paper contains 30 sections, 15 theorems, 44 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Notation
  4. ReLU Neural Network
  5. Positive Invariance and Barrier Certificate
  6. Tangent Cones and Invariance Conditions
  7. Verification Algorithm
  8. Searching for an Initial Valid Linear Region
  9. Valid Test
  10. Boundary Propagation Algorithm
  11. Verification and Falsification in Each Valid Linear Region
  12. the Positively Invariant Condition
  13. the Initial and Unsafe Set Conditions
  14. Experiments
  15. Conclusion
  16. ...and 15 more sections

Key Result

Lemma 1

Let $\mathcal{X}(\mathscr{C})$ denote the set of inputs that activate a particular set of neurons represented by the activation indicator $\mathscr{C}$. For notational consistency, we define $\overline{\bm{W}}_0(\mathscr{C})$ as the identity matrix and $\bar{\bm{b}}_0(\mathscr{C})$ as the zero vecto

Figures (3)

  • Figure 1: Illustration of tangent cones at a nonsmooth boundary point
  • Figure 2: Illustration of enumerating valid linear regions: We begin by randomly selecting two points---one from the initial set (colored in green) and one from the unsafe set (colored in red)---and iteratively shrinking the segment connecting them until an initial valid linear region is found. The boundary propagation algorithm then expands from this region to identify neighboring valid linear regions. By iteratively applying this propagation step, the algorithm eventually enumerates all valid linear regions.
  • Figure 3: Enumerated valid linear regions and the vector fields of system Arch3.

Theorems & Definitions (36)

  • Lemma 1: zhang2023exact
  • Definition 1: Positive invariance
  • Definition 2: Barrier certificate
  • Remark 1
  • Definition 3: Distance
  • Definition 4: Tangent cones clarke2008nonsmoothaubin2009set
  • Theorem 1: clarke2008nonsmooth
  • Definition 5: Valid linear region
  • Proposition 1
  • Proposition 2
  • ...and 26 more