# Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization

arXiv: https://arxiv.org/abs/2509.19688 · HTML: https://mlsanity.com/paper/2509.19688/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 40 references that are in the map.
- First posted on arXiv 24 Sep 2025.

## Builds on (most cited first, 27 of 27)

- [Denoising Diffusion Probabilistic Models](https://mlsanity.com/paper/2006.11239/) (2020)
- [Flow Matching for Generative Modeling](https://mlsanity.com/paper/2210.02747/) (2022)
- [Neural Ordinary Differential Equations](https://mlsanity.com/paper/1806.07366/) (2018)
- [Is Conditional Generative Modeling all you need for Decision-Making?](https://mlsanity.com/paper/2211.15657/) (2022)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Motion Planning Diffusion: Learning and Planning of Robot Motions with Diffusion Models](https://mlsanity.com/paper/2308.01557/) (2023)
- [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021)
- [SafeDiffuser: Safe Planning with Diffusion Probabilistic Models](https://mlsanity.com/paper/2306.00148/) (2023)
- [Learning Robotic Manipulation Policies from Point Clouds with Conditional Flow Matching](https://mlsanity.com/paper/2409.07343/) (2024)
- [Adaptive Conformal Prediction for Motion Planning among Dynamic Agents](https://mlsanity.com/paper/2212.00278/) (2022)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [CoBL-Diffusion: Diffusion-Based Conditional Robot Planning in Dynamic Environments Using Control Barrier and Lyapunov Functions](https://mlsanity.com/paper/2406.05309/) (2024)
- [Funnel Libraries for Real-Time Robust Feedback Motion Planning](https://mlsanity.com/paper/1601.04037/) (2016)
- [Planning with Learned Dynamics: Probabilistic Guarantees on Safety and Reachability via Lipschitz Constants](https://mlsanity.com/paper/2010.08993/) (2020)
- [Multi-Agent Reachability Calibration with Conformal Prediction](https://mlsanity.com/paper/2304.00432/) (2023)
- [DiffuSolve: Diffusion-based Solver for Non-convex Trajectory Optimization](https://mlsanity.com/paper/2403.05571/) (2024)
- [Safe Output Feedback Motion Planning from Images via Learned Perception Modules and Contraction Theory](https://mlsanity.com/paper/2206.06553/) (2022)
- [Convex synthesis and verification of control-Lyapunov and barrier functions with input constraints](https://mlsanity.com/paper/2210.00629/) (2022)
- [DDAT: Diffusion Policies Enforcing Dynamically Admissible Robot Trajectories](https://mlsanity.com/paper/2502.15043/) (2025)
- [A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis](https://mlsanity.com/paper/2112.05745/) (2021)
- [Statistical Safety and Robustness Guarantees for Feedback Motion Planning of Unknown Underactuated Stochastic Systems](https://mlsanity.com/paper/2212.06874/) (2022)
- [One-Shot Reachability Analysis of Neural Network Dynamical Systems](https://mlsanity.com/paper/2209.11827/) (2022)
- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [Learning Complex Motion Plans using Neural ODEs with Safety and Stability Guarantees](https://mlsanity.com/paper/2308.00186/) (2023)
- [Using Neural Networks to Compute Approximate and Guaranteed Feasible Hamilton-Jacobi-Bellman PDE Solutions](https://mlsanity.com/paper/1611.03158/) (2016)
- [Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops](https://mlsanity.com/paper/2410.00145/) (2024)
- [Dynamics-aware Diffusion Models for Planning and Control](https://mlsanity.com/paper/2504.00236/) (2025)

## Built on by (most cited first, 2 of 2)

- [Safe Large-Scale Robust Nonlinear MPC in Milliseconds via Reachability-Constrained System Level Synthesis on the GPU](https://mlsanity.com/paper/2604.07644/) (2026)
- [Scalable Data-Driven Reachability Analysis and Control via Koopman Operators with Conformal Coverage Guarantees](https://mlsanity.com/paper/2601.01076/) (2026)

## Abstract (arXiv)

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).