Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation

Hanjiang Hu, Yujie Yang, Tianhao Wei, Changliu Liu
Proceedings of The 8th Conference on Robot Learning, PMLR 270:1797-1814, 2025.

Abstract

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.

Cite this Paper

BibTeX
@InProceedings{pmlr-v270-hu25a, title = {Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation}, author = {Hu, Hanjiang and Yang, Yujie and Wei, Tianhao and Liu, Changliu}, booktitle = {Proceedings of The 8th Conference on Robot Learning}, pages = {1797--1814}, year = {2025}, editor = {Agrawal, Pulkit and Kroemer, Oliver and Burgard, Wolfram}, volume = {270}, series = {Proceedings of Machine Learning Research}, month = {06--09 Nov}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v270/main/assets/hu25a/hu25a.pdf}, url = {https://proceedings.mlr.press/v270/hu25a.html}, abstract = {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.} }
Endnote
%0 Conference Paper %T Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation %A Hanjiang Hu %A Yujie Yang %A Tianhao Wei %A Changliu Liu %B Proceedings of The 8th Conference on Robot Learning %C Proceedings of Machine Learning Research %D 2025 %E Pulkit Agrawal %E Oliver Kroemer %E Wolfram Burgard %F pmlr-v270-hu25a %I PMLR %P 1797--1814 %U https://proceedings.mlr.press/v270/hu25a.html %V 270 %X 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.
APA
Hu, H., Yang, Y., Wei, T. & Liu, C.. (2025). Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation. Proceedings of The 8th Conference on Robot Learning, in Proceedings of Machine Learning Research 270:1797-1814 Available from https://proceedings.mlr.press/v270/hu25a.html.

Related Material