技術要約：VASO – 物理的AIエージェントのための形式検証可能な自己進化型スキル

問題提起

再利用可能なロボットスキルは、基盤モデルと物理的制御の間のインターフェースとして機能し、身体化されたエージェントが長期的なタスクを安全制約の下で実行することを可能にする。基盤モデルは自然言語からのスキル生成コストを削減したが、「スキルの保証（skill assurance）」という問題は解決していない。既存の自己進化手法は、実行結果、ユニットテスト、環境報酬、あるいはLLMによる自己批判といった「ソフト」なフィードバック信号に依存している。これらの信号は、サンプリングされた実行においてはスキルが機能したことを示す「トレースレベルのエビデンス」を提供するに過ぎず、テストされていない条件下でスキルに起因するプランが時間的安全性契約を満たすことを保証するものではない。ロボティクスにおいて、単一の稀だが深刻な安全性違反（例：人が検知された後に地上走行ロボットが移動する）は許容されないが、ソフトなフィードバックではこうしたエッジケースを検出できないことが多い。

核心となる課題は、単に不安全なプランをフィルタリングしたりモデルの重みを微調整したりすることなく、形式検証とスキルの進化の間のループを閉じることである。形式的な反例（counterexample）が、再利用可能なスキルの契約を直接更新できるような表現が必要であり、それによって改善内容が検査可能、再利用可能、かつ検証可能であることを保証する必要がある。

手法：VASOフレームワーク

著者らは、LLMが生成したロボットスキルの契約の自己進化のための閉ループ・フレームワークであるVASO (Verification-Guided Automated Skill Optimization) を提案する。VASOは、スキルを、形式的なインターフェースとプランナー向けインターフェースを結合させたセマンティックな契約として扱うことで動作する。

1. 検証可能なスキル表現

スキル $sk$は、タプル$(G, \psi_{sk}, C_{sk})$ として定義される：

• $G$ (グローバル仕様): 常に成立しなければならない安全制約を表すLTL（線形時相論理）の集合。
• $\psi_{sk}$ (ローカルルール): スキルの特定の意図またはゴールを定義するLTL式。
• $C_{sk}$ (セマンティック契約): 以下の要素からなるコアコンポーネント：
  • $L_{sk}$ (命題整合型ラベル付け関数): 低レベルのロボット状態、観測、および制御コマンドを原子的な論理命題にマッピングする関数。これは、物理的実行と記号的モデル検査の間のギャップを埋める。
  • $C^p_{sk}$ (テキストベースのプランテンプレート): 実行可能なコマンド（APIコールや軌道など）を生成するようにプランナーを導く行動バイアス。

2. 2レベルの検証ループ

VASOは、スキルを洗練させるために階層的な検証プロセスを採用する：

• スキルレベルの検証（実現可能性チェック）: プランをサンプリングする前に、フレームワークはローカルルール $\psi_{sk}$ がグローバル仕様 $G$ と論理的に一貫しているかを確認する。普遍的な遷移系が構築され、充足可能性が検証される。もしローカルルールがグローバルな安全性に矛盾する場合（例：人が観察されているときに移動を命じるルール）、そのスキルは拒絶され、基盤モデルに対してローカルルールの洗練が要求される。
• プランレベルの検証（行動チェック）: 実現可能なスキルが得られた後、プランナーは実行可能なプラン $\pi$ を生成する。このプランは、ラベル付け関数 $L_{sk}$ を用いて記号的遷移系（オートマトン）へとコンパイルされる。モデルチェッカー（NuSMV）が、$G \land \psi_{sk}$ に対してプランを検証する。

3. テキストによる勾配を用いた最適化

検証が失敗した場合、モデルチェッカーは反例トレース（counterexample trace）を返す。VASOはこのトレースをテキストによる勾配（例：「仕様違反：$G(\text{person\_observed} \to X \text{ stop})$」）に変換する。このテキストによるフィードバックは、セマンティック契約 $C_{sk}$ およびローカルルール $\psi_{sk}$ を更新するために基盤モデルへとフィードバックされる。

• 主要な制約: 基盤モデルの重みは凍結されたままである。最適化はすべてプロンプトおよび契約レベルで行われ、モデルのパラメータや単一のタスクプロンプトをチューニングするのではなく、再利用可能なスキルアーティファクト自体を洗練させる。
• プロセス: ループは、順方向の生成（契約 $\to$ プラン $\to$ オートマトン）と逆方向の洗練（オートマトン $\to$ テキストによる勾配 $\to$ 更新された契約）を交互に繰り返す。

主な貢献

1. 検証可能な自己進化型スキル表現: 本論文は、時間的論理仕様、命題整合型のロボットセマンティクス、およびプランナー向けテンプレートを明示的に接続するスキル構造を導入している。これにより、LLMが生成したスキルを、形式検証にさらされつつもプランニングに使用することが可能になる。
2. 最適化フィードバックとしての形式的反例: 著者らは、反例トレースをテキストによる勾配に変換する2レベルの検証ループを開発した。これにより、特定のプランを単に拒絶したりプロンプトをチューニングしたりするのではなく、再利用可能なスキル契約そのものを洗練させることが可能になる。
3. 物理エージェントによる検証: 本フレームワークは、実機のロボットプラットフォーム（Clearpath JackalおよびPX4クアッドコプター）を用いて検証されており、最適化されたスキルが、基盤モデルのファインチューニングなしに高い形式仕様適合性を達成できることを示している。

実験結果

フレームワークは、2つのロボットプラットフォームにおける400の生成プランに対し、11の時相論理仕様を用いて評価された。

• 適合性: VASOは、100サンプル未満の最適化サンプル（スキルあたり20分未満）を使用して、97.2%の形式仕様適合率を達成した。
• 比較: ゼロショットのベースライン、プロンプト最適化手法（LAD-VFなど）、およびファインチューニングに基づく手法（RLVFなど）を上回った。特筆すべきは、VASOがファインチューニング手法よりも高い安全性スコアに到達しながら、訓練コストと時間をわずか数分の一に抑えた点である。
• 汎化性能: 最適化されたスキルは、同一のタスクファミリー内の未知のタスクプロンプトに対して強い汎化性能を示し、追加の洗練なしに高い安全性とタスク完了率を維持した。
• 自動アライメント: 自動生成された命題整合型ラベル付け関数が、手作業によるマッピングと同等の性能を発揮したことが示され、記号的抽象化を定義するためのドメイン専門知識の必要性を排除した。

重要性と主張

本論文は、物理的AIエージェントのための、形式検証と自己進化型LLM生成スキルの間のループを閉じた最初のフレームワークであると主張している。

• パラダイムの転換: 標準的な検証済みプランニング・パイプラインは、検証を一度限りのプランに対するパス/フェイルのフィルターとしてのみ使用するが、VASOは拒絶の理由（反例）を用いて、プランのソース（再利用可能なスキル）を改善する。
• 効率性と安全性: モデルの重みを最適化するのではなく、スキルの契約を最適化することで、VASOは、生成された行動が検査可能かつ様々なタスクに再利用可能であることを保証し、より安全で信頼性の高い挙動を生成するメカニズムを提供する。これは、物理的AIにおけるスキルの保証という重要なボトルネックに対処するものである。
• 限界: 著者らは、形式的な保証は、AIによって生成された命題整合型ラベル付け関数の正確性に条件付けられることを認めている。低レベルのダイナミクスから記号的な命題へのマッピングにエラーがあると、偽の検証結果を招く可能性があるが、実験データによれば、これは安全性スコアの低下（1%未満）として極めて稀にしか発生しない。現在のフレームワークはまた、逐次的かつ非並行的な実行を想定している。