論文の概要: LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs
- arxiv url: http://arxiv.org/abs/2610.11862v1
- Date: Thu, 08 Oct 2026 12:40:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-10 02:36:54.02796
- Title: LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs
- Title（参考訳）: LEVER:Adaptive Cost-Aware Proof Search over AND/OR Graphs
- Abstract要約: 本稿では,正しい証明を目的とする証明探索アルゴリズムLEVERを提案する。
リーン4のPatnamBenchでは、一致した予算の下で、LEVERは強力なシングル会話エージェントよりも34%安くなります。
局所的な不純物を減らす、すなわち、証明が定理の主題からどのくらい離れているかは、コストの3分の2でポストホック(42%の33%の減少)よりも改善される。
- 参考スコア（独自算出の注目度）: 13.362400908940915
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Mathematicians value proofs for more than correctness: among correct proofs, simplicity, purity and the computational cost of finding them vary widely. Yet LLM-powered theorem provers largely search for any correct proof, and improve its quality only after it is found. We propose LEVER, a proof search algorithm that makes the objective over correct proofs programmable and optimizes it during search. LEVER scores partial proofs over an AND/OR proof graph, combining realized objective values with predictions for open subgoals, so the objective guides search before a proof is complete. The same mechanism optimizes computational cost, proof length, topical impurity, and even their weighted combinations, while the Lean kernel enforces correctness. On PutnamBench in Lean 4, under matched budgets, LEVER costs 34% less than a strong single-conversation agent while raising the solve rate from 80% to 96%. On reducing topical impurity, i.e., how far a proof strays from its theorem's subject, it improves over post-hoc refactoring (42% reduction against 33%) at two-thirds of the cost and more reliably; on proof length, the metric refactoring is built for, it approaches refactoring. Varying the objective's weights traces a quality-cost trade-off curve, so the user can choose how much a better proof is worth. Overall, LEVER is a performant, cost-efficient and tunable proof search algorithm for navigating the space of correct proofs.
- Abstract（参考訳）: 数学者は、正しい証明、単純さ、純粋さ、そしてそれらを見つけるための計算コストが多様である。
しかし LLM を動力とする定理証明は、ほとんど正しい証明を求め、発見後にのみその品質を向上させる。
本稿では,正解の目的をプログラム可能とし,探索中に最適化する証明探索アルゴリズムLEVERを提案する。
LEVERはAND/OR証明グラフ上で部分的証明をスコアし、実現された目標値をオープンサブゴールの予測と組み合わせることで、証明が完了する前に探索をガイドする。
同じメカニズムは計算コスト、証明の長さ、トピックの不純物、さらには重み付けされた組み合わせを最適化します。
リーン4のPatnamBenchでは、整合した予算の下で、LEVERは強力なシングル会話エージェントよりも34%安くなり、解決率は80%から96%に向上した。
局所的な不純物を減らす、すなわち、証明が定理の主題からどのくらい離れているかは、コストの3分の2のコストでポストホックリファクタリング(33%に対して42%の削減)よりも、より確実に改善される。
目標の重み付けは品質コストのトレードオフ曲線をトレースするので、ユーザはどの程度のより良い証明が価値があるかを選択できます。
LEVERは全体として、正しい証明空間をナビゲートするための性能、費用効率、調整可能な証明探索アルゴリズムである。
関連論文リスト
- Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification [19.12388440070344]
プログラム検証は、定理証明器で構築された機械チェック可能な証明を通じてソフトウェア正当性を確立する。
しかし、ほとんどの既存のプローバーは、サンプリングや検索の予算でのみパスレートを追求している。
CoCo-Proverは、メタレベルの意思決定としてコスト効率の高いプログラムを定式化している。
論文 参考訳（メタデータ） (2026-10-07T08:42:24Z) - Learning to Reason Efficiently with A* Post-Training [119.18396754931602]
大規模言語モデルでは, A* 探索のガイダンスを用いて, 正確かつ効率的な証明を生成することができるかを検討する。
経験的に、1B--3B範囲のLlama-3.2モデルはA*ポストトレーニングの恩恵が大きいことが判明した。
より大きな探索空間では、不完全で訓練されたモデルの方が精度が高い。
論文 参考訳（メタデータ） (2026-05-23T14:28:57Z) - Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness [7.694715050727414]
大規模言語モデル(LLM)は数学的な問題解決に有効である。
ProofRankは、挑戦的な数学的競争から得られたベンチマークである。
正当性のみのベンチマークでは得られない証明品質にはかなりの違いがある。
論文 参考訳（メタデータ） (2026-05-11T11:23:36Z) - Proof Minimization in Neural Network Verification [3.2006701823251578]
ディープニューラルネットワーク(DNN)は複雑なツールであり、健全性を損なう可能性のあるバグが含まれ、検証プロセスの信頼性を損なう可能性がある。
検証過程で学習した事実を除去するアルゴリズムを提案するが、証明自体には不要である。
提案アルゴリズムは,検証プロセス自体に実行時のオーバヘッドを7%～20%導入した上で,証明サイズを37%～82%削減し,検証時間を30%～88%短縮することを示した。
論文 参考訳（メタデータ） (2025-11-11T13:02:30Z) - APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。
エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。
この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
論文 参考訳（メタデータ） (2025-05-09T03:38:31Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
リーンの任意のユーザ定義メトリクスを最適化するために、証明を書き換える大規模な言語モデルエージェントであるImProverを紹介します。
我々は、現実世界の学部生、競争、研究レベルの数学定理の書き換えについてImProverをテストする。
論文 参考訳（メタデータ） (2024-10-07T05:14:18Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。