論文の概要: Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation

• arxiv url: http://arxiv.org/abs/2606.19315v1
• Date: Wed, 17 Jun 2026 17:38:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-18 17:16:51.292964
• Title: Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation
• Title（参考訳）: Diffusion-Proof: 自己回帰生成を超えた形式理論のレシピ
• Authors: Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, Tong Zhang,
• Abstract要約: 我々は、我々の知識を最大限に活用するために、形式的定理証明のためにdLLMを訓練し適用する最初のフレームワーク**Diffusion-Proof*を提案する。 我々は,*Diffusion-Proof* が ProofNet-Test で **1.61%* を,***6.14%* が MiniF2F-Test ベンチマークで **1.61%* を絶対的に改善したことを示す。 特に**Diffusion-Proof*は、より先進的な思考モデルであるDeepSeek-Prover-V2-7Bが解決できなかった1つのIMO問題を解決することに成功した。
• 参考スコア（独自算出の注目度）: 22.715237995633625
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Enhancing the formal math reasoning capabilities of Large Language Models (LLMs) has become a key focus in both mathematical and computer science communities in recent years. While significant progress has been made in using state-of-the-art Auto-Regressive (AR) LLMs for formal theorem proving, these models suffer from inherent limitations. Their next-token prediction generation methods may yield suboptimal performance due to the challenges of long-range coherence and the compounding of errors over long sequences. Recent advancements in diffusion LLMs (dLLMs), which generate text through iterative denoising of a multi-token block, offer a promising alternative. However, the application of dLLMs to formal mathematics, where maintaining long-range coherence is critical, remains largely understudied. To address the challenges above, we propose **Diffusion-Proof**, to the best of our knowledge, the first framework to train and apply dLLMs for formal theorem proving. Our frameworks contain training and inference methods for two models. The first one is *dLLM-Prover-7B*, which performs whole-proof writing with long-range coherent tactic usage. The second one is *dLLM-Corrector-7B*, which is a novel large block diffusion-based correction model. It leverages the in-filling capabilities of dLLMs to perform local proof correction using bi-directional information. Extensive experiments demonstrate that **Diffusion-Proof** relatively significantly outperforms the AR LLM baseline trained under the same dataset. **Diffusion-Proof** achieves an absolute improvement of **1.61%** on ProofNet-Test and **6.14%** on MiniF2F-Test benchmarks compare to the baseline. Notably, **Diffusion-Proof** successfully resolves one IMO problem that more advanced thinking model DeepSeek-Prover-V2-7B could not solve, showcasing the unique advantage of dLLMs in formal theorem proving.
• Abstract（参考訳）: 近年,Large Language Models (LLMs) の数学的推論能力の強化は,数学と計算機科学の両分野において重要な焦点となっている。 形式的定理証明に最先端のAuto-Regressive (AR) LLMを使用することで大きな進歩があったが、これらのモデルは固有の制限に悩まされている。 それらの次トーケン予測生成手法は、長距離コヒーレンス(英語版)の課題と長い列上のエラーの複合化により、最適以下の性能が得られる可能性がある。 近年の拡散 LLM (dLLMs) の進歩は, マルチトークンブロックの反復的 denoising を通じてテキストを生成することで, 有望な代替手段を提供する。 しかし、長距離コヒーレンスを維持する形式数学への dLLMs の適用は極めて重要であり、ほとんど検討されていない。 上記の課題に対処するため、我々は**Diffusion-Proof* を提案し、私たちの知識を最大限に活用し、公式な定理証明のために dLLM を訓練し適用する最初のフレームワークである。 フレームワークには2つのモデルのトレーニングと推論方法が含まれています。 ひとつは *dLLM-Prover-7B* で、長距離コヒーレントな戦術的使用による完全防御的な書き込みを実行する。 2つ目は *dLLM-Corrector-7B* で、これは新しい大きなブロック拡散に基づく補正モデルである。 これはdLLMの補充能力を活用し、双方向情報を用いた局所的証明補正を行う。 大規模な実験では、**Diffusion-Proof*は、同じデータセットでトレーニングされたAR LLMベースラインよりも比較的優れています。 **Diffusion-Proof*はProofNet-Testで**1.61%*、***6.14%*はMiniF2F-Testベンチマークで**1.61%*を絶対的に改善する。 特に**Diffusion-Proof** はより高度な思考モデル DeepSeek-Prover-V2-7B が解けないという IMO 問題の1つの解決に成功し、形式定理証明における dLLM のユニークな利点を示している。

