論文の概要: Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
- arxiv url: http://arxiv.org/abs/2608.28639v1
- Date: Tue, 11 Aug 2026 04:28:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-06 19:38:41.459187
- Title: Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
- Title（参考訳）: Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
- Abstract要約: 我々は,Lean 4コンパイラを報奨託書として純粋に扱う3ロールのMonte Carlo Tree Search (MCTS)フレームワークを提案する。
本フレームワークは,証明探索を3つの役割に分解する:証明試行ジェネレータ,サブゴール分解の分解器,サブゴール品質評価の批判器である。
PAB@256 で Goedel-Prover-V2-8B を用いて MiniF2F の87.1% を達成し,PAB@32 で26/659 パットナムベンチ問題を同じ証明試行予算で 18/659 を突破した。
- 参考スコア（独自算出の注目度）: 5.8296917468117835
- License: http://creativecommons.org/publicdomain/zero/1.0/
- Abstract: Formal theorem proving with large language models remains challenging due to the difficulty of navigating large proof search spaces efficiently. Existing tree search approaches either feed verbose compiler error messages directly into the generation context, increasing context usage during search, or employ non-standard evaluation protocols that prevent direct comparison with established baselines. We propose a three-role Monte Carlo Tree Search (MCTS) framework that treats the Lean 4 compiler purely as a reward oracle using compiler output as a scalar signal for UCB-guided tree updates without feeding error content into the generation context. Our framework decomposes proof search into three roles: a generator for proof attempts, a decomposer for subgoal decomposition, and a critic for subgoal quality evaluation. We evaluate across 4 benchmarks spanning competition mathematics and physics (MiniF2F, PutnamBench, LeanPhysBench, PhysLeandata) with three prover models at standard proof attempt budgets (PAB@16 to PAB@256). Our method achieves 87.1\% on MiniF2F with Goedel-Prover-V2-8B at PAB@256 and solves 26/659 PutnamBench problems at PAB@32 surpassing base sampling 18/659 at same proof attempt budget. Through an exhaustive axiom-level audit of every compiled proof, we further identify reward hacking in search-based theorem proving: DeepSeek-Prover-V2-7B produces proofs on PutnamBench that pass compilation and the standard sorry-token scan while depending on sorryAx. The audit removes 4 and 8 such proofs from whole-proof sampling at PAB@32 and PAB@128, and 11 and 19 from MCTS. We do not attribute these counts to the search procedure; we report them to establish that kernel-level auditing is necessary for compiler-verified evaluation.
- Abstract（参考訳）: 大きな言語モデルで証明された形式定理は、大きな証明探索空間を効率的にナビゲートすることが困難であるため、依然として困難である。
既存のツリー検索アプローチは、冗長なコンパイラエラーメッセージを生成コンテキストに直接フィードするか、検索中のコンテキスト使用量を増やすか、あるいは確立されたベースラインとの直接比較を防ぐために、非標準評価プロトコルを使用するかのいずれかである。
本稿では,UCB誘導ツリー更新のためのスカラー信号としてコンパイラ出力を用いて,Lean 4コンパイラを純粋に報酬オラクルとして扱う3ロールモンテカルロ木探索(MCTS)フレームワークを提案する。
本フレームワークは,証明探索を3つの役割に分解する:証明試行ジェネレータ,サブゴール分解の分解器,サブゴール品質評価の批判器である。
我々は,競争数学と物理学を対象とする4つのベンチマーク(MiniF2F,PatnamBench,LeanPhysBench,PhysLeandata)を,標準的な証明試行予算(PAB@16からPAB@256)で評価した。
PAB@256におけるGoedel-Prover-V2-8BによるMiniF2Fの87.1\%を達成し,PAB@32における26/659 PutnamBench問題を,同じ実証試行予算でベースサンプリング18/659を上回った。
DeepSeek-Prover-V2-7Bは、コンパイルをパスするPutnamBenchの証明と、 sorryAx に依存しながら標準の sorry-token スキャンを生成する。
監査では、PAB@32とPAB@128の完全なサンプリングから4と8の証明を取り除き、MCTSから11と19の証明を取り除いた。
本報告では,カーネルレベルの監査がコンパイラ検証に必要であることを示すために,これらのカウントを検索手順に当てはまらない。
関連論文リスト
- Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation [27.324913853284404]
Pythagoras-Prover(ピタゴラス・プロバー)は、実用的な計算予算のために開発された、リーンの定理プローバーの計算効率のよいファミリーである。
学習効率を向上させるために、カリキュラムSFTの簡単で中堅な問題に階層化されたリーン検証コーパスを構築します。
Augmented Lean Formalisation (ALF)も導入しています。
論文 参考訳（メタデータ） (2026-06-10T18:43:11Z) - Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement [69.77146194380488]
私たちはGoedel-Architectを紹介します。これは、青写真の生成と洗練に焦点を当てたLean 4で証明された公式な定理のためのフレームワークです。
Goedel-ArchitectがMiniF2Fテストで99.2%パス@1、PutnamBenchで75.6%パス@1を達成した。
これは、同等のオープンソースパイプラインよりも500倍低い価格で、オープンソースパイプラインの最先端のパフォーマンスを示している。
論文 参考訳（メタデータ） (2026-06-04T17:54:44Z) - Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search [50.16356451328644]
シャノン型エントロピーの不等式を証明することは情報理論の基本的な課題である。
我々は,原子実証のステップを微調整した小規模大規模言語モデルがこのプロセスを自動化することができるか検討する。
GPT-5.5は0ショットプロンプトで1.7%のサンプルを解き、Psitipは33.3%のサンプルを解いた。
論文 参考訳（メタデータ） (2026-06-04T05:43:12Z) - Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4 [1.2816802110958607]
これは、一度精巧な証明状態をキャプチャし、Lean 4言語サーバーへの小さな拡張を通じてブランチ間で再利用します。
48のミニF2F-v2問題に対して,本手法は標準的なフォールバックよりも5.6～50倍の高速化を実現する。
論文 参考訳（メタデータ） (2026-05-25T08:12:26Z) - OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
OProverは、Lean 4.0で証明された代理的な形式的な反復定理のための統一されたフレームワークである。
エージェント証明を実行し、新たに証明された証明をOProofsと検索メモリにインデックスし、修理軌跡をSFTデータとして使用し、未解決のハードケースをRLに使用する。
OProver-32BはMiniF2F (93.3%)、ProverBench (58.2%)、PutnamBench (11.3%)で最高のパス@32を獲得し、MathOlympiad (22.8%)、ProofNet (33.2%)で上位にランクインしている。
論文 参考訳（メタデータ） (2026-05-17T06:39:05Z) - Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。
我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。
我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-13T01:33:20Z) - Reliable Fine-Grained Evaluation of Natural Language Math Proofs [30.992321135182905]
本稿では,0-7スケールの微粒なスコアをモデル生成数学の証明に割り当てる評価器を開発するための体系的手法を提案する。
ProofBenchは,6つの主要な数学コンペティションから145の問題にまたがる,詳細な証明評価のエキスパートによる最初のデータセットである。
本稿では,強力な推論バックボーンLMと参照解とマーキングスキームからのリッチコンテキストを組み合わせた評価器ProofGraderと,シンプルなアンサンブル手法を提案する。
論文 参考訳（メタデータ） (2025-10-14T02:59:07Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。
この合成データセットでDeepSeekMath 7Bモデルを微調整します。
我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文 参考訳（メタデータ） (2024-05-23T09:03:42Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。