論文の概要: MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling

• arxiv url: http://arxiv.org/abs/2606.13473v1
• Date: Thu, 11 Jun 2026 15:27:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-12 15:55:27.884343
• Title: MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling
• Title（参考訳）: MaxProof:generative-Verifier RLと Population-Level Test-Time Scalingによる数学的証明のスケーリング
• Authors: Jiacheng Chen, Xinyu Zhang, Shunkai Zhang, Yanmohan Wang, Lin Li, Tiancheng Qin, Qin Wang, Zhengmao Zhu, Tianle Li, Jingyang Li, Zehan Li, Binyang Jiang, Jin Zhu, Han Ding, Fei Yu, Chenyu Du, Zijian Song, Jiayuan Song, Zhi Zhang, Yunan Huang, Weiyu Cheng, Pengyu Zhao, Yu Cheng,
• Abstract要約: MaxProofは、競合レベルの数学的証明のための集団レベルのテストタイムスケーリングフレームワークである。 M3はまず、証明生成、証明検証、批判条件付き証明修復という、3つの証明指向の能力を訓練する。 テスト時には、MaxProofはモデルをジェネレータ、検証器、精細化器、ランク付け器として扱い、候補証明の集団を探索し、トーナメント選択を通じて最後の1つの証明を返す。
• 参考スコア（独自算出の注目度）: 34.353891209243464
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: We present MaxProof, a population-level test-time scaling framework for competition-level mathematical proof in the MiniMax-M3 series. M3 first trains three proof-oriented capabilities -- proof generation, proof verification, and critique-conditioned proof repair -- using a defense-in-depth generative verifier engineered for low false-positive rate. These capabilities are merged into a single released M3 model. At test time, MaxProof treats the model as a generator, verifier, refiner, and ranker, searches over a population of candidate proofs, and returns one final proof through tournament selection. With MaxProof test-time scaling, the M3 model reaches 35/42 on IMO 2025 and 36/42 on USAMO 2026, exceeding the human gold-medal threshold on both.
• Abstract（参考訳）: 我々は、MiniMax-M3シリーズにおける競合レベルの数学的証明のための集団レベルのテスト時間スケーリングフレームワークであるMaxProofを紹介する。 M3はまず、3つの証明指向能力(証明生成、証明検証、批判条件付き証明修復)を、偽陽性率の低いディフェンス・イン・ディープス・ジェネレーティブ・検証を使って訓練する。 これらの機能は単一のM3モデルにマージされる。 テスト時には、MaxProofはモデルをジェネレータ、検証器、精細化器、ランク付け器として扱い、候補証明の集団を探索し、トーナメント選択を通じて最後の1つの証明を返す。 MaxProofのテストタイムスケーリングでは、M3モデルはIMO 2025で35/42、USAMO 2026で36/42に達し、どちらも人間のゴールドメディカル閾値を上回っている。

関連論文リスト

• Do We Need Frontier Models to Verify Mathematical Proofs? [14.254472131009654]
  より小さなオープンソースモデルは、精度でフロンティアモデルに最大10%遅れていることが示されています。 そして、より小さなモデルが、実際にフロンティアモデルのレベルで証明を検証する数学的能力を持っていることを実証する。 我々は、小型モデルの特定の障害モードを克服し、その性能を9.1%の精度で15.9%の自己整合性で向上する特殊プロンプトのアンサンブルを合成する。
  論文  参考訳（メタデータ） (2026-04-02T18:31:44Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction [95.91743732150233]
  一連のオープンソースの言語モデルであるGoedel-Prover-V2は、自動定理の新たな最先端を証明した。 我々は、より複雑な定理をマスターするためにモデルを訓練することの困難さを増す合成タスクを生成する。 Goedel-Prover-V2-32Bは、標準モードのpass@32でMiniF2Fの88.1%、自己補正モードの90.4%を達成する。
  論文  参考訳（メタデータ） (2025-08-05T16:28:22Z)
• The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs [7.20909461915203]
  提案するOpen Proof Corpus(OPC, Open Proof Corpus)は, 最先端のLLMによって生成される5000以上の人的評価された証明からなるデータセットである。 OPCは、証明生成研究における幅広い適用性と下流利用のために特別に設計された。 本研究では,(1)自然言語と形式的証明生成のパフォーマンスギャップ,(2)最終回答精度と完全正当性との相違,(3)証明品質に対する最良選択の影響について考察する。
  論文  参考訳（メタデータ） (2025-06-23T13:31:58Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• Sample, Don't Search: Rethinking Test-Time Alignment for Language Models [55.2480439325792]
  新しいテストタイムアライメントアプローチであるQAlignを紹介します。 テスト時間計算をスケールする際、QAlignは各プロンプトの最適配向分布からのサンプリングに収束する。 マルコフ連鎖モンテカルロのテキスト生成における最近の進歩を取り入れることで、基礎となるモデルを変更したり、ロジットアクセスを必要とせずに、より良い整合出力を可能にする。
  論文  参考訳（メタデータ） (2025-04-04T00:41:40Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• When Liebig's Barrel Meets Facial Landmark Detection: A Practical Model [87.25037167380522]
  正確で、堅牢で、効率的で、一般化可能で、エンドツーエンドのトレーニングが可能なモデルを提案する。 精度を向上させるために,2つの軽量モジュールを提案する。 DQInitは、インプットからデコーダのクエリを動的に初期化し、複数のデコーダ層を持つものと同じ精度でモデルを実現する。 QAMemは、共有するクエリではなく、それぞれのクエリに別々のメモリ値を割り当てることで、低解像度のフィーチャーマップ上のクエリの識別能力を高めるように設計されている。
  論文  参考訳（メタデータ） (2021-05-27T13:51:42Z)

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

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