論文の概要: Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4

• arxiv url: http://arxiv.org/abs/2604.15839v1
• Date: Fri, 17 Apr 2026 08:40:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-20 22:00:19.833335
• Title: Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
• Title（参考訳）: Discover and Prove: リーン4で証明されたハードモード自動理論のためのオープンソースのエージェントフレームワーク
• Abstract要約: ほとんどのATPベンチマークは、最終回答を公式なステートメントに埋め込んでいる。 私たちはより厳格でリアルな設定を「ハードモード」と呼びます。 システムは、正式な証明を作る前に、独立して答えを見つけなければならない。
• 参考スコア（独自算出の注目度）: 32.91257060425129
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Most ATP benchmarks embed the final answer within the formal statement -- a convention we call "Easy Mode" -- a design that simplifies the task relative to what human competitors face and may lead to optimistic estimates of model capability. We call the stricter, more realistic setting "Hard Mode": the system must independently discover the answer before constructing a formal proof. To enable Hard Mode research, we make two contributions. First, we release MiniF2F-Hard and FIMO-Hard, expert-reannotated Hard Mode variants of two widely-used ATP benchmarks. Second, we introduce Discover And Prove (DAP), an agentic framework that uses LLM natural-language reasoning with explicit self-reflection to discover answers, then rewrites Hard Mode statements into Easy Mode ones for existing ATP provers. DAP sets the state of the art: on CombiBench it raises solved problems from 7 (previous SOTA, Pass@16) to 10; on PutnamBench it is the first system to formally prove 36 theorems in Hard Mode -- while simultaneously revealing that state-of-the-art LLMs exceed 80% answer accuracy on the same problems where formal provers manage under 10%, exposing a substantial gap that Hard Mode benchmarks are uniquely suited to measure.
• Abstract（参考訳）: ほとんどのATPベンチマークは、最終的な答えをフォーマルなステートメント(私たちが"Easy Mode"と呼ぶ慣例)に埋め込んでいます。 私たちは、より厳密でより現実的な「ハードモード」と呼んでいる。 ハードモードの研究を可能にするために、私たちは2つのコントリビューションを行います。 まず、広く使われている2つのATPベンチマークのエキスパート対応ハードモードであるMiniF2F-HardとFIMO-Hardをリリースする。 第二にDiscover And Prove (DAP) は LLM の自然言語推論と明示的な自己回帰を用いたエージェントフレームワークで,解答を探索し,その後,既存の ATP プローバ用の Easy Mode 文にハードモード文を書き換える。 コンビベンチでは7(以前のSOTA、Pass@16)から10まで問題を提起し、パットナムベンチでは36の定理をハードモードで正式に証明した最初のシステムである。

関連論文リスト

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Mode-as-Sequence: Translating Multimodal Motion Prediction into Unified Sequential Mode Modeling [31.631345414385382]
  マルチモーダル・モーション・予測は本質的に監督下にある。 そこで本研究では,非順序モードセットを順序モードシーケンスに変換する統合デコードフレームワークであるMode-as-Sequenceを提案する。 ランキング指向メトリクスとデータセット、地平線、オブジェクトタイプ間でのベスト・オブ・Kの精度の両面で一貫した改善を示す。
  論文  参考訳（メタデータ） (2026-05-21T11:37:17Z)
• Policy Split: Incentivizing Dual-Mode Exploration in LLM Reinforcement with Dual-Mode Entropy Regularization [53.051213470905935]
  Policy Splitは、ポリシーを通常の高エントロピーモードと高エントロピープロンプトに分岐させる新しいパラダイムである。 モデルパラメータを共有しながら、2つのモードは異なる目的に合わせて協調的な二重モードエントロピー正規化を行う。
  論文  参考訳（メタデータ） (2026-04-13T14:13:06Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。 低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。 提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
  論文  参考訳（メタデータ） (2025-07-07T22:38:49Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving [33.61458249318183]
  セルフプレイ・セオレム・プロバー(STP)は、予想と証明という2つの役割を担っている。 STPは同時に、予想と証明という2つの役割を担っている。 私たちはLeanとIsabelleの2つの形式的検証ツールで評価します。
  論文  参考訳（メタデータ） (2025-01-31T23:01:48Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• FreshLLMs: Refreshing Large Language Models with Search Engine Augmentation [92.43001160060376]
  本研究では,現在の世界知識をテストする質問に答える文脈において,大規模言語モデル(LLM)の事実性について検討する。 多様な質問や回答のタイプを含む新しい動的QAベンチマークであるFreshQAを紹介する。 我々は,2モード評価法により,閉じたLLMとオープンソースのLLMの多種多様な配列をベンチマークし,その正しさと幻覚の両面を計測する。 これらの結果に触発されたFreshPromptは、FreshQA上でのLLMの性能を大幅に向上させる単純な数ショットプロンプトである。
  論文  参考訳（メタデータ） (2023-10-05T00:04:12Z)

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

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