Seed-Prover 1.5: Dominando a Demonstração de Teoremas em Nível de Graduação por meio da Aprendizagem por Experiência
Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
December 19, 2025
Autores: 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
Resumo
Os modelos de linguagem de grande escala (LLMs) recentemente alcançaram progressos significativos na geração de provas matemáticas rigorosas. Em contraste, a utilização de LLMs para demonstração de teoremas em linguagens formais (como Lean) permanece desafiadora e computacionalmente dispendiosa, particularmente ao abordar problemas de nível universitário e além. Neste trabalho, apresentamos o Seed-Prover 1.5, um modelo de demonstração de teoremas formais treinado via aprendizado por reforço agentivo em larga escala, juntamente com um fluxo de trabalho eficiente de escalonamento em tempo de teste (TTS). Através de interações extensivas com Lean e outras ferramentas, o modelo acumula experiência continuamente durante o processo de RL, aprimorando substancialmente a capacidade e eficiência da demonstração formal de teoremas. Adicionalmente, aproveitando os avanços recentes na prova em linguagem natural, nosso fluxo de trabalho TTS preenche eficientemente a lacuna entre linguagens naturais e formais. Comparado aos métodos state-of-the-art, o Seed-Prover 1.5 alcança desempenho superior com um orçamento computacional menor. Ele resolve 88% do PutnamBench (nível universitário), 80% do Fate-H (nível de pós-graduação) e 33% do Fate-X (nível de doutorado). Notavelmente, usando nosso sistema, resolvemos 11 dos 12 problemas do Putnam 2025 em 9 horas. Nossos achados sugerem que escalonar o aprendizado a partir da experiência, impulsionado por feedback formal de alta qualidade, detém imenso potencial para o futuro do raciocínio matemático formal.
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.