論文の概要: Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models

• arxiv url: http://arxiv.org/abs/2506.11487v1
• Date: Fri, 13 Jun 2025 06:25:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-16 17:50:49.674639
• Title: Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
• Title（参考訳）: Reasoning Model 時代における高度な理論実証のための DSP の復活
• Authors: Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, Fan Yang,
• Abstract要約: 本稿では,Draft,Sketch,Proveフレームワークの改良版であるtextbfDSP+を紹介する。 相ごとに微細で統合されたニューロシンボリックエンハンスメントを特徴とする。 DSP+は、MiniF2F、ProofNet、PatnamBenchから80.7%、32.8%、24の644の問題を解決する。
• 参考スコア（独自算出の注目度）: 13.498044623556737
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advancements, such as DeepSeek-Prover-V2-671B and Kimina-Prover-Preview-72B, demonstrate a prevailing trend in leveraging reinforcement learning (RL)-based large-scale training for automated theorem proving. Surprisingly, we discover that even without any training, careful neuro-symbolic coordination of existing off-the-shelf reasoning models and tactic step provers can achieve comparable performance. This paper introduces \textbf{DSP+}, an improved version of the Draft, Sketch, and Prove framework, featuring a \emph{fine-grained and integrated} neuro-symbolic enhancement for each phase: (1) In the draft phase, we prompt reasoning models to generate concise natural-language subgoals to benefit the sketch phase, removing thinking tokens and references to human-written proofs; (2) In the sketch phase, subgoals are autoformalized with hypotheses to benefit the proving phase, and sketch lines containing syntactic errors are masked according to predefined rules; (3) In the proving phase, we tightly integrate symbolic search methods like Aesop with step provers to establish proofs for the sketch subgoals. Experimental results show that, without any additional model training or fine-tuning, DSP+ solves 80.7\%, 32.8\%, and 24 out of 644 problems from miniF2F, ProofNet, and PutnamBench, respectively, while requiring fewer budgets compared to state-of-the-arts. DSP+ proves \texttt{imo\_2019\_p1}, an IMO problem in miniF2F that is not solved by any prior work. Additionally, DSP+ generates proof patterns comprehensible by human experts, facilitating the identification of formalization errors; For example, eight wrongly formalized statements in miniF2F are discovered. Our results highlight the potential of classical reasoning patterns besides the RL-based training. All components will be open-sourced.
• Abstract（参考訳）: 近年のDeepSeek-Prover-V2-671BやKimina-Prover-Preview-72Bのような進歩は、自動定理証明のための強化学習(RL)に基づく大規模学習の活用において顕著な傾向を示している。 驚くべきことに、トレーニングがなくても、既存のオフ・ザ・シェルフ推論モデルと戦術ステッププロデューサの神経-記号的調整が同等のパフォーマンスを達成できることがわかりました。 筆者らは,(1) ドラフト段階では, 簡潔な自然言語サブゴールを生成するための推論モデルにより, スケッチフェーズの恩恵を享受し, 思考トークンや人間による証明への参照を排除し, (2) スケッチフェーズでは, サブゴールは, 証明フェーズの利益を期待する仮説で自動生成され, 構文誤差を含むスケッチラインは, 予め定義されたルールに従って隠蔽される; (3) 証明フェーズでは, Aopesのような記号的検索手法を, より厳密に統合して, スケッチフェーズの証明を行う。 実験結果は、追加のモデルトレーニングや微調整がなければ、DSP+は、MiniF2F、ProofNet、PatnamBenchの644問題のうち、80.7\%、32.8\%、24の問題を解決し、最先端技術と比べて予算が少なくなることを示している。 DSP+ は miniF2F の IMO 問題である \texttt{imo\_2019\_p1} を証明している。 さらに、DSP+は人間の専門家によって理解可能な証明パターンを生成し、形式化エラーの識別を容易にする。 以上の結果から,古典的推論パターンの可能性を浮き彫りにした。 すべてのコンポーネントはオープンソースになる。

関連論文リスト

• Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning [38.4246156415702]
  Kimina-Proverは、形式的定理証明のための新しい推論駆動探索パラダイムを開拓した大きな言語モデルである。 Qwen2.5-72Bから大規模な強化学習パイプラインでトレーニングされたKimina-Proverは、Lean 4の証明生成において、強力なパフォーマンスを示している。 Kimina-Prover は miniF2F ベンチマークに新しい最先端をセットし、pass@8192 で 80.7% に達した。
  論文  参考訳（メタデータ） (2025-04-15T16:23:44Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• A Fixed-Point Approach for Causal Generative Modeling [20.88890689294816]
  本稿では,構造因果モデル(Structure Causal Models, SCM)を因果順序付き変数の固定点問題として記述する新しい形式論を提案する。 トポロジカル順序付け(TO)を考えると,その特異な回復のために最も弱い既知の条件を確立する。
  論文  参考訳（メタデータ） (2024-04-10T12:29:05Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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