論文の概要: Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean

• arxiv url: http://arxiv.org/abs/2606.04883v1
• Date: Wed, 03 Jun 2026 13:46:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-04 20:44:18.788558
• Title: Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
• Title（参考訳）: リーンにおけるエージェント定理プローバのコスト-品質トレードオフの最適化
• Authors: Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck, Martin Vechev,
• Abstract要約: 大規模な言語モデル(LLM)は、リーンで形式的な証明を生成するためにますます使われています。 LLMは違法に高価であり、多くの場合、最終的に失敗する試みに相当な計算に費やされる。 本研究では,データプレーンと制御プレーンで構成されるアクションルーティングエージェントを用いてこの問題に対処する。 コントロールプレーンは、失敗していたリーンの試みを観察し、成功の可能性を見積もり、他の試みのコストを見積もり、現在の目標を証明し続けるか、あるいは新たなブレークダウンから再開するかを決めます。
• 参考スコア（独自算出の注目度）: 3.9323543777759014
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proof attempts, and use compiler feedback to guide search. However, they can be prohibitively expensive, often spending substantial compute on attempts that ultimately fail. In this work, we address this problem with an action routing agent that consists of a data plane and a control plane. The data plane generates natural-language lemma decompositions, formalizes them in Lean, and samples proof attempts for the resulting theorem and lemma targets. The control plane observes previous failed Lean attempts, estimates both the likelihood of success and cost of another attempt, and decides whether to continue proving the current target or restart from a new breakdown. On a subset of PutnamBench, our agent decreases the cost by $25.8\%$ over a fixed-step baseline on average, preserving performance while using substantially less compute. These results suggest that failed Lean trajectories provide actionable signals for cost-aware resource allocation in agentic theorem proving.
• Abstract（参考訳）: 大規模な言語モデル(LLM)は、リーンで形式的な証明を生成するワークフローでますます使われています。 これらのワークフローは、しばしば問題を小さな補題に分解し、多くの証明試行をサンプリングし、コンパイラフィードバックを使って検索をガイドする。 しかし、それらは違法に高価であり、多くの場合、最終的に失敗する試みに相当な計算に費やされる。 本研究では,データプレーンと制御プレーンで構成されるアクションルーティングエージェントを用いてこの問題に対処する。 データプレーンは自然言語の補題分解を生成し、それらをLeanで形式化し、結果の定理と補題の目標に対する証明の試みをサンプリングする。 コントロールプレーンは、失敗していたリーンの試みを観察し、成功の可能性を見積もり、他の試みのコストを見積もり、現在の目標を証明し続けるか、あるいは新たなブレークダウンから再開するかを決めます。 PutnamBenchのサブセットでは、エージェントは平均的な固定ステップベースラインに対して25.8\%のコストを削減し、計算量を大幅に減らしながら性能を保っている。 これらの結果は, 失敗に終わったリーン軌道が, エージェント的定理の証明において, コストを意識した資源配分のための実用的な信号を提供することを示している。

関連論文リスト

• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• 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)
• Accelerating LLM Reasoning via Early Rejection with Partial Reward Modeling [12.835376812101323]
  PRMも部分的リワードモデルであるという仮説を導入する。 これにより、中間トークンレベル信号に基づく原理的な早期拒絶が可能となる。 算数推論のベンチマークでは、最終的な性能を劣化させることなく、最大1.4$times$-9$times$の推論FLOPを削減できる。
  論文  参考訳（メタデータ） (2025-08-04T00:58:56Z)
• Runaway is Ashamed, But Helpful: On the Early-Exit Behavior of Large Language Model-based Agents in Embodied Environments [54.67512489842682]
  大規模言語モデル(LLM)は、複雑な実施環境において、強力な計画と意思決定能力を示す。 LLMをベースとしたエージェントの早期退避行動を探究する第一歩を踏み出す。
  論文  参考訳（メタデータ） (2025-05-23T08:23:36Z)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [47.46564769245296]
  タスク分解を用いて問題空間をトラバースする新しい手法を提案する。 我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。 提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
  論文  参考訳（メタデータ） (2024-10-14T19:39:11Z)
• A Voter-Based Stochastic Rejection-Method Framework for Asymptotically Safe Language Model Outputs [0.0]
  本稿では,LLMの安全性を活用して,安全でない,あるいは低品質な大規模言語モデル(LLM)の出力を防止する手法を提案する。 このシステムでは、LCMチェッカーが生成した出力の受理性に投票し、不承認のしきい値に達すると再生する。
  論文  参考訳（メタデータ） (2024-07-24T04:27:55Z)
• Leaving the Nest: Going Beyond Local Loss Functions for Predict-Then-Optimize [57.22851616806617]
  本手法は,文献から得られた4つの領域において,最先端の成果が得られることを示す。 提案手法は, 局所性仮定が破られた場合, 既存手法よりも200%近く性能が向上する。
  論文  参考訳（メタデータ） (2023-05-26T11:17:45Z)

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

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