# SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions

## Requirements

To install requirements and set up for the project:

```setup
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. 

## Training

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.

## Evaluation

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.