Seed-Prover 1.5: Meester worden in het bewijzen van undergraduate-stellingen door leren uit ervaring

Samenvatting

Grote taalmodellen hebben recentelijk aanzienlijke vooruitgang geboekt in het genereren van rigoureuze wiskundige bewijzen. Het gebruik van LLM's voor stellingenbewijzen in formele talen (zoals Lean) blijft daarentegen uitdagend en rekenkundig kostbaar, vooral bij problemen op bachelorniveau en daarboven. In dit werk presenteren we Seed-Prover 1.5, een formeel stellingenbewijsmodel getraind via grootschalig agent-gebaseerd reinforcement learning, samen met een efficiënte workflow voor schaling tijdens testtijd (TTS). Door uitgebreide interacties met Lean en andere tools accumuleert het model continu ervaring tijdens het RL-proces, wat de capaciteit en efficiëntie van formeel stellingenbewijzen aanzienlijk verbetert. Bovendien overbrugt onze TTS-workflow, door gebruik te maken van recente ontwikkelingen in natuurlijktaal-bewijzen, efficiënt de kloof tussen natuurlijke en formele talen. Vergeleken met state-of-the-art methoden behaalt Seed-Prover 1.5 superieure prestaties met een kleiner rekenbudget. Het lost 88% van de PutnamBench-problemen (bachelorniveau), 80% van Fate-H (masterniveau) en 33% van Fate-X (promotieniveau) op. Opmerkelijk is dat we met ons systeem 11 van de 12 problemen van Putnam 2025 binnen 9 uur hebben opgelost. Onze bevindingen suggereren dat het opschalen van leren uit ervaring, aangedreven door hoogwaardige formele feedback, een enorm potentieel heeft voor de toekomst van formeel wiskundig redeneren.

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.

Seed-Prover 1.5: Meester worden in het bewijzen van undergraduate-stellingen door leren uit ervaring

Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience

Samenvatting

Support