Extracting Forward Invariant Sets from Neural Network-Based Control Barrier Functions

TL;DR

The paper tackles the challenge of provably certifying neural-network barrier functions for discrete-time systems by identifying a forward-invariant subset of safe states. It proposes a sound two-step approach: (i) use NN forward reachability to locate a region where the BF decreases along dynamics, and (ii) employ an incremental hyperplane-region enumeration to extract a connected component of the BF zero-sub-level that lies within this region and certify it as forward invariant. The method leverages the piecewise-affine structure of shallow ReLU networks, CROWN-based linear relaxations for bounds, and efficient region-enumeration to deliver certificates. Case studies on an inverted pendulum and a steerable bicycle demonstrate practical success and the scalability analysis shows predictable growth trends with network size and input dimension. Overall, the work provides a computationally efficient, sound certification pipeline that can yield provable BF subsets for learned safety certificates in real-world systems.

Abstract

Training Neural Networks (NNs) to serve as Barrier Functions (BFs) is a popular way to improve the safety of autonomous dynamical systems. Despite significant practical success, these methods are not generally guaranteed to produce true BFs in a provable sense, which undermines their intended use as safety certificates. In this paper, we consider the problem of formally certifying a learned NN as a BF with respect to state avoidance for an autonomous system: viz. computing a region of the state space on which the candidate NN is provably a BF. In particular, we propose a sound algorithm that efficiently produces such a certificate set for a shallow NN. Our algorithm combines two novel approaches: it first uses NN reachability tools to identify a subset of states for which the output of the NN does not increase along system trajectories; then, it uses a novel enumeration algorithm for hyperplane arrangements to find the intersection of the NN's zero-sub-level set with the first set of states. In this way, our algorithm soundly finds a subset of states on which the NN is certified as a BF. We further demonstrate the effectiveness of our algorithm at certifying for real-world NNs as BFs in two case studies. We complemented these with scalability experiments that demonstrate the efficiency of our algorithm.

Figures (8)

• Figure 1: Illustration of the need for a backward pass to identify zero-sub-level sets of a shallow ${\mathscr{N}}$. Top: Shallow NN hyperplane arrangement. The zero sub-level set is shaded gray; $R_0$ is the base region of the arrangement; hyperplane indices are shown in blue on the "positive" side; $\mathcal{T}^{{\mathscr{N}}}_R(x)= 0$ hyperplanes are shown as dashed lines. A table shows $\mathfrak{F}_{ \{\cdot\}}(R)$ for each labeled region Bottom: Corresponding Region Poset (Partial). Full dimensional regions are shown as nodes; full-dimension faces as lines between nodes.
• Figure 2: Certified forward invariant sets are shown in green for the inverted pendulum case study (Left) and steerable bicycle case study (Right); both sets are contained the set of safe states $X_s$, as defined in each case study ($X_s$ is shown as a white/grey box). The green sets are zero-sub-level sets of the trained ${\mathscr{N}}_{\text{BF}}$, and are returned by our algorithm.
• Figure 3: Zero-sub-level Set Verification Time
• Figure 4: Zero-sub-level Set Verification Time
• Figure : Recursive identification of $X_\partial$ for \ref{['prob:neg_deriv_prob']}

Theorems & Definitions (30)

• Definition 1: Shallow NN
• Definition 2: Local Linear Function
• Theorem 1: Barrier Function
• Remark 1
• Definition 3: Hyperplanes and Half-spaces
• Definition 4: Hyperplane Arrangement
• Definition 5: Region of a Hyperplane Arrangement
• Definition 6: Face of a Region
• Definition 7: Flipped/Unflipped Hyperplanes of a Region
• Definition 8: Base Region