Research map / Learning theory and algorithms / Combinatorial and search optimization
SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes SEEV, a framework that trains ReLU neural control barrier functions with a regularizer penalizing activation-set dissimilarity along the boundary and verifies them with breadth-first enumeration of boundary linear segments plus sufficient-condition checks, yielding large speedups over prior exact verification.
Problem
Exact safety verification of ReLU neural control barrier functions requires enumerating and checking all linear activation regions at the safety boundary, which is computationally intractable for high-dimensional systems and large networks.
Approach
Co-designs synthesis and verification: a boundary-activation-set dissimilarity regularizer (using smoothed sigmoid activations and clustering) reduces the number of boundary hyperplanes/hinges to verify, while a neural breadth-first search enumerates boundary hyperplanes and hinges and uses tight linear over-approximations and cheap sufficient conditions before exact checks; counterexamples from t
Key results
- On Darboux with M=512, SEEV verifies in 3.3 s versus 631 s for the prior exact baseline, while dReal and Z3 exceed 3 hours.
- On spacecraft rendezvous (n=6, L=4, M=8), the regularizer reduces boundary hyperplanes from 6218 to 627 at r=50 while keeping the coverage ratio at 1.
- On hi-ord8 (8-D), SEEV finishes in at most 22.4 s while the baseline, dReal and Z3 time out.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use SEEV instead of the exact-verification baseline | ReLU NCBFs · Darboux, Obstacle Avoidance, hi-ord8, and Spacecraft Rendezvous | verification runtime: 315s vs 2.5s; 631s vs 3.3s; 16.0s vs 0.41s; 16.1s vs 0.39; 36.7s vs 0.65s; 207s vs 20.6s; >3h vs 0.54s; >3h vs 11.8s; >3 | Helped |
| add boundary activation-pattern regularizer (r=50) | SEEV NCBF synthesis · Spacecraft Rendezvous (n=6, L=4, M=8) | boundary hyperplanes: 6371 -> 627 | Helped |
| add boundary activation-pattern regularizer (r=50) | SEEV NCBF synthesis · Spacecraft Rendezvous (n=6, L=4, M=8) | relative safe-region coverage: 1 -> 1 | No clear effect |
| add counterexample-guided training | NCBF synthesis · Darboux and hi-ord8 | certification success rate: No CE 0/3; with CE 3/3, 1/3, 1/3, 2/3 on Darboux; hi-ord8 1/3, 0/3, 0/3, 0/3 -> 1/3, 2/3, 0/3, 2/3 | Helped |
| set λc to 1 or 10 instead of 100 (ablation) | SEEV synthesis, Spacecraft Rendezvous (L=4, N=8) · Spacecraft Rendezvous | certification success rate: 3/3 -> 0/3 | Hurt |
| set λc to 200 instead of 100 (ablation) | SEEV synthesis, Spacecraft Rendezvous (L=4, N=8) · Spacecraft Rendezvous | average first training epoch for valid NCBF: 17 -> 17.7 | Mixed |
| set λf to 8 instead of 2 (ablation) | SEEV synthesis, Spacecraft Rendezvous (L=4, N=8) · Spacecraft Rendezvous | certification success rate: 3/3 -> 2/3 | Hurt |
| set sigmoid parameter k to 8 instead of 4 (ablation) | SEEV boundary regularizer, Spacecraft Rendezvous (L=4, N=8) · Spacecraft Rendezvous | certification success rate: 3/3 -> 1/3 | Hurt |
| set sigmoid parameter k to 8 instead of 4 (ablation) | SEEV boundary regularizer, Spacecraft Rendezvous (L=4, N=8) · Spacecraft Rendezvous | average boundary hyperplanes: 3265 -> 1984 | Helped |
Surprising findings
- Counterexample-guided training with CE raised success rates on Darboux and hi-ord8 networks, where training without CE rarely produced a certifiable CBF (0/3 in most configurations).
Limitations
- Scalability to higher-dimensional systems remains challenging.
- Exact verification does not extend to non-ReLU NCBFs.
- Some configurations (e.g., SR with M=16) could not be fully verified before timeouts without regularization.
Experimental setup
Datasets: uniformly sampled states from the state space counterexamples generated by the verifier
Benchmarks: Darboux Obstacle Avoidance Spacecraft Rendezvous hi-ord8
Metrics: verification run-time (s) number of boundary hyperplanes N safe-region coverage ratio training success rate
Baselines: Baseline exact verification (prior ReLU NCBF exact verifier) dReal Z3
Builds on: Neural control barrier functions (exact ReLU NCBF verification) Nagumo's theorem dReal
Closest papers by meaning
- Exact Verification of ReLU Neural Control Barrier Functions (NeurIPS 2023 · similarity 0.92)
- Provably Safe Neural Network Controllers via Differential Dynamic Logic (NeurIPS 2024 · similarity 0.86)
- Verified Safe Reinforcement Learning for Neural Network Dynamic Models (NeurIPS 2024 · similarity 0.85)
- Two‑Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion (NeurIPS 2025 · similarity 0.83)
- Training Verification-Friendly Neural Networks via Neuron Behavior Consistency (AAAI 2025 · similarity 0.83)
- NN4SysBench: Characterizing Neural Network Verification for Computer Systems (NeurIPS 2024 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.