Provably Safe Neural Network Controllers via Differential Dynamic Logic

arXiv:2402.10998 · eess.SY, cs.AI, cs.LG, cs.LO, cs.SY · Submitted 2024-02-16 · Read on arXiv

eess.SY, cs.AI, cs.LG, cs.LO, cs.SY

Submitted: 2024-02-16

Updated: 2024-10-24

Comments: 39 pages (main paper has 10 pages), 13 figures; Accepted at the Thirty-Eighth Annual Conference on Neural Information Processing Systems (NeurIPS 2024)

Journal ref: in Advances in Neural Information Processing Systems, 2024, pp. 1586-1624

DOI: 10.52202/079017-0051

Code: https://github.com/samysweb/NCubeV

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Verification — 109× in this paper · explained in 2 episodes
• Hybrid System — 24× in this paper · explained in 2 episodes
• Activation Function — 20× in this paper · explained in 1 episode
• Benchmark — 18× in this paper · explained in 2 episodes
• SMT solver — 17× in this paper · explained in 2 episodes
• Verifier — 11× in this paper · explained in 2 episodes
• Formal Methods — 6× in this paper · explained in 3 episodes
• Robustness — 5× in this paper · explained in 5 episodes
• Steering — 5× in this paper · explained in 2 episodes
• Abstraction — 4× in this paper · explained in 1 episode
• Core — 4× in this paper · explained in 2 episodes
• Generalization — 4× in this paper · explained in 13 episodes
• Lyapunov function — 4× in this paper · explained in 2 episodes
• Reinforcement Learning — 4× in this paper · explained in 4 episodes
• Formal Verification — 2× in this paper · explained in 2 episodes
• Institutional Review Board — 2× in this paper
• International Joint Conference on Artificial Intelligence — 2× in this paper
• Adversarial Examples — 1× in this paper · explained in 2 episodes
• Adversarial Search — 1× in this paper · explained in 1 episode
• Algorithmic Improvements — 1× in this paper · explained in 1 episode
• Analyzer — 1× in this paper · explained in 1 episode
• Cooperation — 1× in this paper · explained in 2 episodes
• Digital Avionics Systems Conference — 1× in this paper
• Energy Efficiency — 1× in this paper · explained in 3 episodes
• Grounding — 1× in this paper · explained in 3 episodes
• Near Mid-Air Collision — 1× in this paper
• Quantization — 1× in this paper · explained in 12 episodes
• Trace — 1× in this paper · explained in 2 episodes

Sources

• The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results
• Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers
• Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes

Related papers

• One Request, Multiple Experts: LLM Orchestrates Domain Specific Models via Adaptive Task Routing
• A Geometric Decision Procedure for STL Feasibility and Repair
• Submodular Multi-Agent Policy Learning for Online Distributed Task Allocation in Open Multi-Agent Systems
• Policy-Level Recursive Self-Improvement for Embodied AI with a Criticality World Model
• Minimal Experiments for Robust Stabilization: Information, Spectral Geometry, and Duration
• Decentralized Power-Optimal Coordination for Spacecraft Swarms Using Time-Varying Magnetorquer Actuation