This repository contains the implementation of SEEV (Synthesis with Efficient Exact Verification), a novel framework for synthesizing Neural Control Barrier Functions (NCBFs) with ReLU activations and performing efficient safety verification. The SEEV approach integrates synthesis and verification to reduce computational overhead while maintaining safety guarantees for autonomous systems. It includes algorithms for training NCBFs with regularization and efficient verification of safety conditions across benchmark systems.
To install requirements and set up for the project:
pip install -r requirements.txt
[Inside NCBCV] pip install -e .
[Inside neural_clbf_ncbcv] pip install -e .
Note that the directory neural_clbf_ncbcv is adapted from https://github.com/MIT-REALM/neural_clbf.
The commands for trainig the CBFs are located in neural_clbf_ncbcv/darboux_commands.txt, neural_clbf_ncbcv/obs_avoid_commands.txt, neural_clbf_ncbcv/linear_satellite_commands.txt and neural_clbf_ncbcv/high_o_commands.txt. The commands in these files are properly seeded, with hyperparameters specified accordingly.
To perform certification, run the commands located in neural_clbf_ncbcv/certify_commands.sh, which evaluates pretrained models located in neural_clbf_ncbcv/models. The metrics reported in the paper will be outputs to stdout.
If you find this repository useful in your research, please consider citing:
@inproceedings{
anonymous2024seev,
title={{SEEV}: Synthesis with Efficient Exact Verification for Re{LU} Neural Barrier Functions},
author={Anonymous},
booktitle={The Thirty-eighth Annual Conference on Neural Information Processing Systems},
year={2024},
url={https://openreview.net/forum?id=nWMqQHzI3W}
}