Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation
Not on the map. Why?
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.
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
43 of 63 references.
References · 43
- 2017Towards Deep Learning Models Resistant to Adversarial Attackscited by 6,415
- 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 445
- 2019Control Barrier Functions: Theory and Applicationscited by 372
- 2019End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Taskscited by 289
- 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 228
- 2019Algorithms for Verifying Deep Neural Networkscited by 221
- 2019Towards Stable and Efficient Training of Verifiably Robust Neural Networkscited by 205
- 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
- 2022Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methodscited by 151
- 2020Neural Lyapunov Controlcited by 142
- 2021Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functionscited by 94
- 2021Lyapunov-stable neural-network controlcited by 66
31 more
- 2023State-wise Safe Reinforcement Learning: A Surveycited by 55
- 2022Certified Training: Small Boxes are All You Needcited by 52
- 2021Fast Certified Robust Training with Short Warmupcited by 46
- 2020Learning Stability Certificates from Datacited by 45
- 2022Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagationcited by 45
- 2023How to Train Your Neural Control Barrier Function: Learning Safety Filters for Complex Input-Constrained Systemscited by 44
- 2019Control Barrier Functions for Systems with High Relative Degreecited by 31
- 2022Safe Control Under Input Limits with Neural Control Barrier Functionscited by 29
- 2024Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulationcited by 25
- 2020Learning Hybrid Control Barrier Functions from Datacited by 24
- 2021Safe Control with Neural Network Dynamic Modelscited by 22
- 2022Safety Certification for Stochastic Systems via Neural Barrier Functionscited by 22
- 2020ShieldNN: A Provably Safe NN Filter for Unsafe NN Controllerscited by 17
- 2023Model-Based Control with Sparse Neural Dynamicscited by 16
- 2022Probabilistic Safeguard for Reinforcement Learning Using Safety Index Guided Gaussian Process Modelscited by 15
- 2022Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functionscited by 14
- 2022Convex synthesis and verification of control-Lyapunov and barrier functions with input constraintscited by 14
- 2023Exact Verification of ReLU Neural Control Barrier Functionscited by 14
- 2021Verification and Synthesis of Control Barrier Functionscited by 13
- 2024Learning a Formally Verified Control Barrier Function in Stochastic Environmentcited by 11
- 2016Correctness Guarantees for the Composition of Lane Keeping and Adaptive Cruise Controlcited by 7
- 2024Verification-Aided Learning of Neural Network Barrier Functions with Termination Guaranteescited by 7
- 2022Learning a Better Control Barrier Functioncited by 6
- 2023Simultaneous Synthesis and Verification of Neural Control Barrier Functions through Branch-and-Bound Verification-in-the-loop Trainingcited by 6
- 2022Automatically Bounding the Taylor Remainder Series: Tighter Bounds and New Applicationscited by 5
- 2024Real-Time Safe Control of Neural Network Dynamic Models with Sound Approximationcited by 5
- 2021High Relative Degree Control Barrier Functions Under Input Constraintscited by 3
- 2023Verification and Synthesis of Robust Control Barrier Functions: Multilevel Polynomial Optimization and Semidefinite Relaxationcited by 3
- 2023SOS Construction of Compatible Control Lyapunov and Barrier Functionscited by 3
- 2023Neural Differentiable Integral Control Barrier Functions for Unknown Nonlinear Systems with Input Constraintscited by 3
- 2024The Feasibility Theory of Constrained Reinforcement Learning: A Tutorial Studycited by 1
Built on by
Citing papers per year: 2024: 3; 2025: 6; 2026: 3.
12 papers.
- 2025Steering Dialogue Dynamics for Robustness against Multi-turn Jailbreaking Attackscited by 20
- 2025Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networkscited by 5
- 2024Certified Training with Branch-and-Bound for Lyapunov-stable Neural Controlcited by 3
- 2025Designing Control Barrier Function via Probabilistic Enumeration for Safe Reinforcement Learning Navigationcited by 3
- 2025Reachability Barrier Networks: Learning Hamilton-Jacobi Solutions for Smooth and Flexible Control Barrier Functionscited by 3
- 2024Learning Ensembles of Vision-based Safety Control Filterscited by 2
- 2025Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagationcited by 2
- 2024Safe PDE Boundary Control with Neural Operatorscited by 1
- 2026Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorialcited by 1
- 2025Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verificationcited by 0
- 2026Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activationscited by 0
- 2026A Survey on the Verification of Reinforcement Learning Policiescited by 0
- 2026Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial26 May 2026
- 2026A Survey on the Verification of Reinforcement Learning Policies14 May 2026
- 2026Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations8 May 2026
- 2025Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verification12 Nov 2025
- 2025Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation9 Nov 2025
- 2025Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks27 May 2025
- 2025Reachability Barrier Networks: Learning Hamilton-Jacobi Solutions for Smooth and Flexible Control Barrier Functions16 May 2025
- 2025Designing Control Barrier Function via Probabilistic Enumeration for Safe Reinforcement Learning Navigation30 Apr 2025
- 2025Steering Dialogue Dynamics for Robustness against Multi-turn Jailbreaking Attacks28 Feb 2025
- 2024Learning Ensembles of Vision-based Safety Control Filters2 Dec 2024
- 2024Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control27 Nov 2024
- 2024Safe PDE Boundary Control with Neural Operators23 Nov 2024