用小神经控制器验证生成式运动规划的安全性，不改原模型也能提升安全性。
Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization
- 用小控制器稳定生成样本，把复杂模型转为可验证的闭环系统。
- 在仿真和硬件上均显著提升机器人运动安全，无需重新训练。
- 适用于扩散、流匹配等多种生成模型，适合高风险场景部署。
我们提出一种针对学习型生成式运动规划器的形式化安全验证方法。生成式运动规划器（GMPs）虽具优势，但其输出的安全性和动态可行性难以验证，因神经网络验证工具仅支持数百个神经元，而GMPs通常包含数百万参数。我们的核心思路是：用小型神经跟踪控制器对从GMP中采样的参考轨迹进行稳定，并对闭环动力学应用神经网络验证。这能严格证实在闭环下的可达集安全性，同时控制器确保动态可行性。基于此，我们构建了经验证的GMP参考库，并在线部署时尽可能模仿原始GMP分布，只要安全即启用，从而在不重新训练的前提下提升整体安全性。我们在多种规划器（包括扩散模型、流匹配模型及视觉-语言模型）上进行评估，在地面机器人与四旋翼无人机的仿真中以及差速驱动机器人硬件平台上均取得显著安全性能提升。
原文摘要 · Abstract (English)
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).
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。