Stochastic Neural Control Barrier Functions

Hongchao Zhang; Manan Tayal; Jackson Cox; Pushpak Jagtap; Shishir Kolathaya; Andrew Clark

eess.SYJun 26, 2025

Stochastic Neural Control Barrier Functions

Authors: Hongchao Zhang, Manan Tayal, Jackson Cox, Pushpak Jagtap, Shishir Kolathaya, Andrew Clark

Organizations: Electrical and Systems Engineering Department, McKelvey School of Engineering, Washington University in St. Louis, St. Louis, MO 63130 USA · Center for Cyber-Physical Systems, Indian Institute of Science (IISc), Bengaluru.

Abstract

Control Barrier Functions (CBFs) are utilized to ensure the safety of control systems. CBFs act as safety filters in order to provide safety guarantees without compromising system performance. These safety guarantees rely on the construction of valid CBFs. Due to their complexity, CBFs can be represented by neural networks, known as neural CBFs (NCBFs). Existing works on the verification of the NCBF focus on the synthesis and verification of NCBFs in deterministic settings, leaving the stochastic NCBFs (SNCBFs) less studied. In this work, we propose a verifiably safe synthesis for SNCBFs. We consider the cases of smooth SNCBFs with twice-differentiable activation functions and SNCBFs that utilize the Rectified Linear Unit or ReLU activation function. We propose a verification-free synthesis framework for smooth SNCBFs and a verification-in-the-loop synthesis framework for both smooth and ReLU SNCBFs. and we validate our frameworks in three cases, namely, the inverted pendulum, Darboux, and the unicycle model.

Figures & tables

Symbol	Description	Symbol	Description
$\mathcal{X}$	State space	$\alpha(\cdot)$	Class $\mathcal{K}$ function
$\mathcal{X}_{S}$	Safe set	$V$	Diffusion coefficient
$\mathcal{X}_{U}$	Unsafe set	$f,g$	Drift, control vector fields
$\mathcal{X}_{I}$	Initial safe set	$\theta$	Neural-network parameters
$\mathcal{D}$	Super-0-level set of $B(\mathbf{x})$	$N$	Sample size
$B(\mathbf{x})$	CBF candidate	$\bar{\epsilon}$	Sampling radius

TABLE I : Notation Table

Fig. 1 : Workflow of the synthesis with verification in the loop.

Panel of Figure 3 — Fig. 2 : Experimental results on the inverted pendulum. (a) $B(\mathbf{x})$ over $\mathcal{X}$ : blue and red denote the safe ( $B\geq-\psi^{*}$ ) and unsafe ( $B<\psi^{*}$ ) regions; black boxes mark the initial safe and unsafe boundaries, and the trained SNCBF boundary (black dots) separates them. (b) 3D plot of $B(\mathbf{x})$ over $\mathcal{X}$ . (c) Trajectories initialized in the safe set under SNCBF-QP with different reference controllers.

Fig. 3 : Vehicle trajectories under the SNCBF-QP controller at reaction distances of $6$ , $8$ , and $12$ m from the pedestrian; all successfully maneuver to avoid the pedestrian.

	Baseline	Smooth SNCBF
Verifiability	No	Yes
Coverage	$14.8\%$	$72.5\%$
Training Time	$39.4$ minutes	$64.2$ minutes

TABLE II : Comparison of baseline and smooth SNCBF synthesis proposed in Algorithm 1 .

$N$	$5.4\times 10^{7}$	$2\times 10^{6}$	$2.5\times 10^{5}$	$3.12\times 10^{4}$	$2\times 10^{3}$
$\psi$	$-0.04$	$-0.13$	$-0.25$	$-0.49$	$-1.20$
$T_{s}$	64.2	26.5	17.3	12.1	7.25
$r_{c}$	78.65%	78.20%	76.53%	76.72%	72.66%

TABLE III : Sensitivity analysis of sampling budget

N

(and implicitly

\bar{\epsilon}

) on the unicycle system.

Control Barrier Functions

Control barrier functions encode safe states as constraints that keep a controlled system away from hazards.

See all 158 papers

Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations
May 8, 2026Jun Zhang, Haibo Zhang, Chun Liu +2Neural Network Verification Control Barrier Functions
School of Mechatronic Engineering and Automation, Shanghai University, Shanghai, China · Beijing Institute of Control Engineering, Beijing, China · School of Mechatronic Engineering and Automation, Shanghai2026 University, Shanghai, China +1
VertexCBF: Improving Neural Control Barrier Functions via Vertex-Restricted Control Search
Sep 11, 2026Bojan Derajić, Sebastian Bernhard, Wolfgang HönigControl Barrier Functions Safe Robot Navigation
Technical University of Berlin, Germany · AUMOVIO, Germany · Technical University of Applied Sciences Augsburg, Germany +1
Synthesis and Deployment of Maximal Robust Control Barrier Functions through Adversarial Reinforcement Learning
Apr 14, 2026Donggeon David Oh, Duy P. Nguyen, Haimin Hu +1Adversarial MARL Control Barrier Functions
Department of Electrical and Computer Engineering, Princeton University, Princeton, NJ 08540, USA · Department of Computer Science, Johns Hopkins University, Baltimore, MD 21218, USA

May 8, 2026J/K move · Enter open · S save

Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations

Jun Zhang, Haibo Zhang, Chun Liu, Xiaofan Wang+1

School of Mechatronic Engineering and Automation, Shanghai University, Shanghai, China · Beijing Institute of Control Engineering, Beijing, China · School of Mechatronic Engineering and Automation, Shanghai2026 University, Shanghai, China+1

Neural Network Verification Control Barrier Functions

Open paper AskPDF arXiv

Formal verification of neural control barrier functions (NCBFs) remains challenging, especially for neural networks with nonlinear activations like

\tanh

. Existing CROWN-based methods rely on conservative linear relaxations for Jacobian bounds, limiting scalability. We propose LightCROWN, which computes tighter Jacobian bounds by exploiting the analytical properties of activation functions. Experiments on nonlinear control systems including the inverted pendulum, Dubins car, and planar quadrotor demonstrate that LightCROWN improves verification success rates up to 100%, while enhancing speed and scalability. Our approach provides a generalizable improvement for CROWN-based frameworks, enabling more efficient verification of complex NCBFs. The code can be found at github.com/Autonomous-Systems-and-Control-Lab/verify-neural-CBF.

Abstract

Control Barrier Functions

Explore similar work

Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations

VertexCBF: Improving Neural Control Barrier Functions via Vertex-Restricted Control Search

Synthesis and Deployment of Maximal Robust Control Barrier Functions through Adversarial Reinforcement Learning