論文の概要: DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent

• arxiv url: http://arxiv.org/abs/2604.26311v1
• Date: Wed, 29 Apr 2026 05:35:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-30 15:59:36.262518
• Title: DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent
• Title（参考訳）: DreamProver: Wake-Sleep Theorem-Proving Agentによるトランスファー可能なLemmaライブラリの進化
• Abstract要約: 既存のアプローチは、適応性を制限する固定された補題ライブラリに依存するか、あるいは個々の定理に合わせて高度に特定の中間補題を合成する。 DreamProverは、反復的な2段階のプロセスを通じて、このギャップに対処する。 ウェイクステージでは、DreamProverは、現在の補題ライブラリを使用して、新しい候補補題を提案しながら、トレーニングセットから定理を証明しようと試みている。 スリープ」の段階では、ライブラリを圧縮し最適化するためにこれらの候補を抽象化し、洗練し、統合する。
• 参考スコア（独自算出の注目度）: 16.041659918901665
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce DreamProver, an agentic framework that leverages a "wake-sleep" program induction paradigm to discover reusable lemmas for formal theorem proving. Existing approaches either rely on fixed lemma libraries, which limit adaptability, or synthesize highly specific intermediate lemmas tailored to individual theorems, thereby lacking generality. DreamProver addresses this gap through an iterative two-stage process. In the wake stage, DreamProver attempts to prove theorems from a training set using the current lemma library while proposing new candidate lemmas. In the "sleep" stage, it abstracts, refines, and consolidates these candidates to compress and optimize the library. Through this alternating cycle, DreamProver progressively evolves a compact set of high-level, transferable lemmas that can be effectively used to prove unseen theorems in related domains. Experimental results demonstrate that DreamProver substantially improves proof success rates across a diverse set of mathematical benchmarks, while also producing more concise proofs and reducing computational cost.
• Abstract（参考訳）: 本稿では,「覚醒」プログラム誘導パラダイムを活用するエージェントフレームワークであるDreamProverを紹介し,形式的定理証明のための再利用可能な補題を発見する。 既存のアプローチは、適応性を制限する固定された補題ライブラリに依存するか、あるいは個々の定理に合わせて高度に特定の中間補題を合成する。 DreamProverは、反復的な2段階のプロセスを通じて、このギャップに対処する。 ウェイクステージでは、DreamProverは、現在の補題ライブラリを使用して、新しい候補補題を提案しながら、トレーニングセットから定理を証明しようと試みている。 スリープ」の段階では、ライブラリを圧縮し最適化するためにこれらの候補を抽象化し、洗練し、統合する。 この交互サイクルを通じて、ドリームプロバーは、関連する領域における目に見えない定理を効果的に証明できるような、高レベルで移動可能な補題のコンパクトな集合を徐々に進化させる。 実験の結果、DreamProverは、様々な数学ベンチマークの集合における証明成功率を大幅に改善し、より簡潔な証明と計算コストの削減を図っている。

関連論文リスト

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Gödel's Poetry [0.0]
  本稿では,Lean4の証明生成に特殊言語モデルを用いるコンピュータ定理証明の新しいアプローチを提案する。 分解せずにMiniF2Fの90.4%のパスレートを達成する。 重要な技術的貢献は、抽象構文木(AST)解析機能を備えたKimina Lean Serverの拡張にあります。
  論文  参考訳（メタデータ） (2025-12-16T10:00:01Z)
• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
  本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。 IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。 シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
  論文  参考訳（メタデータ） (2025-07-31T17:00:30Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation [27.60611509339328]
  1つのトレーニングデータサンプルの最適順序は、特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに発生すると論じる。 証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。
  論文  参考訳（メタデータ） (2024-10-30T18:00:04Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。 PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。 本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
  論文  参考訳（メタデータ） (2021-06-02T17:58:35Z)

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

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