# Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Builds on 43 of its 63 references that are in the map.
- First posted on arXiv 4 Oct 2024.

## Builds on (most cited first, 30 of 43)

- [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)
- [End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Tasks](https://mlsanity.com/paper/1903.08792/) (2019)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021)
- [Lyapunov-stable neural-network control](https://mlsanity.com/paper/2109.14152/) (2021)
- [State-wise Safe Reinforcement Learning: A Survey](https://mlsanity.com/paper/2302.03122/) (2023)
- [Certified Training: Small Boxes are All You Need](https://mlsanity.com/paper/2210.04871/) (2022)
- [Fast Certified Robust Training with Short Warmup](https://mlsanity.com/paper/2103.17268/) (2021)
- [Learning Stability Certificates from Data](https://mlsanity.com/paper/2008.05952/) (2020)
- [Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation](https://mlsanity.com/paper/2210.07394/) (2022)
- [How to Train Your Neural Control Barrier Function: Learning Safety Filters for Complex Input-Constrained Systems](https://mlsanity.com/paper/2310.15478/) (2023)
- [Control Barrier Functions for Systems with High Relative Degree](https://mlsanity.com/paper/1903.04706/) (2019)
- [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)
- [Learning Hybrid Control Barrier Functions from Data](https://mlsanity.com/paper/2011.04112/) (2020)
- [Safe Control with Neural Network Dynamic Models](https://mlsanity.com/paper/2110.01110/) (2021)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [ShieldNN: A Provably Safe NN Filter for Unsafe NN Controllers](https://mlsanity.com/paper/2006.09564/) (2020)
- [Model-Based Control with Sparse Neural Dynamics](https://mlsanity.com/paper/2312.12791/) (2023)
- [Probabilistic Safeguard for Reinforcement Learning Using Safety Index Guided Gaussian Process Models](https://mlsanity.com/paper/2210.01041/) (2022)
- [Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions](https://mlsanity.com/paper/2206.07811/) (2022)
- [Convex synthesis and verification of control-Lyapunov and barrier functions with input constraints](https://mlsanity.com/paper/2210.00629/) (2022)
- [Exact Verification of ReLU Neural Control Barrier Functions](https://mlsanity.com/paper/2310.09360/) (2023)

## Built on by (most cited first, 12 of 12)

- [Steering Dialogue Dynamics for Robustness against Multi-turn Jailbreaking Attacks](https://mlsanity.com/paper/2503.00187/) (2025)
- [Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks](https://mlsanity.com/paper/2506.15693/) (2025)
- [Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control](https://mlsanity.com/paper/2411.18235/) (2024)
- [Designing Control Barrier Function via Probabilistic Enumeration for Safe Reinforcement Learning Navigation](https://mlsanity.com/paper/2504.21643/) (2025)
- [Reachability Barrier Networks: Learning Hamilton-Jacobi Solutions for Smooth and Flexible Control Barrier Functions](https://mlsanity.com/paper/2505.11755/) (2025)
- [Learning Ensembles of Vision-based Safety Control Filters](https://mlsanity.com/paper/2412.02029/) (2024)
- [Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation](https://mlsanity.com/paper/2511.06341/) (2025)
- [Safe PDE Boundary Control with Neural Operators](https://mlsanity.com/paper/2411.15643/) (2024)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verification](https://mlsanity.com/paper/2511.11699/) (2025)
- [Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations](https://mlsanity.com/paper/2605.07757/) (2026)
- [A Survey on the Verification of Reinforcement Learning Policies](https://mlsanity.com/paper/2607.16210/) (2026)

## Abstract (arXiv)

Control barrier functions (CBFs) are important in safety-critical systems and robot control applications. Neural networks have been used to parameterize and synthesize CBFs with bounded control input for complex systems. However, it is still challenging to verify pre-trained neural networks CBFs (neural CBFs) in an efficient symbolic manner. To this end, we propose a new efficient verification framework for ReLU-based neural CBFs through symbolic derivative bound propagation by combining the linearly bounded nonlinear dynamic system and the gradient bounds of neural CBFs. Specifically, with Heaviside step function form for derivatives of activation functions, we show that the symbolic bounds can be propagated through the inner product of neural CBF Jacobian and nonlinear system dynamics. Through extensive experiments on different robot dynamics, our results outperform the interval arithmetic based baselines in verified rate and verification time along the CBF boundary, validating the effectiveness and efficiency of the proposed method with different model complexity. The code can be found at https://github.com/intelligent-control-lab/ verify-neural-CBF.