通过认证局部稳定实现生成式运动规划器的形式化安全验证与精化
机器人学
2025-09-25 v1 机器学习
系统与控制
系统与控制
最优化与控制
摘要
我们提出了一种用于基于学习的生成式运动规划器的形式化安全验证方法。生成式运动规划器 (GMPs) 相比传统规划器具有优势，但验证其输出的安全性和动力学可行性是困难的，因为神经网络验证 (NNV) 工具仅能扩展到数百个神经元，而 GMPs 通常包含数百万个。为了在保持 GMP 表达力的同时实现验证，我们的关键思路是通过一个小的神经跟踪控制器稳定从 GMP 采样的参考轨迹，然后对闭环动力学应用 NNV。这产生了严格证明闭环安全的可达集，同时控制器保证了动力学可行性。在此基础上，我们构建了一个已验证的 GMP 参考轨迹库，并在安全的情况下以模仿原始 GMP 分布的方式在线部署它们，从而在不重新训练的情况下提高安全性。我们在包括扩散、流匹配和视觉语言模型在内的多种规划器上进行了评估，在仿真（地面机器人和四旋翼飞行器）和硬件（差速驱动机器人）上均提高了安全性。
引用
@article{arxiv.2509.19688,
title = {Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization},
author = {Devesh Nath and Haoran Yin and Glen Chou},
journal= {arXiv preprint arXiv:2509.19688},
year = {2025}
}
备注
10 pages, 12 figures