Seed-Prover 1.5: Beherrschung des Beweisens von mathematischen Sätzen auf Bachelor-Niveau durch Lernen aus Erfahrung

papers.abstract

Große Sprachmodelle haben kürzlich bedeutende Fortschritte bei der Generierung rigoroser mathematischer Beweise erzielt. Im Gegensatz dazu bleibt der Einsatz von LLMs für Theorembeweise in formalen Sprachen (wie Lean) herausfordernd und rechenintensiv, insbesondere bei Problemen auf Undergraduate-Niveau und darüber hinaus. In dieser Arbeit stellen wir Seed-Prover 1.5 vor, ein formales Theorembeweis-Modell, das durch groß angelegtes agentenbasiertes Verstärkungslernen trainiert wurde, zusammen mit einem effizienten Test-Time-Scaling (TTS)-Workflow. Durch umfangreiche Interaktionen mit Lean und anderen Werkzeugen sammelt das Modell während des RL-Prozesses kontinuierlich Erfahrungen, was die Fähigkeiten und die Effizienz des formalen Theorembeweisens erheblich steigert. Darüber hinaus überbrückt unser TTS-Workflow durch die Nutzung jüngster Fortschritte beim natürlichem Sprachbeweis effizient die Lücke zwischen natürlichen und formalen Sprachen. Im Vergleich zu state-of-the-art-Methoden erzielt Seed-Prover 1.5 eine überlegene Leistung mit einem geringeren Rechenbudget. Es löst 88 % der PutnamBench- (Undergraduate-Niveau), 80 % der Fate-H- (Graduate-Niveau) und 33 % der Fate-X- (PhD-Niveau) Probleme. Bemerkenswerterweise lösten wir mit unserem System 11 von 12 Problemen des Putnam-Wettbewerbs 2025 innerhalb von 9 Stunden. Unsere Ergebnisse deuten darauf hin, dass die Skalierung des Lernens aus Erfahrung, getrieben durch hochwertiges formales Feedback, immenses Potenzial für die Zukunft des formalen mathematischen Denkens birgt.

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: Beherrschung des Beweisens von mathematischen Sätzen auf Bachelor-Niveau durch Lernen aus Erfahrung

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

papers.abstract

Support