論文の概要: MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

• arxiv url: http://arxiv.org/abs/2605.26959v2
• Date: Wed, 27 May 2026 04:48:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-28 17:38:55.159496
• Title: MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
• Title（参考訳）: MerLean-Prover: リーン4の理論実証のための再帰的なループのハーネス
• Authors: Jinzheng Li, Zeru Zhu, Yuanjie Ren,
• Abstract要約: MerLean-Proverは、残念な宣言をカーネルチェック可能な証明に置き換える、エンドツーエンドのLean4定理証明器である。 23のPhD-qualification-exam定理のベンチマークであるFormalQualBenchでは、MerLean-Proverは10/23を解く。 Sonnetは4つのテストされたFormalQualBench問題を全てクローズし、Haikuは2つの短い問題をクローズする。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs. It is built from three agent types (Planning, Check, and Lean) composed by a recursive outer loop whose unit of revision is the proof plan itself, and uses no fine-tuning, no custom RL objective, and no theorem-specific scaffolding. On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23, surpassing the strongest published open-source baseline (OpenGauss, 8/23). On Putnam2025, the same harness closes 12/12 with substantially lower total wall-clock than the next-best system that closes the full set. The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones. These results suggest that harness design is a central factor in end-to-end Lean4 theorem proving, alongside raw model capability, and that a relatively simple harness can already be effective.
• Abstract（参考訳）: MerLean-Proverは、残念な宣言をカーネルチェック可能な証明に置き換える、エンドツーエンドのLean4定理証明器である。 3つのエージェントタイプ(Planning、Check、Lean)で構成され、リビジョンの単位が証明計画自身である再帰的な外ループで構成され、微調整もカスタムRLの目的も、定理固有の足場も使用しない。 23のPhD-qualification-exam定理のベンチマークであるFormalQualBenchでは、MerLean-Proverが10/23を解き、最も強力なオープンソースベースライン(OpenGauss, 8/23)を超えた。 パットナム2025では、同じハーネスが12/12に閉鎖され、全体の壁時計はフルセットを閉じる次のベストシステムよりも大幅に低い。 Sonnetは4つのテストされたFormalQualBench問題を全てクローズし、Haikuは2つの短い問題をクローズする。 これらの結果は、ハーネス設計が、生のモデル能力と並行して、エンドツーエンドのLean4定理の証明の中心的な要素であり、比較的単純なハーネスが既に有効であることを示唆している。

関連論文リスト

• 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)
• Hilbert: Recursively Building Formal Proofs with Informal Reasoning [38.36481253622752]
  大規模言語モデル(LLM)は、驚くべき数学的推論能力を示しているが、そのソリューションには自動検証できないエラーが含まれていることが多い。 非公式な推論と形式的検証の相補的な強みを組み合わせたエージェントフレームワークであるHilbertを紹介する。 我々のシステムは4つのコンポーネントを編成する: 数学的推論に優れる非公式のLLM、リーン4の戦術に最適化された特殊なLLM、形式検証器、意味定理検索器。
  論文  参考訳（メタデータ） (2025-09-26T18:24:23Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Theorem-Validated Reverse Chain-of-Thought Problem Generation for Geometric Reasoning [53.13514542825493]
  TRCoT(Theorem-d Reverse Chain-of-Thought Reasoning Synthesis)フレームワークについて述べる。 最初の段階であるTR-Engineは、構造的な記述と性質を持つ定理基底幾何学図を合成する。 第2段階であるTR-Reasonerは、幾何特性と記述フラグメントを交互に検証することで、反復的に質問と回答のペアを洗練するためのリバース推論を採用している。
  論文  参考訳（メタデータ） (2024-10-23T13:58:39Z)
• 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)
• REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
  我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。 新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。 また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
  論文  参考訳（メタデータ） (2024-02-26T21:21:30Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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