# Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations

arXiv: https://arxiv.org/abs/2605.07757 · HTML: https://mlsanity.com/paper/2605.07757/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 24 references that are in the map.
- First posted on arXiv 8 May 2026.

## Builds on (most cited first, 14 of 14)

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Safe Control Under Input Limits with Neural Control Barrier Functions](https://mlsanity.com/paper/2211.11056/) (2022)
- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation](https://mlsanity.com/paper/2410.16281/) (2024)
- [Learning a Formally Verified Control Barrier Function in Stochastic Environment](https://mlsanity.com/paper/2403.19332/) (2024)
- [Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees](https://mlsanity.com/paper/2403.07308/) (2024)
- [Simultaneous Synthesis and Verification of Neural Control Barrier Functions through Branch-and-Bound Verification-in-the-loop Training](https://mlsanity.com/paper/2311.10438/) (2023)
- [Real-Time Safe Control of Neural Network Dynamic Models with Sound Approximation](https://mlsanity.com/paper/2404.13456/) (2024)
- [Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation](https://mlsanity.com/paper/2511.06341/) (2025)
- [Dynamic Collision Avoidance Using Velocity Obstacle-Based Control Barrier Functions](https://mlsanity.com/paper/2503.00606/) (2025)

## Abstract (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.