論文の概要: QED-Nano: Teaching a Tiny Model to Prove Hard Theorems

• arxiv url: http://arxiv.org/abs/2604.04898v1
• Date: Mon, 06 Apr 2026 17:44:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-07 15:49:19.318215
• Title: QED-Nano: Teaching a Tiny Model to Prove Hard Theorems
• Title（参考訳）: QED-Nano: 厳密な理論を証明するためのTiny Modelを教える
• Authors: LM-Provers, Yuxiao Qu, Amrith Setlur, Jasper Dekoninck, Edward Beeching, Jia Li, Ian Wu, Lewis Tunstall, Aviral Kumar,
• Abstract要約: 我々は,オリンピアードレベルの証明のための4BモデルであるQED-Nanoを構築した。 QED-NanoとQED-Nano-SFTモデル、FineProofs-SFTとFineProofs-RLデータセット、トレーニングおよび評価コードを含む、完全なQED-Nanoパイプラインをリリースする。
• 参考スコア（独自算出の注目度）: 34.119608370222245
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Proprietary AI systems have recently demonstrated impressive capabilities on complex proof-based problems, with gold-level performance reported at the 2025 International Mathematical Olympiad (IMO). However, the training pipelines behind these systems remain largely undisclosed, and their reliance on large "internal" models and scaffolds makes them expensive to run, difficult to reproduce, and hard to study or improve upon. This raises a central question: can small, open models also be trained to achieve competitive reasoning performance on difficult Olympiad-level math? In this paper, we answer this question by building QED-Nano, a 4B model post-trained for Olympiad-level proofs. Our training recipe has three stages: (1) supervised fine-tuning to imbue good proof-writing styles by distilling from DeepSeek-Math-V2, (2) reinforcement learning (RL) with rubric-based rewards, and (3) expanding RL with a reasoning cache, which decomposes long proofs into iterative summarize-and-refine cycles and enables stronger test-time reasoning. QED-Nano surpasses the proof-generation performance of much larger open models, including Nomos-1 and GPT-OSS-120B, and approaches the performance of proprietary models like Gemini 3 Pro, at a fraction of the inference cost. To support further research on open mathematical reasoning, we release the full QED-Nano pipeline, including the QED-Nano and QED-Nano-SFT models, the FineProofs-SFT and FineProofs-RL datasets, and the training and evaluation code.
• Abstract（参考訳）: プロプライエタリなAIシステムは、2025年の国際数学オリンピック(IMO)で報告された、複雑な証明に基づく問題に対する印象的な能力を最近示した。 しかし、これらのシステムの背後にある訓練パイプラインはほとんど開示されておらず、大きな「内部」モデルや足場に依存しているため、実行が難しく、再現が難しく、研究や改善が難しい。 コンパクトでオープンなモデルは、難しいオリンピアードレベルの数学において、競争力のある推論性能を達成するために訓練できるのか? 本稿では,オリンピアードレベルの証明のための4BモデルであるQED-Nanoを構築することで,この問題に答える。 トレーニングレシピは,(1)DeepSeek-Math-V2から蒸留して良質な証明書字スタイルを指導し,(2)強化学習(RL)と,(3)長い証明を反復的な要約と再定義のサイクルに分解し,より強力なテスト時間推論を可能にする推論キャッシュを備えたRLの3段階からなる。 QED-Nano は Nomos-1 や GPT-OSS-120B など、はるかに大きなオープンモデルの実証世代性能を上回り、ジェミニ3 Pro のようなプロプライエタリなモデルの性能を推論コストのごく一部で実現している。 オープンな数学的推論のさらなる研究を支援するため、QED-NanoとQED-Nano-SFTモデル、FinProofs-SFTとFinProofs-RLデータセット、トレーニングおよび評価コードを含む完全なQED-Nanoパイプラインをリリースする。

関連論文リスト

• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
  本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。 IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。 シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
  論文  参考訳（メタデータ） (2025-07-31T17:00:30Z)
• 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)
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving [33.61458249318183]
  セルフプレイ・セオレム・プロバー(STP)は、予想と証明という2つの役割を担っている。 STPは同時に、予想と証明という2つの役割を担っている。 私たちはLeanとIsabelleの2つの形式的検証ツールで評価します。
  論文  参考訳（メタデータ） (2025-01-31T23:01:48Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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