Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations

• URL: http://arxiv.org/abs/2605.07757v1
• Date: Fri, 08 May 2026 13:59:53 GMT
• Title: Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations
• Abstract summary: We propose LightCROWN, which computes tighter Jacobian bounds by exploiting the analytical properties of activation functions.<n>Experiments on nonlinear control systems demonstrate that LightCROWN improves success rates up to 100%, while enhancing speed and scalability.
• Score: 11.170776418209117
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: 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.

Related papers

• Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial [23.69448525306035]
  $,!$-CROWN is a general-purpose bounding engine for nonlinear functions represented as graphs.<n>In this tutorial, we discuss the basics of $,!$-CROWN and introduce its application to various control-related computation tasks.
  arXiv  Detail & Related papers  (2026-05-26T05:49:19Z)
• Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation [50.53301323864253]
  Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems.<n>We present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF.<n>Our approach scales to larger neural networks than state-of-the-art verification procedures for CBFs.
  arXiv  Detail & Related papers  (2025-11-09T11:51:15Z)
• Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation [6.987300771372427]
  We propose a new efficient verification framework for ReLU-based neural CBFs. We show that the symbolic bounds can be propagated through the inner product of neural CBF Jacobian and nonlinear system dynamics.
  arXiv  Detail & Related papers  (2024-10-04T21:42:25Z)
• Data-Driven Stochastic Optimal Control in Reproducing Kernel Hilbert Spaces [4.722936792899906]
  This paper proposes a fully data-driven approach for optimal control of nonlinear control-affine systems represented by a diffusion.<n>The focus is on the scenario where both the nonlinear dynamics and stage cost functions are unknown, while only a control penalty function and constraints are provided.<n> Numerical results demonstrate its ability to address diverse nonlinear control tasks, including the depth regulation of an autonomous underwater vehicle.
  arXiv  Detail & Related papers  (2024-07-23T11:53:03Z)
• Safe Neural Control for Non-Affine Control Systems with Differentiable Control Barrier Functions [58.19198103790931]
  This paper addresses the problem of safety-critical control for non-affine control systems. It has been shown that optimizing quadratic costs subject to state and control constraints can be sub-optimally reduced to a sequence of quadratic programs (QPs) by using Control Barrier Functions (CBFs) We incorporate higher-order CBFs into neural ordinary differential equation-based learning models as differentiable CBFs to guarantee safety for non-affine control systems.
  arXiv  Detail & Related papers  (2023-09-06T05:35:48Z)
• Globally Optimal Training of Neural Networks with Threshold Activation Functions [63.03759813952481]
  We study weight decay regularized training problems of deep neural networks with threshold activations. We derive a simplified convex optimization formulation when the dataset can be shattered at a certain layer of the network.
  arXiv  Detail & Related papers  (2023-03-06T18:59:13Z)
• Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers [5.543220407902113]
  This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system.
  arXiv  Detail & Related papers  (2023-01-19T06:46:36Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety. We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior.
  arXiv  Detail & Related papers  (2021-11-18T23:21:00Z)
• Learning the Linear Quadratic Regulator from Nonlinear Observations [135.66883119468707]
  We introduce a new problem setting for continuous control called the LQR with Rich Observations, or RichLQR. In our setting, the environment is summarized by a low-dimensional continuous latent state with linear dynamics and quadratic costs. Our results constitute the first provable sample complexity guarantee for continuous control with an unknown nonlinearity in the system model and general function approximation.
  arXiv  Detail & Related papers  (2020-10-08T07:02:47Z)
• Learning Control Barrier Functions from Expert Demonstrations [69.23675822701357]
  We propose a learning based approach to safe controller synthesis based on control barrier functions (CBFs) We analyze an optimization-based approach to learning a CBF that enjoys provable safety guarantees under suitable Lipschitz assumptions on the underlying dynamical system. To the best of our knowledge, these are the first results that learn provably safe control barrier functions from data.
  arXiv  Detail & Related papers  (2020-04-07T12:29:06Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.