関連論文リスト

• Test-Time Scaling with Diffusion Language Models via Reward-Guided Stitching [66.39914384073145]
  本稿では,安価な拡散サンプリング推論をステップレベル候補の再利用プールに変換する自己整合性フレームワークを提案する。 ステップレベルの再結合は、難しい問題に対して最も有益であることがわかった。 トレーニング不要のフレームワークは、6つの数学およびコーディングタスクの平均精度を最大2倍改善します。
  論文  参考訳（メタデータ） (2026-02-26T11:08:39Z)
• DiffuRank: Effective Document Reranking with Diffusion Language Models [71.16830004674513]
  拡散言語モデル(dLLM)に基づいて構築されたフレームワークであるDiffuRankを提案する。 dLLMは、左から右への順序に制約されないより柔軟なデコーディングと生成プロセスをサポートする。 モデルサイズが類似した自己回帰LDMに匹敵する性能を示す。
  論文  参考訳（メタデータ） (2026-02-13T02:18:14Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。 テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。 そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
  論文  参考訳（メタデータ） (2026-02-02T09:14:51Z)
• DiRL: An Efficient Post-Training Framework for Diffusion Language Models [54.405206032785706]
  Diffusion Language Models (dLLMs) はAuto-Regressive(AR)モデルに代わる有望な代替品として登場した。 既存の手法は、訓練と推論の間の計算の非効率性と客観的なミスマッチに悩まされている。 我々は,FlexAttention-accelerated blockwise trainingとLMDeploy-timized inferenceを密接に統合した,効率的なポストトレーニングフレームワークであるDiRLを紹介した。
  論文  参考訳（メタデータ） (2025-12-23T08:33:19Z)
• Diffusion LLMs Can Do Faster-Than-AR Inference via Discrete Diffusion Forcing [14.22753953706955]
  Diffusion Large Language Models (dLLMs) は、テキスト生成のための自動回帰(AR) LLM に代わる有望な代替品として登場した。 本稿では、離散拡散強制(D2F)と呼ばれる単純かつ効果的な戦略に基づいて、この障壁を破る。 このようにして、バニラdLLMは効率的な推論のためにAR拡散ハイブリッドパラダイムに再構成される。
  論文  参考訳（メタデータ） (2025-08-08T04:51:37Z)
• DiffuCoder: Understanding and Improving Masked Diffusion Models for Code Generation [68.19756761027351]
  拡散大言語モデル(dLLM)は自己回帰(AR)モデルの魅力的な代替品である。 本研究は,それらの認知過程と強化学習手法について考察する。 我々の研究は、dLLM生成のメカニズムについて深い洞察を与え、効果的な拡散ネイティブなRLトレーニングフレームワークを提供します。
  論文  参考訳（メタデータ） (2025-06-25T17:35:47Z)
• d1: Scaling Reasoning in Diffusion Large Language Models via Reinforcement Learning [31.531278643184656]
  最近の大規模言語モデル(LLM)は、オンライン強化学習(RL)の恩恵を受ける強力な推論能力を示している。 教師付きファインタニング(SFT)とRLの組み合わせにより,事前学習したマスク付きdLLMを推論モデルに適応するフレームワークであるd1を提案する。 d1は最高の性能を示し、最先端のdLLMの性能を大幅に向上させる。
  論文  参考訳（メタデータ） (2025-04-16T16:08:45Z)

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

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