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.
翻译:专有AI系统近期在复杂证明类问题上展现出令人瞩目的能力,在2025年国际数学奥林匹克竞赛(IMO)中取得了金牌级表现。然而,这些系统背后的训练流程仍高度保密,其依赖大型"内部"模型与框架的做法导致运行成本高昂、复现困难,且难以开展深入研究与改进。这引发了一个核心问题:能否通过训练小型开源模型在极具挑战性的奥赛级数学问题上实现同等竞争力的推理能力?本文通过构建QED-Nano——一个专为奥赛级证明进行后训练的4B参数模型——对此问题给出了肯定答案。我们的训练方案包含三个阶段:(1)通过从DeepSeek-Math-V2进行知识蒸馏的有监督微调,赋予模型良好的证明写作风格;(2)基于评分标准的强化学习(RL);(3)引入带推理缓存的强化学习,将长证明分解为"总结-优化"迭代循环,从而增强测试时推理能力。QED-Nano在证明生成性能上超越了包括Nomos-1和GPT-OSS-120B在内的更大规模开源模型,且推理成本仅为专有模型(如Gemini 3 Pro)的零头。为支持开放数学推理领域的进一步研究,我们完整开源了QED-Nano训练流程,包含QED-Nano与QED-Nano-SFT模型、FineProofs-SFT与FineProofs-RL数据集,以及训练与评估代码。