論文の概要: 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ライブラリの進化
- Authors: Youyuan Zhang, Jialiang Sun, Hangrui Bi, Chuqin Geng, Wenjie Ma, Zhaoyu Li, Xujie Si,
- 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は、様々な数学ベンチマークの集合における証明成功率を大幅に改善し、より簡潔な証明と計算コストの削減を図っている。
関連論文リスト
- Gödel's Poetry [0.0]
本稿では,Lean4の証明生成に特殊言語モデルを用いるコンピュータ定理証明の新しいアプローチを提案する。
分解せずにMiniF2Fの90.4%のパスレートを達成する。
重要な技術的貢献は、抽象構文木(AST)解析機能を備えたKimina Lean Serverの拡張にあります。
論文 参考訳（メタデータ） (2025-12-16T10:00:01Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。