Research map / Learning theory and algorithms / Combinatorial and search optimization
Provably Safe Neural Network Controllers via Differential Dynamic Logic
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.
Introduces VerSAILLE, which reuses differential dynamic logic control envelopes to prove infinite-time safety of neural network controllers via nondeterministic mirrors and open-loop NN verification, plus Mosaic, a sound and complete lifting of linear NN verifiers to polynomial real arithmetic with arbitrary logical structure, implemented in SNNT.
Problem
Verifying safety of neural network controlled cyber-physical systems over unbounded time horizons, where existing closed-loop NN verifiers only give bounded-time guarantees and open-loop NN verifiers only handle linear normalized queries.
Approach
Replace a dL control envelope by a nondeterministic mirror of the NN, derive a ModelPlex controller monitor formula, and verify it as an open-loop NN query; Mosaic lifts complete linear-constraint NN verifiers to nonlinear, non-normalized queries by linearization, input-space partitioning (azulejos), and SMT filtering of affine counterexample regions.
Key results
- On VCAS level-flight scenarios, DNC and DND advisories are verified safe (0.35 h and 0.28 h), while DES1500, CL1500, SDES1500, SCL1500, SDES2500 and SCL2500 are shown unsafe with exhaustive counterexample enumeration (e.g. 49,428 CE regions for DES1500 in 5.45 h).
- On the adaptive cruise control running example, verification or exhaustive counterexample enumeration completes in 47 to 300 seconds depending on NN size and linearization.
- The largest NN verified had 270 ReLU neurons, and the authors claim SNNT is at the frontier of scalability for global properties.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use Mosaic query normalization instead of naive expansion | ACAS VCAS verification query generation · ACAS level-flight verification | number of propositionally feasible queries: up to 39 trillion -> 19k | Helped |
| Add SMT filtering of counterexample regions to approximation-based verification (ablation) | Mosaic on the DNC network · VCAS level flight, DNC | safety verification | Helped |
| Use approximation alone without completeness-preserving counterexample filtering (ablation) | Mosaic on the DNC network · VCAS level flight, DNC | safety verification | Hurt |
| Apply VerSAILLE and Mosaic to the level-flight VCAS networks | ACAS VCAS networks · VCAS level flight, DNC and DND | safety status | Helped |
| Apply VerSAILLE and Mosaic to the level-flight VCAS networks | ACAS VCAS networks · VCAS level flight, DES1500, CL1500, SDES1500, SCL1500, SDES2500, and SCL2500 | safety status | Hurt |
Surprising findings
- Safety for the DNC advisory was only verifiable through SMT filtering, since approximation alone produced spurious counterexamples.
- Naive rewriting (DNNV-style expansion) may produce up to 39 trillion propositionally feasible queries for the ACAS case, versus 19k with Mosaic's normalization.
Limitations
- Implementation SNNT only supports ReLU networks; piece-wise Noetherian theory is not implemented.
- Infinite-time guarantees depend on an existing verified dL control envelope and invariant, which must be provided or proven.
- Scalability is limited relative to local robustness verifiers; largest verified NN has 270 ReLUs.
Experimental setup
Datasets: VCAS airborne collision avoidance NN benchmark
Benchmarks: VCAS (ACAS X) airborne collision avoidance adaptive cruise control running example Zeppelin steering case study
Metrics: verification status (safe/unsafe) wall-clock runtime number of counterexample regions time to first counterexample
Baselines: DNNV nnenum Marabou closed-loop NNV tools
Builds on: differential dynamic logic ModelPlex nnenum OVERT DNNV
Closest papers by meaning
- Reachability Analysis of Neural Network Control Systems (AAAI 2023 · similarity 0.88)
- Verified Safe Reinforcement Learning for Neural Network Dynamic Models (NeurIPS 2024 · similarity 0.88)
- SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions (NeurIPS 2024 · similarity 0.86)
- Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation (ICML 2024 · similarity 0.86)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.85)
- NN4SysBench: Characterizing Neural Network Verification for Computer Systems (NeurIPS 2024 · similarity 0.85)
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.