論文の概要: Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

• arxiv url: http://arxiv.org/abs/2508.03613v1
• Date: Tue, 05 Aug 2025 16:28:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-06 18:18:56.073522
• Title: Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
• Title（参考訳）: Goedel-Prover-V2:Scaffoldedデータ合成と自己補正による形式理論のスケーリング
• Authors: Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, Chi Jin,
• Abstract要約: 一連のオープンソースの言語モデルであるGoedel-Prover-V2は、自動定理の新たな最先端を証明した。 我々は、より複雑な定理をマスターするためにモデルを訓練することの困難さを増す合成タスクを生成する。 Goedel-Prover-V2-32Bは、標準モードのpass@32でMiniF2Fの88.1%、自己補正モードの90.4%を達成する。
• 参考スコア（独自算出の注目度）: 95.91743732150233
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: We introduce Goedel-Prover-V2, a series of open-source language models that set a new state-of-the-art in automated theorem proving. Built on the standard expert iteration and reinforcement learning pipeline, our approach incorporates three key innovations: (1) Scaffolded data synthesis: We generate synthetic tasks of increasing difficulty to train the model to master increasingly complex theorems; (2) Verifier-guided self-correction: We enable the model to iteratively revise its proofs by leveraging feedback from the Lean compiler; (3) Model averaging: We merge model checkpoints to mitigate the decrease in model output diversity in later stages of training. Our small model, Goedel-Prover-V2-8B, reaches 84.6% pass@32 on MiniF2F and outperforms DeepSeek-Prover-V2-671B under the same metric, despite being 80X smaller. Our flagship model, Goedel-Prover-V2-32B, achieves 88.1% on MiniF2F at pass@32 in standard mode and 90.4% in self-correction mode, outperforming prior SOTA by a large margin. Additionally, our flagship model solves 86 problems on PutnamBench at pass@184, securing the first place among open-source models on the leaderboard, surpassing DeepSeek-Prover-V2-671B's record of solving 47 problems by pass@1024 with a significantly smaller model size and compute budget. At the time of its release (July-August 2025), Goedel-Prover-V2 achieves the strongest overall performance among all open-source theorem provers. It also ranks among the top-performing models--including closed-source systems with publicly reported performance--under a constrained test-time compute budget. Our models, code, and data are released at https://github.com/Goedel-LM/Goedel-Prover-V2.
• Abstract（参考訳）: Goedel-Prover-V2は、一連のオープンソースの言語モデルであり、自動定理証明における新しい最先端技術を確立している。 標準のエキスパートイテレーションと強化学習パイプラインに基づいて構築されたアプローチでは,3つの重要なイノベーションが組み込まれています。(1) 共有データ合成: より複雑な定理を習得するためにモデルをトレーニングすることの困難さを増す合成タスク,(2) 検証ガイドによる自己補正: リーンコンパイラからのフィードバックを活用して,モデルを反復的に修正可能にすること,(3) モデル平均化: モデルの出力多様性の低下を軽減するために,モデルチェックポイントをマージする,という方法です。 私たちの小さなモデルであるGoedel-Prover-V2-8Bは、MiniF2Fで84.6%のpass@32に達し、80倍小さいにもかかわらず、DeepSeek-Prover-V2-671Bより優れています。 我々のフラッグシップモデルであるGoedel-Prover-V2-32Bは、標準モードではpass@32でMiniF2Fで88.1%、自己補正モードでは90.4%を達成し、SOTAよりも大きなマージンで上回っている。 さらに、当社のフラッグシップモデルはPatnamBenchのpass@184で86の問題を解決し、DeepSeek-Prover-V2-671Bによる、モデルサイズと計算予算が大幅に小さくなった47の問題を解決するという、DeepSeek-Prover-V2-671Bの記録を破って、リーダボード上のオープンソースモデルの中で第1位を確保しました。 リリース(2025年7月から8月)の時点で、Goedel-Prover-V2 はすべてのオープンソース定理プローバーの中で最も高い総合的な性能を達成している。 また、制限されたテストタイムの計算予算の下で、パフォーマンスを公表したクローズドソースシステムを含む、最高のパフォーマンスモデルにもランク付けしている。 私たちのモデル、コード、データはhttps://github.com/Goedel-LM/Goedel-Prover-V2でリリースされます。

関連論文リスト

• URPO: A Unified Reward & Policy Optimization Framework for Large Language Models [10.511836918064724]
  本稿では,1つのモデルと1つのトレーニングフェーズにおいて,命令フォロー(プレイヤ)と報酬モデリング(参照)を統一する新しいフレームワークを提案する。 提案手法は,全てのアライメントデータを含む選好ペア,検証可能な推論,オープンな命令を統一された生成形式に再キャストする。 Qwen2.5-7Bモデルの実験はURPOの優位性を示している。
  論文  参考訳（メタデータ） (2025-07-23T13:52:27Z)
• Skywork Open Reasoner 1 Technical Report [51.403686909760914]
  提案するSkywork-OR1は,長期チェーン・オブ・ソート(CoT)モデルのための,効果的かつスケーラブルな強化学習(RL)実装である。 DeepSeek-R1-Distillモデルシリーズをベースとして、我々のRLアプローチは顕著なパフォーマンス向上を実現している。 我々のSkywork-OR1-32Bモデルは、AIME24とAIME25ベンチマークでDeepSeek-R1とQwen3-32Bを上回っています。
  論文  参考訳（メタデータ） (2025-05-28T12:56:04Z)
• DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition [24.50773495427783]
  我々はDeepSeek-Prover-V2を紹介します。 このモデルは、ニューラル定理の証明における最先端のパフォーマンスを達成し、ミニF2Fテストで88.9%のパス比に達し、PutnamBenchの658問題のうち49を解決した。 標準ベンチマークに加えて、325の形式化された問題の集合であるProverBenchを導入し、最近のAIMEコンペティションから選択された15の問題を含む評価を強化した。
  論文  参考訳（メタデータ） (2025-04-30T16:57:48Z)
• S*: Test Time Scaling for Code Generation [55.11863577956177]
  コード生成のための最初のハイブリッドテストタイムスケーリングフレームワークであるS*を提案する。 S*は生成されたコードのカバレッジと選択精度を大幅に改善する。
  論文  参考訳（メタデータ） (2025-02-20T09:18:53Z)
• 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)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• ReNO: Enhancing One-step Text-to-Image Models through Reward-based Noise Optimization [59.72782742378666]
  本稿では,Reward-based Noise Optimization (ReNO) を提案する。 20-50秒の計算予算の中で、ReNOによって強化されたワンステップモデルは、現在のすべてのオープンソーステキスト・トゥ・イメージ・モデルの性能を一貫して上回った。
  論文  参考訳（メタデータ） (2024-06-06T17:56:40Z)
• CodingTeachLLM: Empowering LLM's Coding Ability via AST Prior Knowledge [0.0]
  我々は,コーディング学習用に設計された大規模言語モデル(LLM)であるCodingTeachLLMを紹介する。 本モデルは,学習知識の構造的分解と漸進的指導によるアウトプットを実現する。 当社のモデルは,オープンソースモデルと比較して,コード能力の最先端性も達成している。
  論文  参考訳（メタデータ） (2024-03-13T05:38:39Z)

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

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