QED-Nano：教导一个小型模型证明困难定理
人工智能
2026-04-07 v1 计算与语言
机器学习
摘要
专有 AI 系统最近在复杂证明类问题上展现出惊人的能力，在 2025 年国际数学奥林匹克（IMO）中取得了金牌水平。然而，这些系统背后的训练管道大多保持保密，它们依赖大型“内部”模型和脚手架，运行成本高昂、难以复现且难以研究和改进。这引出了一个核心问题：小型开源模型能否在困难的数学竞赛水平问题上实现具竞争力的推理性能？本文通过构建 QED-Nano，一个 4B 参数模型后训练用于奥林匹克级证明，回答了这一问题。我们的训练配方包含三个阶段：（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 数据集，以及训练和评估代码。
引用
@article{arxiv.2604.04898,
title = {QED-Nano: Teaching a Tiny Model to Prove Hard Theorems},
author = {LM-Provers and Yuxiao Qu and Amrith Setlur and Jasper Dekoninck and Edward Beeching and Jia Li and Ian Wu and Lewis Tunstall and Aviral Kumar},
journal= {arXiv preprint arXiv:2604.04898},
year = {2026}
}