論文の概要: 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データ合成と自己補正による形式理論のスケーリング
• 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でリリースされます。

関連論文リスト

• Explorative Modeling: Unlocking a Third Pretraining Axis and End-to-End Generation [89.51408170909548]
  トレーニングループを規定する新しいパラダイムであるExplorative Modelingを導入し、モデル世代とデータ間のK候補マッチングを探索し、最高のトレーニングを行う。 まず、探索の増加は、既存の生成モデルのためのパラメータとデータを超えた第3の事前学習軸を追加する。 第2に、XMは16-256倍の推論ステップで制御タスク上の拡散と一致する、エンドツーエンドの再構成生成モデリングを可能にする。
  論文  参考訳（メタデータ） (2026-07-29T18:25:17Z)
• Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation [27.324913853284404]
  Pythagoras-Prover(ピタゴラス・プロバー)は、実用的な計算予算のために開発された、リーンの定理プローバーの計算効率のよいファミリーである。 学習効率を向上させるために、カリキュラムSFTの簡単で中堅な問題に階層化されたリーン検証コーパスを構築します。 Augmented Lean Formalisation (ALF)も導入しています。
  論文  参考訳（メタデータ） (2026-06-10T18:43:11Z)
• Solve the Loop: Attractor Models for Language and Reasoning [4.8720589853137435]
  Looped Transformerは、純粋にフィードフォワード計算に代わる有望な代替手段を提供する。 本稿では、まず、バックボーンモジュールが出力の埋め込みを提案し、次にアトラクターモジュールが固定点を解くことでそれらを洗練するAttractor Modelsを紹介する。 本研究では,Attractor Modelsが,大規模言語モデル事前学習と推論という2つのレシエーションにおいて,既存モデルよりも優れていることを示す。
  論文  参考訳（メタデータ） (2026-05-12T17:51:26Z)
• Three Roles, One Model: Role Orchestration at Inference Time to Close the Performance Gap Between Small and Large Agents [0.4666493857924357]
  複雑なマルチステップ環境において,推論時足場のみに追加のトレーニング計算を使わずに,小さなモデルの性能を向上させることができるかどうかを検討した。 我々は,AppWorldベンチマークのQwen3-8Bを,完全精度と4ビット量子化構成の両方で評価した。 本格的な推測では、私たちの足場付き8Bモデルは、オリジナルのAppWorld評価からDeepSeek-Coder 33Bインストラクション(7.1%)を上回っています。
  論文  参考訳（メタデータ） (2026-04-13T13:40:33Z)
• Efficient Multi-Model Orchestration for Self-Hosted Large Language Models [2.3275796286410677]
  Pick and Spinは、セルフホストのオーケストレーションと経済性を実現するフレームワークである。 統合されたHelmベースのデプロイメントシステム、適応型スケールツーゼロ自動化、ハイブリッドルーティングモジュールを統合している。 最大21.6%の成功率、30%のレイテンシ、クエリ毎のコストの33%削減を実現している。
  論文  参考訳（メタデータ） (2025-12-26T22:42:40Z)
• URPO: A Unified Reward & Policy Optimization Framework for Large Language Models [10.511836918064724]
  本稿では,1つのモデルと1つのトレーニングフェーズにおいて,命令フォロー(プレイヤ)と報酬モデリング(参照)を統一する新しいフレームワークを提案する。 提案手法は,全てのアライメントデータを含む選好ペア,検証可能な推論,オープンな命令を統一された生成形式に再キャストする。 Qwen2.5-7Bモデルの実験はURPOの優位性を示している。
  論文  参考訳（メタデータ） (2025-07-23T13:52:27Z)
• Navigating the Accuracy-Size Trade-Off with Flexible Model Merging [15.497612580389479]
  我々は、新しいデータフリーモデルマージフレームワークFlexMergeを提案する。 異なる大きさのマージモデルを柔軟に生成し、単一のマージモデルから完全なスペクトルにまたがり、すべての微調整モデルを保持する。 FlexMergeを使って、異なるアルゴリズムの精度と大きさのトレードオフを体系的に特徴づける。
  論文  参考訳（メタデータ） (2025-05-29T07:50:32Z)
• 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)

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

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