Seed-Prover 1.5: Освоение доказательства теорем на уровне бакалавриата через обучение на основе опыта
Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
December 19, 2025
Авторы: Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, Zhihong Wang, Mingxuan Wang, Chenrui Wei, Shufa Wei, Huajian Xin, Fan Yang, Weihao Gao, Zheng Yuan, Tianyang Zhan, Zeyu Zheng, Tianxi Zhou, Thomas Hanwen Zhu
cs.AI
Аннотация
В последнее время крупные языковые модели достигли значительного прогресса в генерации строгих математических доказательств. В то же время использование LLM для доказательства теорем на формальных языках (таких как Lean) остаётся сложной и вычислительно затратной задачей, особенно при решении проблем уровня бакалавриата и выше. В данной работе мы представляем Seed-Prover 1.5 — модель для формального доказательства теорем, обученную с помощью масштабируемого агентного обучения с подкреплением, а также эффективный workflow масштабирования на этапе тестирования (TTS). Благодаря интенсивному взаимодействию с Lean и другими инструментами модель непрерывно накапливает опыт в процессе RL, существенно повышая возможности и эффективность формального доказательства теорем. Кроме того, используя последние достижения в области доказательств на естественном языке, наш TTS-workflow эффективно преодолевает разрыв между естественными и формальными языками. По сравнению с передовыми методами Seed-Prover 1.5 демонстрирует превосходящую производительность при меньших вычислительных затратах. Модель решает 88% задач PutnamBench (уровень бакалавриата), 80% задач Fate-H (уровень магистратуры) и 33% задач Fate-X (уровень PhD). Примечательно, что с помощью нашей системы мы решили 11 из 12 задач Putnam 2025 за 9 часов. Наши результаты свидетельствуют, что масштабирование обучения на основе опыта, подкреплённое качественной формальной обратной связью, обладает огромным потенциалом для будущего формального математического мышления.
English
Large language models have recently made significant progress to generate rigorous mathematical proofs. In contrast, utilizing LLMs for theorem proving in formal languages (such as Lean) remains challenging and computationally expensive, particularly when addressing problems at the undergraduate level and beyond. In this work, we present Seed-Prover 1.5, a formal theorem-proving model trained via large-scale agentic reinforcement learning, alongside an efficient test-time scaling (TTS) workflow. Through extensive interactions with Lean and other tools, the model continuously accumulates experience during the RL process, substantially enhancing the capability and efficiency of formal theorem proving. Furthermore, leveraging recent advancements in natural language proving, our TTS workflow efficiently bridges the gap between natural and formal languages. Compared to state-of-the-art methods, Seed-Prover 1.5 achieves superior performance with a smaller compute budget. It solves 88\% of PutnamBench (undergraduate-level), 80\% of Fate-H (graduate-level), and 33\% of Fate-X (PhD-level) problems. Notably, using our system, we solved 11 out of 12 problems from Putnam 2025 within 9 hours. Our findings suggest that scaling learning from experience, driven by high-quality formal feedback, holds immense potential for the future of formal mathematical reasoning.