QED-Nano: Teaching a Tiny Model to Prove Hard Theorems

📄 arXiv: 2604.04898 📥 PDF

作者: LM-Provers, Yuxiao Qu, Amrith Setlur, Jasper Dekoninck, Edward Beeching, Jia Li, Ian Wu, Lewis Tunstall, Aviral Kumar

分类: cs.AI, cs.CL, cs.LG

发布日期: 2026-04-07

💡 一句话要点

QED-Nano：训练小型模型解决奥赛级难题，性能媲美大型闭源模型。

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱五：交互与反应 (Interaction & Reaction)

关键词: 数学推理 定理证明 强化学习 模型蒸馏 奥林匹克数学

📋 核心要点

  1. 现有数学解题AI依赖大型模型，训练流程不透明，复现和研究困难。
  2. QED-Nano通过蒸馏、强化学习和推理缓存，训练小型模型解决奥赛级难题。
  3. QED-Nano性能超越大型开源模型，接近闭源模型，且推理成本更低。

📝 摘要（中文）

本文介绍了QED-Nano，一个为解决奥林匹克级别证明题而进行后训练的40亿参数模型。现有AI系统在基于证明的复杂问题上表现出色，但其训练流程不公开，且依赖大型模型，导致运行成本高昂、难以复现和改进。QED-Nano通过三个阶段的训练解决此问题：(1) 通过从DeepSeek-Math-V2蒸馏，进行监督微调以学习良好的证明写作风格；(2) 使用基于评分标准的奖励进行强化学习(RL)；(3) 通过推理缓存扩展RL，将长证明分解为迭代的总结和改进循环，从而增强测试时的推理能力。QED-Nano超越了包括Nomos-1和GPT-OSS-120B在内的大型开源模型的证明生成性能，并以更低的推理成本接近Gemini 3 Pro等专有模型的性能。为了支持对开放数学推理的进一步研究，我们发布了完整的QED-Nano流程，包括QED-Nano和QED-Nano-SFT模型、FineProofs-SFT和FineProofs-RL数据集以及训练和评估代码。

🔬 方法详解

问题定义：现有AI系统在解决奥林匹克级别的数学证明题时，依赖于大型的、不开源的模型，这使得研究人员难以复现、分析和改进这些系统。此外，这些大型模型的推理成本也很高，限制了其应用范围。因此，如何训练小型、开源的模型，使其在奥赛级别的数学证明题上达到具有竞争力的性能，是一个重要的研究问题。

核心思路：QED-Nano的核心思路是通过一个三阶段的训练流程，将大型模型的知识迁移到小型模型上，并利用强化学习和推理缓存来提升模型的推理能力。具体来说，首先通过监督微调学习良好的证明写作风格，然后通过强化学习优化模型的证明策略，最后通过推理缓存来分解长证明，从而提高模型的推理效率和准确性。

技术框架：QED-Nano的训练流程包含三个主要阶段：(1) 监督微调(SFT)：使用DeepSeek-Math-V2生成的数据集，对模型进行微调，使其学习到良好的证明写作风格。(2) 强化学习(RL)：使用基于评分标准的奖励函数，对模型进行强化学习，使其能够生成正确的证明。(3) 扩展强化学习(RL with Reasoning Cache)：引入推理缓存机制，将长证明分解为迭代的总结和改进循环，从而增强模型的推理能力。

关键创新：QED-Nano的关键创新在于其三阶段的训练流程，特别是推理缓存机制的引入。推理缓存可以将长证明分解为更小的子问题，并利用强化学习来优化每个子问题的解决方案。这种方法可以有效地提高模型的推理效率和准确性，使其能够在奥赛级别的数学证明题上达到具有竞争力的性能。

关键设计：在监督微调阶段，使用了DeepSeek-Math-V2生成的数据集，并采用交叉熵损失函数进行训练。在强化学习阶段，使用了基于评分标准的奖励函数，并采用PPO算法进行训练。在扩展强化学习阶段，引入了推理缓存机制，并采用迭代的总结和改进循环来生成证明。具体的参数设置和网络结构细节未在摘要中详细说明，需要参考论文全文。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

QED-Nano在奥赛级别的数学证明题上取得了显著的性能提升，超越了Nomos-1和GPT-OSS-120B等大型开源模型，并接近Gemini 3 Pro等闭源模型的性能，同时推理成本更低。这表明，通过有效的训练策略，小型模型也可以在复杂推理任务上达到具有竞争力的性能。

🎯 应用场景

QED-Nano的研究成果可应用于自动化定理证明、数学教育、AI辅助科学发现等领域。通过训练小型模型解决复杂数学问题，降低了AI推理的成本，使得更多研究者和学生能够参与到数学研究中。未来，该技术有望扩展到其他需要复杂推理的领域，例如程序验证、法律推理等。

📄 摘要（原文）

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.