Seed-Prover: Ragionamento Profondo e Ampio per il Teorema Automatico

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

July 31, 2025

Autori: 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

Abstract

I LLM hanno dimostrato forti capacità di ragionamento matematico sfruttando il reinforcement learning con lunghe catene di pensiero, ma continuano a incontrare difficoltà nella dimostrazione di teoremi a causa della mancanza di segnali di supervisione chiari quando si utilizza esclusivamente il linguaggio naturale. Linguaggi specifici di dominio come Lean forniscono una supervisione chiara attraverso la verifica formale delle dimostrazioni, consentendo un addestramento efficace tramite reinforcement learning. In questo lavoro, proponiamo Seed-Prover, un modello di ragionamento a dimostrazione completa in stile lemma. Seed-Prover può affinare iterativamente la sua dimostrazione basandosi sul feedback di Lean, sui lemmi dimostrati e sull'auto-riassunto. Per risolvere problemi di livello IMO, progettiamo tre strategie di inferenza al momento del test che consentono sia un ragionamento profondo che ampio. Seed-Prover dimostra il 78,1% dei problemi IMO formalizzati del passato, satura MiniF2F e raggiunge oltre il 50% su PutnamBench, superando di gran lunga lo stato dell'arte precedente. Per affrontare la mancanza di supporto per la geometria in Lean, introduciamo un motore di ragionamento geometrico, Seed-Geometry, che supera i precedenti motori formali di geometria. Utilizziamo questi due sistemi per partecipare all'IMO 2025 e dimostrare completamente 5 su 6 problemi. Questo lavoro rappresenta un significativo avanzamento nel ragionamento matematico automatizzato, dimostrando l'efficacia della verifica formale con ragionamento a lunga catena di pensiero.

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.