論文の概要: Automating Formal Verification with Agent-Guided Tree Search

• arxiv url: http://arxiv.org/abs/2605.27485v1
• Date: Tue, 26 May 2026 14:50:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-28 17:38:55.368628
• Title: Automating Formal Verification with Agent-Guided Tree Search
• Title（参考訳）: エージェントガイド木探索による形式検証の自動化
• Authors: Leo Yao,
• Abstract要約: 形式的検証は、ソフトウェアを確実に修正する道を提供するが、検証済みのコードを書くのに十分な費用がかかるため、本番ではほとんど使われない。 最近のベンチマークでは、仕様をコードに変換する能力と、マシンチェックによる正確さの反復を計測している。 この論文は、リーンにおけるLCM駆動による検証コード生成の状況を評価し、パフォーマンスを改善するための検索ベースの手法を開発する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification offers a path to provably correct software, but writing verified code remains expensive enough that the technique is rarely used in production. Recent large language models can accelerate this work, and recent benchmarks measure their ability to translate specifications into code and machine-checked proofs of correctness. This thesis evaluates the state of such LLM-driven verified-code generation ("vericoding") in Lean and develops search-based methods for improving verification performance. We first reproduce a subset of the vericoding-benchmark Lean leaderboard on a current cross-vendor model pool, finding that non-reasoning performance remains roughly steady on US closed-source models while open-weight models have slightly improved. We update the iterative methodology of vericoding-benchmark with an agentic loop equipped with mathlib search, finding that model performance greatly improves and scales with agent budget. GPT-5.4 nearly saturates the benchmark at 95.0% on 423 specs with $K=50$ LLM calls. We then design two agent-directed tree-search formulations: a state-based orchestrator that branches on partial-proof states, and a context-based orchestrator that branches on full subagent contexts. Compared against the agent baseline, the context-based design solves a wider range of intermediate-difficulty specs at lower token cost, while the agent baseline retains an advantage on the hardest specs, where uninterrupted iteration matters most. We conclude that search structure has selective advantages over a strong agent baseline, and that more challenging benchmarks drawn from modern code are important to measure and drive further progress in automated formal verification. Code available upon request by contacting the author at leoy@mit.edu.
• Abstract（参考訳）: 形式的検証は、ソフトウェアを確実に修正する道を提供するが、検証済みのコードを書くのに十分な費用がかかるため、本番ではほとんど使われない。 最近の大規模言語モデルは、この作業を加速し、最近のベンチマークでは、仕様をコードに翻訳する能力と、正しさのマシンチェックされた証明を計測している。 この論文は、リーンにおけるLCM駆動の検証コード生成("vericoding")の状態を評価し、検証性能を改善するための検索ベースの手法を開発する。 私たちはまず、現在のクロスベンダモデルプール上で、ベリコードベンチマークのリーンリーダーボードのサブセットを再現し、非合理的なパフォーマンスが米国のクローズドソースモデルでほぼ安定しているのに対して、オープンウェイトモデルはわずかに改善されていることを発見した。 我々は,モデル性能がエージェント予算で大幅に向上し,スケールすることが判明した,エージェントループによる検証ベンチマークの反復的手法を更新する。 GPT-5.4は423のスペックで95.0%とほぼ飽和している。 次に、部分的な保護状態に枝分かれする状態ベースのオーケストレータと、完全なサブエージェントコンテキストに枝分かれするコンテキストベースのオーケストレータという、2つのエージェント指向ツリー検索の定式化を設計する。 エージェントベースラインと比較して、コンテキストベースデザインはトークンコストの低い中間微分スペックの範囲を広く解決する一方、エージェントベースラインは、中断しないイテレーションが最も重要となる最も難しいスペックに有利なままである。 我々は,探索構造が強力なエージェントベースラインに対して選択的に有利であること,また,最新のコードから抽出されたより困難なベンチマークが,自動形式検証のさらなる進歩を促進する上で重要であることを結論付けた。 leoy@mit.edu.comで著者に連絡し、リクエストに応じて利用できるコード。

関連論文リスト

• DocSync: Agentic Documentation Maintenance via Critic-Guided Reflexion [0.0]
  DocSyncは、ドキュメントのメンテナンスを構造的に基盤付けられた反復的な生成タスクとしてフレーム化するエージェントワークフローである。 LoRA適応小言語モデルを用いたDocSyncの資源制約実装を実証的に評価する。 このAST対応エージェントアプローチが標準エンコーダ・デコーダのベースラインを大幅に上回ることを示す。
  論文  参考訳（メタデータ） (2026-05-04T02:41:33Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoderはエージェントコード検証フレームワークである。 コード、不変性、そして証明が共進化する所で、証明・アズ・ユー・ジェネレーション開発を可能にする。
  論文  参考訳（メタデータ） (2026-03-31T00:06:44Z)
• An Agentic Evaluation Framework for AI-Generated Scientific Code in PETSc [7.236134946837382]
  petscagent-benchはエージェント評価エージェントのパラダイムに基づいて構築されたエージェントフレームワークである。 正確性、パフォーマンス、コード品質、アルゴリズムの適切性、ライブラリ固有の規約の5つの評価カテゴリで14評価パイプラインを編成する。 本フレームワークは,HPC用PETScライブラリを用いて,現実的な問題のベンチマークスイート上で実演する。
  論文  参考訳（メタデータ） (2026-03-16T22:46:10Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
  論文  参考訳（メタデータ） (2026-02-10T06:58:26Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
  大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。 LLM生成コードの正確性を保証することは依然として困難である。 検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
  論文  参考訳（メタデータ） (2025-05-29T06:12:52Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。 我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。 当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
  論文  参考訳（メタデータ） (2024-10-12T23:56:19Z)
• Autoregressive Search Engines: Generating Substrings as Document Identifiers [53.0729058170278]
  自動回帰言語モデルは、回答を生成するデファクト標準として現れています。 これまでの研究は、探索空間を階層構造に分割する方法を探究してきた。 本研究では,検索空間の任意の構造を強制しない代替として,経路内のすべてのngramを識別子として使用することを提案する。
  論文  参考訳（メタデータ） (2022-04-22T10:45:01Z)

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

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