VASO: 物理AIエージェントのための形式検証可能な自己進化スキル
VASOは、形式検証を用いてLLM生成ロボットスキル契約の自己進化を導くフレームワークです。Clearpath JackalおよびPX4クアッドコプタータスクにおいて、100サンプル未満の最適化で97.2%の形式仕様準拠を達成し、実行フィードバック、プロンプト最適化、ファインチューニングベースラインを上回ります。形式検証と自己進化スキルを閉ループ化した最初のフレームワークです。
基盤モデル（大規模言語モデルなど）の急速な発展により、ロボットスキルの作成コストは大幅に低下しましたが、信頼コストは依然として高いままです。従来のスキル進化ループは実行フィードバック、単体テスト、環境報酬、LLMの自己批判に依存していますが、これらのシグナルは軌跡レベルの証拠しか提供せず、未テスト条件下でスキルが誘導する計画が時相安全契約を満たすことを保証しません。この問題に対処するため、研究チームはVASO（Verifiably Autonomous Self-Operating）フレームワークを提案しました。これは形式検証を用いてLLMが生成するロボットスキル契約の自己進化を導くものです。
VASOの核心は、各再利用可能なロボットスキルを意味契約として表現することです。この契約は二つのインターフェースを持ちます。形式的インターフェースはロボットの状態、観測、制御コマンドを論理命題と整合させ、モデル検査を可能にします。プランナー向けインターフェースは実行可能な行動生成を導きます。動作中、モデルチェッカーはまず論理的に矛盾するスキル契約をフィルタリングし、次にスキルが誘導する計画をグローバルおよびローカルの時相仕様に対して検証します。検証が失敗すると、VASOは反例トレースをテキスト勾配に変換し、基盤モデルの重みを固定したまま再利用可能なスキル契約を更新します。
実験では、Clearpath Jackal地上ロボットとPX4クアッドコプターを用いてVASOを評価しました。その結果、VASOは100サンプル未満の最適化で97.2%の形式仕様準拠を達成し、実行フィードバック、プロンプト最適化、ファインチューニングのベースラインを上回りました。私たちの知る限り、VASOは形式検証とLLM生成スキルの自己進化を閉ループ化した初めてのフレームワークです。形式反例は単発計画の検証に留まらず、再利用可能なスキル契約の最適化フィードバックとして機能し、プランナープロンプトの調整やモデル重みのファインチューニングに頼る従来のアプローチを超えています。
この研究はロボットスキルの信頼できる進化に新たなパラダイムを提供し、安全性が重要な物理AIアプリケーションでの活用が期待されます。形式検証をスキル進化ループに組み込むことで、VASOは複雑な環境でもロボットの動作が常に期待通りであることを強力に保証します。