生成運動プランナーのための認証済み局所安定化による正式な安全検証と改良
なぜ重要か: 企業や社会への影響が見込まれ、一般メディアにも波及する可能性があります。
arXiv:2509.19688v1発表種別：クロス
概要：本稿では、学習に基づく生成運動プランナーの形式的安全性検証手法を提案する。生成運動プランナー(GMP)は従来のプランナーに比べて利点を持つが、ニューラルネットワーク検証(NNV)ツールは数百ニューロン程度にしかスケールしないのに対し、GMPはしばしば数百万ニューロンを含むため、その出力の安全性と動的実現可能性を検証することは困難である。GMPの表現力を維持しつつ検証を可能にするため、本稿の主要な着眼点は、GMPからサンプリングされた参照軌道を小さなニューラル追従制御器で安定化し、その後閉ループダイナミクスにNNVを適用することである。これにより、閉ループの安全性を厳密に保証する到達可能集合が得られる一方、制御器は動的実現可能性を保証する。これを基に、検証済みのGMP参照軌道のライブラリを構築し、安全である限りオリジナルのGMP分布を模倣するようにオンラインで展開することで、再学習なしに安全性を向上させる。拡散モデル、フローマッチング、ビジョン言語モデルなど、様々なプランナーにおいてシミュレーション（地上ロボットおよびクアッドコプター）とハードウェア（差動駆動ロボット）上で評価を行い、安全性を向上させた。
原文（英語）を表示
Title (EN): Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization
arXiv:2509.19688v1 Announce Type: cross
Abstract: 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).
Published: 2025-09-24 19:00 UTC