SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions
Authors: Hongchao Zhang, Zhizhen Qin, Sicun Gao, Andrew Clark
NeurIPS 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our simulations show that SEEV significantly improves verification efficiency while maintaining the CBF quality across various benchmark systems and neural network structures. Our simulation results demonstrate significant improvements in verification efficiency and reliability across a range of benchmark systems. In this section, we evaluate the proposed SEEV in regularizer efficacy and verification efficiency. We also demonstrated the improved performance with counter-example guidance in the synthesis framework, whose results are detailed in B.2. We experiment on four systems, namely Darboux, obstacle avoidance, hi-ord8, and spacecraft rendezvous. |
| Researcher Affiliation | Academia | Hongchao Zhang Electrical & Systems Engineering Washington University in St. Louis hongchao@wustl.edu Zhizhen Qin Computer Science & Engineering University of California, San Diego zhizhenqin@ucsd.edu Sicun Gao Computer Science & Engineering University of California, San Diego scungao@ucsd.edu Andrew Clark Electrical & Systems Engineering Washington University in St. Louis andrewclark@wustl.edu |
| Pseudocode | Yes | Algorithm 1 Efficient Exact Verification; Algorithm 2 Binary Search for S0; Algorithm 3 Enumerate Activated Sets; Algorithm 4 Enumerate Hinges |
| Open Source Code | Yes | Our code is available at https://github.com/Hongchao Zhang-HZ/SEEV. |
| Open Datasets | No | The training dataset T is initialized by uniform sampling over X. |
| Dataset Splits | No | The paper initializes its training dataset by uniform sampling and updates it with counterexamples, but does not define fixed train/validation/test dataset splits with percentages or counts. |
| Hardware Specification | Yes | The experiments run on a workstation with an Intel i7-11700KF CPU, and an NVIDIA Ge Force RTX 3080 GPU. |
| Software Dependencies | No | The paper mentions tools like 'd Real' and 'Z3' but does not specify version numbers for general software dependencies or libraries. |
| Experiment Setup | Yes | We include experiment settings in Appendix B.1 and hyperparameters settings in Table 4 in Appendix B.3. |