Seed-Prover 1.5: Dominio de la Demostración de Teoremas a Nivel Pregrado mediante el Aprendizaje por Experiencia
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
Resumen
Los modelos de lenguaje grande han logrado recientemente avances significativos en la generación de demostraciones matemáticas rigurosas. Por el contrario, utilizar LLMs para la demostración de teoremas en lenguajes formales (como Lean) sigue siendo un desafío y computacionalmente costoso, particularmente al abordar problemas de nivel universitario y superiores. En este trabajo, presentamos Seed-Prover 1.5, un modelo de demostración formal de teoremas entrenado mediante aprendizaje por refuerzo agéntico a gran escala, junto con un flujo de trabajo eficiente de escalado en tiempo de prueba (TTS). A través de extensas interacciones con Lean y otras herramientas, el modelo acumula experiencia continuamente durante el proceso de RL, mejorando sustancialmente la capacidad y eficiencia de la demostración formal de teoremas. Además, aprovechando los avances recientes en demostración en lenguaje natural, nuestro flujo de trabajo TTS cierra eficientemente la brecha entre los lenguajes natural y formal. En comparación con los métodos de vanguardia, Seed-Prover 1.5 logra un rendimiento superior con un presupuesto computacional más pequeño. Resuelve el 88% de PutnamBench (nivel universitario), el 80% de Fate-H (nivel de posgrado) y el 33% de Fate-X (nivel de doctorado). Notablemente, utilizando nuestro sistema, resolvimos 11 de los 12 problemas del Putnam 2025 en menos de 9 horas. Nuestros hallazgos sugieren que escalar el aprendizaje a partir de la experiencia, impulsado por retroalimentación formal de alta calidad, tiene un inmenso potencial para el futuro del razonamiento 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.