Learning a Formally Verified Control Barrier Function in Stochastic Environment

TL;DR

The paper addresses safety guarantees for continuous-time control in stochastic environments by learning a Stochastic Neural Control Barrier Function (SNCBF) that is formally verifiable in a single training step. It introduces a data-driven SOP framework with Lipschitz-certified neural networks to ensure safety constraints hold across the state space, eliminating post hoc verification. The approach yields a SNCBF and an accompanying SNCBF-QP controller, demonstrated on an inverted pendulum and obstacle avoidance tasks, achieving larger safe regions than baselines. This work advances safe learning-based control by providing formal guarantees under stochastic disturbances and scalable, offline training suitable for real-time deployment. The methods have practical impact for safety-critical autonomous systems where data-driven policies must be verifiably safe in continuous-time stochastic settings.

Abstract

Safety is a fundamental requirement of control systems. Control Barrier Functions (CBFs) are proposed to ensure the safety of the control system by constructing safety filters or synthesizing control inputs. However, the safety guarantee and performance of safe controllers rely on the construction of valid CBFs. Inspired by universal approximatability, CBFs are represented by neural networks, known as neural CBFs (NCBFs). This paper presents an algorithm for synthesizing formally verified continuous-time neural Control Barrier Functions in stochastic environments in a single step. The proposed training process ensures efficacy across the entire state space with only a finite number of data points by constructing a sample-based learning framework for Stochastic Neural CBFs (SNCBFs). Our methodology eliminates the need for post hoc verification by enforcing Lipschitz bounds on the neural network, its Jacobian, and Hessian terms. We demonstrate the effectiveness of our approach through case studies on the inverted pendulum system and obstacle avoidance in autonomous driving, showcasing larger safe regions compared to baseline methods.

Figures (3)

• Figure 1: This figure presents the experimental results on the inverted pendulum system. Fig. \ref{['fig:2d_sample']} visualizes of $\tilde{h}\left(x \mid \theta\right)$ over $X$. Blue and red regions denote the safe region ($\tilde{h} \geq -\psi^*$) and the unsafe region ($\tilde{h} < \psi^*$), respectively. The initial safety region boundary and unsafe region boundary is denoted by black boxes. We observe that the boundary of trained SNCBF (black dots) successfully separate the unsafe and safe region. Fig. \ref{['fig:3d_sncbf']} shows the 3D plot of $\tilde{h}\left(x \mid \theta\right)$ over $X$. We observe that the safe region is greater than zero while unsafe region has negative function value. Fig. \ref{['fig:ip_traj']} presents trajectories initiating inside the safe set following SNCBF-QP, following different reference controllers
• Figure 2: Proposed safe control comparison among different reaction distance. We let the vehicle to adjust its orientation to maneuver in its lane. We show three trajectories to demonstrate our proposed SNCBF-based controller under different initial state, namely, $6$, $8$ and $12$ meter away from the pedestrian, respectively. Three trajectories of the vehicle under control shows our proposed method succeeds in maneuvering the vehicle to avoid the pedestrian.
• Figure 3: The left and right figures show the unsafe region and the zero-level sets of the SNCBF $\tilde{h}$ trained by baseline and the proposed method, respectively. Both zero-level sets (in yellow) do not overlap with the unsafe region in red color. The SNCBF trained by the baseline ensures a guaranteed safe subset over the state space with the ratio $11.8\%$ only, whereas the proposed method ensures a guaranteed safe subset with a ratio up to $77.6\%$.

Theorems & Definitions (12)

• Definition 1: Safety
• Definition 2: Control barrier function (CBF)
• Lemma 1: clark2021verification
• Theorem 1
• proof
• Lemma 2: pauli2021training
• Remark 1
• Theorem 2
• proof
• Theorem 3