論文の概要: Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification
- arxiv url: http://arxiv.org/abs/2610.09681v1
- Date: Wed, 07 Oct 2026 08:42:24 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-08 21:58:22.810483
- Title: Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification
- Title（参考訳）: プログラム検証におけるエージェントオーケストレーションによる費用効率の高い理論証明
- Abstract要約: プログラム検証は、定理証明器で構築された機械チェック可能な証明を通じてソフトウェア正当性を確立する。
しかし、ほとんどの既存のプローバーは、サンプリングや検索の予算でのみパスレートを追求している。
CoCo-Proverは、メタレベルの意思決定としてコスト効率の高いプログラムを定式化している。
- 参考スコア（独自算出の注目度）: 19.12388440070344
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Program verification establishes software correctness through machine-checkable proofs constructed in theorem provers. It's a guarantee especially valuable for code generated by large language models (LLMs), which is fluent but carries no assurance of correctness. Almost all existing provers, however, pursue pass rates alone at whatever sampling or search budget it takes, and overlook the success-vs-cost frontier; yet real software often carries hundreds of interdependent proof obligations, so what matters at scale is not whether one theorem can be proved, but how many can be proved economically. We introduce CoCo-Prover, which formalizes cost-efficient program proving as metalevel decision-making under cost, grounded on two-level proof graphs: an AND/OR proof hypergraph within each declaration is joined to a lemma-dependency graph across declarations; and at each step, it answers two questions: which open goals to select, and which actions to purchase on these goals. Selection stays symbolic as a topological pass over the proof graphs. Action choice is agent orchestration via metalevel decision-making: an agentic router treats every bounded specialist invocation as a separately priced, best-effort computation, matching heterogeneous specialist agents together with configurations, under evolved routing rules as evidence accumulates. On five program verification benchmarks in Lean 4 including function-level CLEVER, VERINA, and AlgoVeri, and repository-level NTP4VC and Vero, we show that CoCo-Prover achieves a better success-vs-cost frontier than baselines including frontier coding agents and state-of-the-art LLM-based provers: it achieves the best solve rate on every benchmark and up to 100% on two benchmarks. It also reduces cost by up to 30.9% compared to the strongest baseline with the strongest LLM in our evaluation.
- Abstract（参考訳）: プログラム検証は、定理証明器で構築された機械チェック可能な証明を通じてソフトウェア正当性を確立する。
これは、大きな言語モデル(LLM)によって生成されるコードにとって特に価値のある保証です。
実際のソフトウェアは数百の相互依存的な証明義務を負うことが多いため、スケールにおいて重要なことは、1つの定理が証明できるかどうかではなく、経済的に証明できる回数である。
我々は,コスト効率の高いプログラムをメタレベル意思決定として定式化するCoCo-Proverを紹介し,各宣言内のAND/OR証明ハイパーグラフを宣言間の補題依存グラフに結合し,各ステップにおいて,どの目標を選択するか,どの目標を購入すべきか,という2つの疑問に答える。
選択は証明グラフ上の位相パスとして象徴的である。
エージェントルータは、すべての境界付けられた専門家の呼び出しを、独立した価格でベストエフォートな計算として扱い、異種の専門家のエージェントと構成を一致させ、エビデンスが蓄積されるにつれて進化したルーティングルールの下で処理する。
関数レベルのCLEVER、VERINA、AlgoVeri、リポジトリレベルのNTP4VC、Veroを含むLean 4の5つのプログラム検証ベンチマークでは、CoCo-Proverは、フロンティアコーディングエージェントや最先端のLCMベースのプロバーを含むベースラインよりも、成功率の高いフロンティアを実現している。
また、評価において最強のLCMを持つ最強のベースラインと比較して、最大で30.9%のコスト削減を実現しています。
関連論文リスト
- P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation [19.3449645807529]
検証されたコード生成は、プログラムの実行可能プログラムとマシンチェック可能な証明の両方を生成するために、大きな言語モデル(LLM)を要求する。
このシーケンシャルパイプラインは、実際には非効率かつ非効率である可能性があることを観察する。
プログラムとその正当性引数を手作業で開発するべきだというディクストラの見解に触発されて、我々は$P3$を提案する。
論文 参考訳（メタデータ） (2026-08-10T08:33:18Z) - Harnessing Code Agents for Automatic Software Verification [0.47154736035631406]
大規模言語モデル(LLM)は、自動的に証明を生成することを約束するが、既存のアプローチは、固定された人間設計の証明戦略をシステムに結び付ける。
このような戦略を課すことは不要で制限的であることを示す。
レムマ全体を一般的なコードエージェントに手渡して、独自のアプローチを自由に選択し、検証ハーネスにラップすることは、シンプルでより効果的です。
論文 参考訳（メタデータ） (2026-07-07T14:39:59Z) - Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs [21.65389718022749]
提案するQuarryは,証明計画と証明実行を分離した,計画に基づく証明合成フレームワークである。
特に、Quarry は LLM に対して、任意のサブレンマを持つ複数の証明分解を積極的に提案するよう求め、Rocq で一時的に承認されたサブレンマの下でそれらをタイプチェックし、証明状態に基づく困難モデルを用いて候補をランク付けする。
可解性を考慮した評価による計画ベース分解は,予測可能なコストを維持しつつ,自動化を大幅に改善することを示す。
論文 参考訳（メタデータ） (2026-06-16T14:33:15Z) - HELP: HyperNode Expansion and Logical Path-Guided Evidence Localization for Accurate and Efficient GraphRAG [53.30561659838455]
大きな言語モデル(LLM)は、しばしば固有の知識境界と幻覚に苦しむ。
Retrieval-Augmented Generation (RAG) は、マルチホップ推論に不可欠な構造的相互依存性をしばしば見落としている。
ヘルプは、複数の単純でマルチホップなQAベンチマークで競合性能を達成し、グラフベースのRAGベースラインよりも28.8$times$のスピードアップを実現している。
論文 参考訳（メタデータ） (2026-02-24T14:05:29Z) - The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee [5.345468714252351]
この研究は LLM-Verifier Convergence Theorem の開発によってギャップを埋める。
LLMと検証器の相互作用を離散時間マルコフ連鎖としてモデル化する。
われわれはこの予測を90,000件以上の治験を含む広範囲な実証キャンペーンでストレステストした。
論文 参考訳（メタデータ） (2025-11-30T22:19:09Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
暗黙的な検索と構造化された協調を組み合わせた統合フレームワークを開発する。
Humanity's Last Exam (HLE) Bio/Chem Goldでは,48.3%の精度を実現している。
SuperGPQAとTRQAの結果はドメイン間の堅牢性を確認した。
論文 参考訳（メタデータ） (2025-09-25T14:05:55Z) - Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。
LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。
本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文 参考訳（メタデータ） (2024-10-05T05:21:48Z) - Self-Evaluation Guided Beam Search for Reasoning [61.523627290397556]
我々は,Large Language Model (LLM) の推論プロセスのガイドと校正を行うための段階的自己評価機構を導入する。
本稿では,ビームサーチによる自己評価ガイダンスを統合した復号アルゴリズムを提案する。
我々のアプローチは、GSM8K、AQuA、StrategyQAにおいて、対応するCodexバックボンドベースラインをわずかに精度6.34%、9.56%、および5.46%で上回る。
論文 参考訳（メタデータ） (2023-05-01T02:37:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。