論文の概要: 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を教える
• 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パイプラインをリリースする。

関連論文リスト

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Achieving Gold-Medal-Level Olympiad Reasoning via Simple and Unified Scaling [108.48818215929494]
  訓練後,背骨を厳密なオリンピックレベル解法に変換するためのシンプルで統一的なレシピを紹介した。 約340Kのサブ8K軌道上でSFTで30B-A3Bのバックボーンをトレーニングし,200RLステップを行った。 結果として得られるモデル SU-01 は、100Kトークンを超える軌道上の難しい問題に対する安定な推論をサポートする。
  論文  参考訳（メタデータ） (2026-05-13T10:13:26Z)
• Answer First, Reason Later: Aligning Search Relevance via Mode-Balanced Reinforcement Learning [7.006180736433431]
  低レイテンシと高パフォーマンスを実現する検索関連モデルを構築することは、検索業界において長年の課題である。 我々は,新しいtextbfAnswer-First, Reason Later(AFRL)パラダイムを提案する。 このパラダイムでは、モデルが第1のトークンで決定的な関連性スコアを出力し、続いて構造化された論理的説明を行う必要がある。
  論文  参考訳（メタデータ） (2026-02-10T17:28:12Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• Knowledge Graphs are Implicit Reward Models: Path-Derived Signals Enable Compositional Reasoning [4.464939140209426]
  本稿では,モデルが公理的領域の事実に根ざしたボトムアップ学習パラダイムを提案する。 知識グラフパスから新たな報酬信号を導き出すことで、検証可能でスケーラブルで、根底からの監視を提供する。 実験の結果、経路由来の報酬は「複合橋」として機能し、我々のモデルがより大きなモデルを大幅に上回ることを示した。
  論文  参考訳（メタデータ） (2026-01-21T16:38:59Z)
• ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations [14.748476989228214]
  Proofrは、人間の監督を必要とせず、リーンの証明を単純化するために訓練された最初の言語モデルです。 Provrは専門家の反復と強化学習を通じてトレーニングされ、リーンを使って単純化の検証とトレーニング信号を提供する。 Provrは、最先端のRL訓練プローバーが標準ベンチマークで生成した証明を実質的に圧縮する。
  論文  参考訳（メタデータ） (2025-10-17T14:45:30Z)
• 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)

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

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