Exact Verification of ReLU Neural Control Barrier Functions
Authors: Hongchao Zhang, Junlin Wu, Yevgeniy Vorobeychik, Andrew Clark
NeurIPS 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We evaluate our approach through numerical studies with comparison to state-of-the-art SMT-based methods. |
| Researcher Affiliation | Academia | Hongchao Zhang Electrical & Systems Engineering Washington University in St. Louis St. Louis, MO 63130 hongchao@wustl.edu Junlin Wu Computer Science & Engineering Washington University in St. Louis St. Louis, MO 63130 junlin.wu@wustl.edu Yevgeniy Vorobeychik Computer Science & Engineering Washington University in St. Louis St. Louis, MO 63130 yvorobeychik@wustl.edu Andrew Clark Electrical & Systems Engineering Washington University in St. Louis St. Louis, MO 63130 andrewclark@wustl.edu |
| Pseudocode | No | The paper describes the steps of its verification algorithm in prose, but it does not include any formally structured pseudocode or algorithm blocks. |
| Open Source Code | Yes | Our code is available at https: //github.com/Hongchao Zhang-HZ/exactverif-reluncbf-nips23. |
| Open Datasets | No | The paper evaluates its method on several control systems (Darboux, Obstacle Avoidance, Spacecraft Rendezvous, hi-ord8) whose dynamics are defined or referenced, and mentions training NCBFs using methods from prior work ([13], [24]). However, it does not provide explicit access information (link, DOI, specific repository, or citation to a dataset resource) for a publicly available dataset used in its experiments. |
| Dataset Splits | No | The paper does not explicitly provide training/test/validation dataset splits. It describes the systems used for verification but not data partitioning for model training. |
| Hardware Specification | Yes | The experiments run on a 64-bit Windows PC with Intel i7-12700 processor, 32GB RAM and NVIDIA Ge Force RTX 3080 GPU. |
| Software Dependencies | No | The paper mentions software components such as FOSSIL, d Real, Z3, auto-Li RPA, and SciPy, but does not provide specific version numbers for these tools in the text. |
| Experiment Setup | Yes | We include experiment details in the supplement. Section A.13 'Training Details' provides specific hyperparameters for training NCBFs in Table 3a and Table 3b, including LEARNING_RATE, EPOCHS, BATCH_SIZE, and CBF_HIDDEN_SIZE. |