ByteDance's Seed-Prover: SOTA bei automatisiertem Mathematikbeweis

Große Sprachmodelle (LLMs) haben erhebliche Fortschritte im mathematischen Denken gezeigt, oft indem sie ihre natürlichen Sprachfähigkeiten nutzen, um die Leistung bei Benchmarks wie MATH und AIME zu verbessern. Eine zentrale Herausforderung beim Training dieser Modelle mit Reinforcement Learning (RL) ist jedoch die Schwierigkeit, die Korrektheit von natürlichsprachigen Beweisen zu überprüfen, was typischerweise eine akribische manuelle Überprüfung jedes Schrittes erfordert. Diese Einschränkung behindert die breitere Anwendung von RL bei der Entwicklung mathematischer Theorembeweismodelle. Während formale Sprachen wie Lean eine automatische Korrektheitsprüfung ermöglichen, stoßen aktuelle LLM-basierte formale Beweiser immer noch auf Einschränkungen. Zum Beispiel generieren schrittweise Beweiser Code inkrementell, erfordern aber oft spezifische strukturelle Unterstützung und haben Schwierigkeiten mit hochrangigem Denken.

Als Reaktion darauf hat das Seed Team von ByteDance Seed-Prover eingeführt, ein neuartiges, lemmabasiertes Ganzbeweis-Argumentationsmodell. Seed-Prover verfeinert Beweise iterativ, indem es Feedback von Lean einbezieht, zuvor etablierte Lemmata nutzt und Selbstzusammenfassung anwendet. Es integriert drei spezialisierte Inferenzstrategien zur Testzeit, die tiefe und breite Denkfähigkeiten ermöglichen, um komplexe Probleme, einschließlich derer der Internationalen Mathematik-Olympiade (IMO), zu bewältigen. Seine Kerninnovation liegt in der Annahme eines lemmabasierten Beweisansatzes, der den Denkprozess um Lemmata herumzentriert, anstatt traditionelle Schritt-für-Schritt- oder monolithische Ganzbeweis-Generierungsmethoden zu verwenden. Ergänzend dazu wird auch Seed-Geometry eingeführt, eine spezialisierte Geometrie-Denkmaschine, die entwickelt wurde, um die Einschränkungen von Lean bei der Bearbeitung geometrischer Probleme zu überwinden.

Die Interaktion zwischen Seed-Prover und Lean wird durch ein mehrstufiges, multimodales Reinforcement-Learning-Framework auf Basis von VAPO ermöglicht. Der Trainingsdatensatz kombiniert öffentlich verfügbare Datensätze mit ByteDance-internen formalen Problemen. Eine „Proposer“-Komponente wird verwendet, um einfachere Variationen schwieriger Aufgaben zu generieren, während übermäßig einfache Probleme (mit Beweisraten über 25%) ausgeschlossen werden. Das Backend von Seed-Geometry unterstützt die groß angelegte Problemgenerierung und hat innerhalb von sieben Tagen über 230 Millionen einzigartige Probleme identifiziert, was eine achtfache Verbesserung der Sucheffizienz demonstriert. Obwohl separate Policy- und Wertmodelle trainiert werden, zeigten umfangreiche Tests, dass Wertmodelle aufgrund von Schätzfehlern manchmal die Leistung reduzieren könnten, was zur Einführung der schrittweisen Generierung mit Beam Search in verteilten Umgebungen führte.

Seed-Prover hat in mehreren mathematischen Benchmarks hochmoderne Ergebnisse erzielt. Bei der IMO 2025 löste Seed-Prover erfolgreich 5 von 6 Problemen; insbesondere löste Seed-Geometry sofort Problem 2, und Seed-Prover leitete Beweise für die verbleibenden Probleme unter Verwendung verschiedener Inferenz-Einstellungen ab. Bei früheren IMO-Problemen bewies es 121 von 155 Aufgaben und erreichte eine Erfolgsquote von 78,1% über alle Schwierigkeitsgrade hinweg. Diese Leistung umfasst das Lösen von 47 von 55 einfachen Problemen, 47 von 56 mittleren Problemen und 27 von 44 schweren Problemen. Auch die fachspezifischen Erfolgsquoten waren stark, mit 72 von 85 in Algebra, 42 von 55 in Zahlentheorie und 7 von 14 in Kombinatorik.

Auf dem MiniF2F-Benchmark berichteten Forscher eine Beweisrate von 99,6% für Validierungs- und Testsets unter mittleren Einstellungen, wobei sie erfolgreich herausfordernde Probleme wie IMO 1990 P3 lösten. Die PutnamBench-Ergebnisse zeigten eine signifikante Verbesserung von 201 auf 331 gelöste Probleme von 657 beim Upgrade von leichten auf mittlere Inferenz-Einstellungen, was einen bemerkenswerten Leistungssprung gegenüber früheren mathematischen Denksystemen auf Bachelor-Niveau darstellt. Während Seed-Prover 30 von 100 Kombinatorikproblemen auf CombiBench löste und damit bestehende Methoden übertraf, hoben die Ergebnisse auch die anhaltenden Herausforderungen im kombinatorischen Denken hervor. Darüber hinaus erreichte Seed-Prover eine Erfolgsquote von 81,8% auf MiniCTX-v2, was starke Generalisierungsfähigkeiten über wettbewerbsspezifische Probleme hinaus demonstriert und die Baseline von o4-mini von 44,3% bei Pass@8 übertrifft.

Zusammenfassend lässt sich sagen, dass ByteDance's Seed Team Seed-Geometry und Seed-Prover eingeführt hat, zwei formale Denkmethoden, die die Fähigkeiten von LLMs effektiv integrieren. Seed-Geometry bietet beschleunigte Verifikation und verbesserte Suchmechanismen für geometrische Probleme, während Seed-Prover iterative Verfeinerung und komplexe Testzeit-Inferenzstrategien für allgemeine mathematische Beweise nutzt. Die Leistung, 5 von 6 Problemen bei der IMO 2025 gelöst zu haben, unterstreicht die praktische Wirksamkeit dieser Methoden bei der Bewältigung mathematischer Elite-Wettbewerbe. Die Einführung formaler Sprachen wie Lean bietet eine schnelle Beweisverifikation, die sowohl kostengünstiger als menschliche Experten als auch zuverlässiger als LLM-basierte Richter ist. Zukünftige Forschung wird sich darauf konzentrieren, formale Systeme weiter mit LLMs zu kombinieren, um offene mathematische Vermutungen zu lösen.