論文の概要: VeriSkill: A Self-Evolution Framework for Program Verification Skills
- arxiv url: http://arxiv.org/abs/2607.27733v1
- Date: Thu, 30 Jul 2026 06:15:29 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-31 21:37:00.421209
- Title: VeriSkill: A Self-Evolution Framework for Program Verification Skills
- Title（参考訳）: VeriSkill: プログラム検証スキルのための自己進化フレームワーク
- Abstract要約: プログラム検証のための自己進化フレームワークであるVeriSkillを提案する。
検証失敗をスキル不足とみなし、診断シグネチャを再利用可能なレッスンに蒸留し、候補スキルを反復的に洗練する。
- 参考スコア（独自算出の注目度）: 19.114016708981023
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Automating program verification with LLM agents requires generating specifications, annotations, auxiliary lemmas, and tool invocations, all of which depend on reusable skills. A natural remedy is skill self-evolution: distilling skills from trajectories and refining them through feedback. However, existing evolution methods struggle with program verification tasks because they cannot reliably identify skill-specific failures or extract actionable signals from opaque verifier feedback. In this paper, we propose VeriSkill, a self-evolution framework built for program verification. It attributes verification failures to skill deficiencies, distills diagnostic signatures into reusable lessons, and iteratively refines candidate skills, admitting only revisions that improve verification performance while preserving program semantics. Experiments show that VeriSkill consistently outperforms all baselines across multiple verification tools, agent frameworks, and LLM backends.
- Abstract（参考訳）: LLMエージェントによるプログラム検証の自動化には、仕様生成、アノテーション、補助レムマ、ツール呼び出しが必要である。
自然な治療法はスキルの自己進化であり、軌跡からスキルを蒸留し、フィードバックを通じてそれらを精製する。
しかし、既存の進化的手法は、スキル固有の失敗を確実に識別したり、不透明な検証者フィードバックから実行可能な信号を抽出できないため、プログラム検証タスクに苦慮している。
本稿では,プログラム検証のための自己進化フレームワークであるVeriSkillを提案する。
検証の失敗をスキル不足とみなし、診断シグネチャを再利用可能なレッスンに蒸留し、プログラムのセマンティクスを維持しながら検証パフォーマンスを改善するリビジョンのみを認めながら、候補スキルを反復的に洗練する。
実験によると、VeriSkillは複数の検証ツール、エージェントフレームワーク、LLMバックエンドで、すべてのベースラインを一貫して上回っている。
関連論文リスト
- Evo-Harness: Context-to-Harness Skill Compilation for Self-Evolving Agents [67.97365535829098]
経験から学ぶことは、有能で自己改善型の大規模言語モデル(LLM)エージェントの開発に不可欠である。
Evo-Harnessは、ノイズの多いシングルショット実行を、クロスドメインとトピックレベルの適応のための再利用可能なスキルハーネスに蒸留する。
本分析は,エボ・ハーネスの有効性を実証し,LLMエージェントがリアルタイムで効果的に学習する方法の原理的理解を提供する。
論文 参考訳（メタデータ） (2026-08-15T06:43:56Z) - Skill Self-Play: Pushing the Frontier of LLM Capability with Co-Evolving Skills [53.15216425100295]
本稿では,提案者,解決者,スキルコントローラからなる共進化型フレームワークであるスキルセルフプレイ(スキルSP)を紹介する。
プロジェクタは動的にサンプリングされたスキルを前提とした挑戦的なタスクを生成し、ソルバは能力境界を押し上げるための候補ソリューションを探索し、スキルコントローラは実行フィードバックを収集してスキルライブラリを更新および拡張する。
このインタラクティブな共進化は、構造化された検証とオープンな調査の間のギャップを効果的に埋める。
論文 参考訳（メタデータ） (2026-07-24T17:59:22Z) - AEVAL: From Anecdotal to Deterministic Testing for Agentic Skill Workflows [1.6785141970297952]
AEVAL(Agentic Evaluation)はCI統合フレームワークで、このプラクティスをエージェントスキルのための決定論的かつ再現可能なテストパイプラインに置き換える。
すべてのスキル変更がテストイベントをトリガーする。スキルは、自動エグゼキュータ内の開発者が宣言した評価契約に対して実行される。
鍵となる要素は、実行子とグレーダの間の構造的分離であり、微妙だが広汎な障害モードを防止する。
論文 参考訳（メタデータ） (2026-07-16T21:33:05Z) - TTHE: Test-Time Harness Evolution [50.26245555541721]
既存のアプローチでは、デプロイ前、トレーニング前、あるいはテスト時に凍結される固定されたエージェントワークフローの開発データを最適化する。
我々は、エージェントがテスト入力で生成するラベルのない実行トレースのみを使用して、評価自体にハーネスを最適化できるかどうかを問う。
評価中、TTHEは候補ハーネスの人口を維持し、それらの実行トレースの理由をエージェントプロジェクタを通じてそれらを洗練する。
その後、審査員は実行元プロキシ信号から改善されたハーネスをコミットし、選択したプログラムは継続してその後の入力を統治する。
論文 参考訳（メタデータ） (2026-07-09T05:53:39Z) - SkillCoach: Self-Evolving Rubrics for Evaluating and Enhancing Agentic Skill-Use [21.05387636058484]
SkillCoachは、エージェントのスキル使用を評価し、強化するための自己進化フレームワークである。
実際のロールアウトから熟練したプロセスルーブリックを導き、四次元に沿って軌道を評価する。
外部検証器を別個の結果信号として保持し、プロセス品質を偶然のタスク成功と区別できるようにする。
論文 参考訳（メタデータ） (2026-07-02T08:28:51Z) - SkillAudit: Ground-Truth-Free Skill Evolution via Paired Trajectory Auditing [81.51044612408793]
SkillAuditは、地味なフィードバックなしにエージェントスキルを進化させるフレームワークである。
行動の違いを編集指導に変換するために、SkillAuditはProcess-Aligned Contrastive Evaluationを使用する。
Refineはノイズや無関係なガイダンスを広く有用なスキルから取り除き、修復はタスクと競合するパスを置き換える。
論文 参考訳（メタデータ） (2026-06-12T08:20:09Z) - Socratic-SWE: Self-Evolving Coding Agents via Trace-Derived Agent Skills [12.442806027914097]
本稿では,エージェントの過去の解法トレースをトレーニング信号のソースとして再利用する,クローズドループ自己進化フレームワークであるSocratic-SWEを紹介する。
トレースを報酬計算の証拠としてのみ扱うのではなく、Socratic-SWEはそれらを、繰り返し発生する障害と効果的な修復パターンを要約した構造化されたエージェントスキルに蒸留する。
論文 参考訳（メタデータ） (2026-06-05T16:00:17Z) - VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。
VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。
Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
論文 参考訳（メタデータ） (2026-06-03T20:02:35Z) - SkillGrad: Optimizing Agent Skills Like Gradient Descent [30.781132643932338]
エージェントスキルは、構造化ファイルに再利用可能な手続き的知識を格納することで、特殊なドメインにLLMエージェントを適用するための軽量な方法を提供する。
既存のスキル進化法はしばしば、明示的な定式化なしに反射を通してこれらの欠陥に対処する。
エージェントスキルを最適化するための勾配に着想を得たフレームワークであるSkillGradを提案する。
論文 参考訳（メタデータ） (2026-05-26T23:18:43Z) - Trace2Skill: Verifier-Guided Skill Evolution for Long-Context EDA Agents [0.3733676450456031]
テスト時間スケーリングフレームワークであるTrace2Skillを提案する。
新しいモデルをトレーニングしたり、より多くの候補ソリューションをサンプリングする代わりに、Trace2Skillはエージェントの自然言語スキルを進化可能なポリシーとして扱う。
成功と失敗モードのために繰り返しロールアウトトレースをマイニングし、それらを密集した診断やオラクルのレッスンに変換し、オラクル、ミューテータ、セレクタループを使用してタスク固有のスキルを生成する。
論文 参考訳（メタデータ） (2026-05-20T23:10:49Z) - ReVISE: Learning to Refine at Test-Time via Intrinsic Self-Verification [53.80183105328448]
Refine via Intrinsic Self-Verification (ReVISE)は、LLMが自己検証を通じてアウトプットを自己修正できる効率的なフレームワークである。
様々な推論タスクに関する実験により、ReVISEは効率的な自己補正を実現し、推論性能を大幅に向上することを示した。
論文 参考訳（メタデータ） (2025-02-20T13:50:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。