QED-Nano：教微型模型证明难定理

专有AI系统近期在复杂的基于证明的问题上展现出令人印象深刻的能力，据报道已在2025年国际数学奥林匹克（IMO）上达到金牌水平。然而，这些系统背后的训练流水线在很大程度上仍未公开，其对大型“内部”模型与脚手架的依赖使其运行成本高昂、难以复现，也难以研究和改进。这引出一个核心问题：小型开放模型能否也被训练出在困难的奥赛级数学上具有竞争力的推理性能？本文通过构建QED-Nano——一个为奥赛级证明进行后训练的4B模型——来回答这一问题。我们的训练配方分三个阶段：（1）通过从DeepSeek-Math-V2蒸馏进行监督微调，以注入良好的证明写作风格；（2）使用基于量规（rubric）奖励的强化学习（RL）；（3）用推理缓存扩展RL，将长证明分解为迭代式的总结-精炼循环，从而实现更强的测试时推理。QED-Nano在证明生成上超越大得多的开放模型，包括Nomos-1与GPT-OSS-120B，并接近Gemini 3 Pro等专有模型的性能，而推理成本仅为后者的一小部分。为支持开放数学推理的进一步研究，我们发布了完整的QED-Nano流水线，包括QED-Nano与QED-Nano-SFT模型、FineProofs-SFT与FineProofs-RL数据集，以及训练与评估代码。