Seed-Prover: Raciocínio Profundo e Amplo para Prova 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

Resumo

Os LLMs demonstraram fortes habilidades de raciocínio matemático ao aproveitar o aprendizado por reforço com cadeias longas de pensamento, mas continuam a enfrentar dificuldades na prova de teoremas devido à falta de sinais claros de supervisão quando utilizam apenas linguagem natural. Linguagens específicas de domínio, como Lean, fornecem supervisão clara por meio da verificação formal de provas, permitindo um treinamento eficaz através do aprendizado por reforço. Neste trabalho, propomos o Seed-Prover, um modelo de raciocínio de prova completa no estilo de lemas. O Seed-Prover pode refinar iterativamente sua prova com base no feedback do Lean, nos lemas provados e na auto-summarização. Para resolver problemas de nível de competição da IMO, projetamos três estratégias de inferência em tempo de teste que permitem raciocínios profundos e amplos. O Seed-Prover prova 78,1% dos problemas formalizados de edições anteriores da IMO, satura o MiniF2F e alcança mais de 50% no PutnamBench, superando o estado da arte anterior por uma grande margem. Para lidar com a falta de suporte a geometria no Lean, introduzimos um mecanismo de raciocínio geométrico, o Seed-Geometry, que supera os motores formais de geometria anteriores. Utilizamos esses dois sistemas para participar da IMO 2025 e provar completamente 5 dos 6 problemas. Este trabalho representa um avanço significativo no raciocínio matemático automatizado, demonstrando a eficácia da verificação formal com raciocínio de cadeias longas de pensamento.

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.