論文の概要: VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents

• arxiv url: http://arxiv.org/abs/2606.05395v1
• Date: Wed, 03 Jun 2026 20:02:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-05 22:39:44.374132
• Title: VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents
• Title（参考訳）: VASO: 物理的AIエージェントのための形式的に検証可能な自己進化スキル
• Authors: Yunhao Yang, Neel P. Bhatt, Kevin Wang, Samuel Tetteh, Zhangyang Wang, Ufuk Topcu,
• Abstract要約: 本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。 VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。 Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
• 参考スコア（独自算出の注目度）: 57.240036084348354
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Reusable robot skills are becoming the basic units through which embodied agents turn open-ended instructions into long-horizon physical behavior. We argue that, while foundation models have collapsed the cost of creating these skills, the cost of trusting them has not. Existing skill-evolution loops refine skills through execution feedback, unit tests, environment reward, or LLM self-critique, but these signals provide only trace-level evidence: they show that a skill worked on sampled executions, not that skill-induced plans satisfy temporal safety contracts under untested conditions. We introduce VASO, a framework for verification-guided self-evolution of LLM-generated robot skill contracts. In VASO, each skill is represented as a semantic contract with two coupled interfaces: a formal interface that aligns robot states, observations, and control commands with logical propositions for model checking, and a planner-facing interface that guides executable behavior generation. A model checker first filters logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications. When verification fails, VASO translates the counterexample trace into a textual gradient that updates the reusable skill contract while keeping foundation-model weights frozen. On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples, outperforming execution-feedback, prompt-optimization, and fine-tuning baselines. To our knowledge, VASO is the first framework that closes the loop between formal verification and self-evolving LLM-generated skills for physical AI agents: formal counterexamples become optimization feedback for reusable robot skill contracts, rather than merely verifying one-off plans, tuning planner prompts, or fine-tuning model weights.
• Abstract（参考訳）: 再使用可能なロボットのスキルは、エンボディエージェントがオープンエンドの指示をロングホライズンな身体行動に変換する基本的なユニットになりつつある。 ファンデーションモデルはこれらのスキルを作るコストを崩壊させたが、信頼するコストは高くない、と私たちは主張する。 既存のスキル進化ループは、実行フィードバック、ユニットテスト、環境報酬、LLM自己批判を通じてスキルを洗練させるが、これらのシグナルはトレースレベルの証拠のみを提供する。 LLM生成ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。 VASOでは、各スキルは、ロボットの状態、観察、制御コマンドを、モデルチェックのための論理的命題と整列する形式的なインターフェースと、実行可能な振る舞い生成を導くプランナー対面インターフェースの2つの結合インターフェースによるセマンティックコントラクトとして表現される。 モデルチェッカーは、まず論理的に一貫性のないスキルコントラクトをフィルタリングし、その後、グローバルおよびローカルの時間仕様に対してスキルによって誘発される計画を検証する。 検証が失敗した場合、VASOは反例トレースをテキストの勾配に変換し、基本モデルの重みを凍結させながら再利用可能なスキル契約を更新します。 Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100未満の最適化サンプルを使用して97.2%の形式的な仕様準拠に達し、実行フィードバック、プロンプト最適化、微調整ベースラインを達成している。 我々の知る限り、VASOは、正式な検証と物理的AIエージェントの自己進化的LLM生成スキルの間のループを閉じる最初のフレームワークである。

関連論文リスト

• Contractual Skills: A GovernSpec Design Framework for Enterprise AI Agents [8.419155861590548]
  本稿では,SKILL.mdファイルを可読性のあるタスクコントラクトとして整理するための,GovernSpecにインスパイアされた設計フレームワークであるコントラクトスキルを提案する。 このフレームワークは、コントラクトスキル、GovernSpec YAMLコントラクト、モデルコンテキストプロトコル(MCP)サーフェス、ツールアダプタ、ランタイムガードレール、トレース、評価システムの境界を明確にしている。
  論文  参考訳（メタデータ） (2026-05-21T15:40:05Z)
• Harnessing LLM Agents with Skill Programs [58.356514745548026]
  HASPは、実行可能なプログラム関数(PF)にスキルをアップグレードする新しいフレームワークです。 PFは障害が発生しやすい状態を起動し、次のアクションを変更したり、修正コンテキストを注入する実行可能なガードレールとして機能する。 HASPは、Web検索、数学推論、コーディングタスクにおいて、トレーニング不要とトレーニングベースの両方の手法と比較して、大幅に向上している。
  論文  参考訳（メタデータ） (2026-05-18T01:35:11Z)
• Skill-R1: Agent Skill Evolution via Reinforcement Learning [84.35984979949502]
  Skill-R1は、検証可能な報酬からインスタンスレベルの繰り返しスキル最適化のための強化学習フレームワークである。 オープンソースモデルとクローズドソースモデルの両方とのブラックボックス互換性を維持しつつ、モデルレベルの更新よりも大幅に安価に適応できる。
  論文  参考訳（メタデータ） (2026-05-10T06:19:15Z)
• SEVerA: Verified Synthesis of Self-Evolving Agents [12.9624447364193]
  自己進化型エージェントフレームワークは、安全性や正確性の正式な保証を提供しない。 エージェントコード生成を制約付き学習問題として定式化し、ハードな形式仕様とソフトな目的とを組み合わせてタスクユーティリティをキャプチャする。 探索はFGGMコールを含む候補パラメトリックプログラムを合成し、検証は全てのパラメータ値に対する厳しい制約に関して正当性を証明し、制約のない学習に還元する。
  論文  参考訳（メタデータ） (2026-03-26T07:32:20Z)
• Execution-State-Aware LLM Reasoning for Automated Proof-of-Vulnerability Generation [36.950993500170014]
  本稿では,PoV生成を反復的仮説検証法として再構成するエージェントフレームワークであるDrillAgentを提案する。 我々は、実世界のC/C++脆弱性の大規模なベンチマークであるSEC-bench上でDrillAgentを評価する。
  論文  参考訳（メタデータ） (2026-02-14T03:17:27Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。 エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
  論文  参考訳（メタデータ） (2026-01-27T16:10:23Z)
• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。 これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
  論文  参考訳（メタデータ） (2025-09-28T06:32:14Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。