This is the official code for CoRL 2024 work "Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation".
The code is based on Julia and is tested with Julia v1.9.4. Check here to install Julia environment. Install ModelVerification.jl
from this repo and check out the branch verify_gradient
here. Install RobotZoo.jl
from this repo and TaylorModels.jl
from here.
To collect data for each robot dynamics, see Jupyter file collect_data.ipynb
for details.
For the model training under Point Robot, see Jupyter file train_naive_point.ipynb
for regular training and train_adv_point.ipynb
for adversarial training. For the model training under Dubins Car, see Jupyter file train_naive_car.ipynb
for regular training and train_adv_car.ipynb
for adversarial training. For the model training under Planar Quadrotor, see Jupyter file train_naive_planar_quad.ipynb
for regular training and train_adv_planar_quad.ipynb
for adversarial training.
For the verificaiton under Dubins Car, see Jupyter file verify_car.ipynb
. Similarly, verify_point.ipynb
is for point robot and verify_planar_quad.ipynb
is for planar quadrotor. Replace the corresponding path with naive
or adv
for different pre-trained models. Also, max_iter=1
in BFS
mehtod to specify NNCB-IBP and otherwise, it is for BBV baseline.
If you find the repo useful, please cite:
H. Hu, Y. Yang, T. Wei and C. Liu "Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation", Conference on Robot Learning (CoRL). PMLR, 2024
@inproceedings{
hu2024verification,
title={Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation},
author={Hanjiang Hu and Yujie Yang and Tianhao Wei and Changliu Liu},
booktitle={8th Annual Conference on Robot Learning},
year={2024},
url={https://openreview.net/forum?id=jnubz7wB2w}
}