Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization
This addresses safety verification for learning-based motion planners in robotics, which is critical for real-world deployment but challenging due to scalability issues.
The paper tackles the problem of verifying safety and dynamic feasibility for generative motion planners (GMPs) by proposing a method that stabilizes GMP outputs with a small neural tracking controller and applies neural network verification to certify closed-loop safety, improving safety in simulation and on hardware without retraining.
We present a method for formal safety verification of learning-based generative motion planners. Generative motion planners (GMPs) offer advantages over traditional planners, 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 verification, 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 without 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).