ロボットが複雑な指示を長時間にわたって実行するためには、再利用可能なスキル（技能）が重要な役割を果たします。基盤モデルの登場により、こうしたスキルを生成するコストは大幅に低下しましたが、生成されたスキルが本当に信頼できるかどうかを検証するコストはまだ高いままです。従来のスキル進化ループは、実行フィードバック、ユニットテスト、環境報酬、またはLLMの自己批評を通じてスキルを改善していますが、これらの信号は限られたサンプル実行でうまくいったことを示すだけで、未テスト条件下で安全性の契約を満たすかどうかは保証しません。 そこで研究チームは、形式検証に基づいてLLM生成ロボットスキルを自己進化させるフレームワーク「VASO」を開発しました。VASOでは、各スキルはセマンティック契約として表現され、2つの結合インターフェースを持ちます。形式インターフェースはロボットの状態、観測、制御コマンドを論理命題と整列させてモデルチェッキングを可能にし、プランナー向けインターフェースは実行可能な動作生成を導きます。 フレームワークはまずモデルチェッカーで論理的に矛盾したスキル契約をフィルタリングし、スキルが生成するプランを時間的仕様に対して検証します。検証が失敗した場合、VASOは反例トレースをテキスト勾配に変換し、基盤モデルの重みは凍結したまま再利用可能なスキル契約を更新します。 ClearpathJackalとPX4クワッドコプターのタスクでは、VASOは100未満の最適化サンプルで97.2%の形式仕様準拠を達成し、実行フィードバック、プロンプト最適化、ファインチューニングのベースラインを上回りました。形式検証と自己進化LLMスキルの間のループを閉じた初のフレームワークとして、VASOは反例を単なるプラン検証ではなく、再利用可能なロボットスキル契約の最適化フィードバックに変える革新的なアプローチを実現しています。