Seed-Prover 1.5：通过经验学习掌握 undergraduate 级别的定理证明
计算与语言
2025-12-22 v1
摘要
大型语言模型最近在生成严谨的数学证明方面取得了显著进展。相比之下，在形式语言（如 Lean）中利用 LLM 进行定理证明仍具有挑战性且计算成本高昂，尤其是当针对大学生水平及更高层次的问题时。在本工作中，我们提出了 \textbf{Seed-Prover 1.5}，这是通过大规模智能体强化学习训练的形式定理证明模型，伴随一种高效的测试时扩展（TTS）工作流程。通过与 Lean 和其他工具的广泛交互，模型在 RL 过程中持续积累经验，显著增强了形式定理证明的能力和效率。此外，利用最近在自然语言证明方面的进展，我们的 TTS 工作流程高效地桥接了自然语言与形式语言之间的差距。与最先进的方法相比，Seed-Prover 1.5 在更小的计算预算下实现了卓越的性能。它解决了 \textbf{PutnamBench}（大学生水平）的 \textbf{88\%}、\textbf{Fate-H}（研究生水平）的 \textbf{80\%}，以及 \textbf{Fate-X}（博士水平）的 \textbf{33\%}问题。值得注意的是，我们的系统在 \textbf{9 小时内}解决了 \textbf{2025 年 Putnam 考试}的 \textbf{11 个问题}。我们的发现表明，扩大来自经验的学习，由高质量形式反馈驱动，对于形式数学推理的未来拥有巨大的潜力。
关键词
引用
@article{arxiv.2512.17260,
title = {Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience},
author = {Jiangjie Chen and Wenxiang Chen and Jiacheng Du and Jinyi Hu and Zhicheng Jiang and Allan Jie and Xiaoran Jin and Xing Jin and Chenggang Li and Wenlei Shi and Zhihong Wang and Mingxuan Wang and Chenrui Wei and Shufa Wei and Huajian Xin and Fan Yang and Weihao Gao and Zheng Yuan and Tianyang Zhan and Zeyu Zheng and Tianxi Zhou and Thomas Hanwen Zhu},
journal= {arXiv preprint arXiv:2512.17260},
year = {2025}
}
备注
21 pages