再利用可能なロボットスキルは、身体性エージェントがオープンエンドな指示を長期的な物理行動へ変換するための基本単位になりつつある。基盤モデルによってこうしたスキルの作成コストは大幅に下がったが、著者らは、それらを信頼するコストは下がっていないと指摘する。既存のスキル進化ループは、実行フィードバック、単体テスト、環境報酬、LLMの自己批評などを通じてスキルを洗練させるが、これらの信号はトレースレベルの証拠しか提供しない。つまり、サンプリングされた実行でスキルが機能したことを示すだけで、未テストの条件下でスキルが誘導する計画が時間的安全コントラクトを満たすことを保証するものではない。
そこで研究チームは、LLM生成のロボットスキルコントラクトを検証誘導で自己進化させるフレームワーク「VASO」を提案する。VASOの中心的な考え方は、形式的検証とスキル進化のループを閉じることにある。形式的反例は、一度きりの計画検証に使うだけでなく、再利用可能なスキルコントラクトを最適化するためのフィードバック信号として利用される。
VASOでは、各スキルは二つの結合したインターフェースを持つ意味的コントラクトとして表現される。第一は形式インターフェースで、ロボットの状態、観測、制御コマンドをモデル検査用の論理命題に整列させる。第二はプランナ向けインターフェースで、実行可能な行動生成を導く。この二重インターフェース設計により、スキルは形式的ツールで分析できると同時に、プランナが実際に利用できるものになる。
VASOの処理は二段階で進む。まずモデルチェッカーが論理的に矛盾するスキルコントラクトを除外し、無効なコントラクトが後続処理に進むのを防ぐ。次に、モデルチェッカーがスキルによって誘導される計画を、グローバルおよびローカルの時間仕様に対して検証する。検証が失敗した場合、VASOは反例トレースをテキスト勾配に変換し、その勾配を用いて再利用可能なスキルコントラクトを更新する。この間、基盤モデルの重みは凍結されたままである。つまり、スキル進化はモデルパラメータではなくコントラクトのレベルで行われる。
Clearpath JackalとPX4クアッドコプターのタスクでの実験では、VASOは100未満の最適化サンプルで97.2%の形式仕様準拠率を達成し、実行フィードバック、プロンプト最適化、ファインチューニングのベースラインを上回った。著者らの知る限り、VASOは物理AIエージェントにおいて、形式的検証とLLM生成スキルの自己進化のループを閉じた最初のフレームワークである。形式的反例は、一度きりの計画検証、プランナプロンプトの調整、モデル重みのファインチューニングにとどまらず、再利用可能なロボットスキルコントラクトの最適化フィードバックとなる。
本論文はYunhao Yangら6名の著者によるもので、2026年6月3日に提出され、ロボティクス（cs.RO）と人工知能（cs.AI）の交叉領域に属する。論文番号はarXiv:2606.05395であり、プロジェクトページも公開されている。