Seed-Prover: Razonamiento Profundo y Amplio para la Demostración Automática de Teoremas

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

July 31, 2025

Autores: Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, Thomas Hanwen Zhu

cs.AI

Resumen

Los LLM han demostrado una fuerte capacidad de razonamiento matemático al aprovechar el aprendizaje por refuerzo con cadenas de pensamiento largas, pero continúan enfrentando dificultades en la demostración de teoremas debido a la falta de señales de supervisión claras cuando se utiliza únicamente lenguaje natural. Lenguajes específicos de dominio como Lean proporcionan una supervisión clara mediante la verificación formal de pruebas, lo que permite un entrenamiento efectivo a través del aprendizaje por refuerzo. En este trabajo, proponemos Seed-Prover, un modelo de razonamiento de pruebas completas en estilo lema. Seed-Prover puede refinar iterativamente su demostración basándose en la retroalimentación de Lean, lemas probados y auto-resúmenes. Para resolver problemas de nivel de la Olimpiada Internacional de Matemáticas (IMO), diseñamos tres estrategias de inferencia en tiempo de prueba que permiten un razonamiento tanto profundo como amplio. Seed-Prover demuestra el 78.1% de los problemas formalizados de IMO anteriores, satura MiniF2F y logra más del 50% en PutnamBench, superando ampliamente el estado del arte anterior. Para abordar la falta de soporte de geometría en Lean, introducimos un motor de razonamiento geométrico, Seed-Geometry, que supera a los motores formales de geometría anteriores. Utilizamos estos dos sistemas para participar en la IMO 2025 y demostrar completamente 5 de los 6 problemas. Este trabajo representa un avance significativo en el razonamiento matemático automatizado, demostrando la efectividad de la verificación formal con cadenas de pensamiento largas.

English

LLMs have demonstrated strong mathematical reasoning abilities by leveraging reinforcement learning with long chain-of-thought, yet they continue to struggle with theorem proving due to the lack of clear supervision signals when solely using natural language. Dedicated domain-specific languages like Lean provide clear supervision via formal verification of proofs, enabling effective training through reinforcement learning. In this work, we propose Seed-Prover, a lemma-style whole-proof reasoning model. Seed-Prover can iteratively refine its proof based on Lean feedback, proved lemmas, and self-summarization. To solve IMO-level contest problems, we design three test-time inference strategies that enable both deep and broad reasoning. Seed-Prover proves 78.1% of formalized past IMO problems, saturates MiniF2F, and achieves over 50\% on PutnamBench, outperforming the previous state-of-the-art by a large margin. To address the lack of geometry support in Lean, we introduce a geometry reasoning engine Seed-Geometry, which outperforms previous formal geometry engines. We use these two systems to participate in IMO 2025 and fully prove 5 out of 6 problems. This work represents a significant advancement in automated mathematical reasoning, demonstrating the effectiveness of formal verification with long chain-of-thought reasoning.