Formal Safety Verification and Refinement for Generative Motion Planners Via Certified Local Stabilization
Devesh Nath, Haoran Yin, Glen Chou
AI summary
Problem
Generative motion planners produce diverse, high-quality trajectories but are too large for neural network verification tools, making it impossible to formally guarantee their safety and dynamic feasibility for safety-critical robotics.
Approach
The method decouples trajectory generation from verification by sampling references from the large planner and stabilizing them with a small neural tracking controller, then applying reachability analysis to the closed-loop system to certify safety.
Key results
- NNV-based formal safety verification for large GMPs by decoupling generation from feedback loop verification
- Certified neural tracking controller that stabilizes dynamically-infeasible GMP references
- Trajectory-library method preserving original GMP behavior with proven sample complexity bounds
- Extensive simulation and hardware validation across diffusion, flow matching, and VLM planners
Why it matters
Enables deployment of expressive, data-driven motion planners in safety-critical robotics by providing hard, computationally tractable safety guarantees without costly retraining.
Abstract
We present a method for formal safety verifica- tion of learning-based generative motion planners. Generative motion planners (GMPs) offer advantages over traditional plan- ners, but verifying the safety and dynamic feasibility of their outputs is difficult since neural network verification (NNV) tools scale only to a few hundred neurons, while GMPs often contain millions. To preserve GMP expressiveness while enabling ver- ification, our key insight is to imitate the GMP by stabilizing references sampled from the GMP with a small neural tracking controller and then applying NNV to the closed-loop dynamics. This yields reachable sets that rigorously certify closed-loop safety, while the controller enforces dynamic feasibility. Building on this, we construct a library of verified GMP references and deploy them online in a way that imitates the original GMP distribution whenever it is safe to do so, improving safety with- out retraining. We evaluate across diverse planners, including diffusion, flow matching, and vision-language models, improving safety in simulation (on ground robots and quadcopters) and on hardware (differential-drive robot).