🤖 AI

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

Pythagoras-Prover ist eine effiziente Familie von Open-Source-Lean-Theorembeweisern, die kurrikularbasiertes überwachtes Fine-Tuning und Augmented Lean Formalisation nutzt, um mit signifikant weniger Parametern als bestehende Modelle Spitzenleistungen bei formalen Beweis-Benchmarks zu erzielen.

Ursprüngliche Autoren: Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia

Veröffentlicht 2026-06-12

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, einem Roboter beizubringen, extrem schwierige mathematische Rätsel zu lösen, aber mit einem Haken: Der Roboter muss seine Lösung in einer strengen, computerlesbaren Sprache namens Lean schreiben. Wenn der Roboter auch nur einen winzigen logischen Fehler macht, lehnt der Computer die Antwort ab. Dies ist die Welt des Automated Theorem Proving (automatisches Beweistheorem-Verfahren).

Lange Zeit war der einzige Weg, einen Roboter gut darin zu machen, ihn mit massiven Datenmengen zu füttern und ein riesiges „Gehirn“ (ein Computermodell) zu verwenden, das Millionen von Dollar kostet. Es war, als würde man versuchen, ein Schachturnier zu gewinnen, indem man ein Team von 1.000 Großmeistern anheuert, die für einen denken.

Das Paper stellt Pythagoras-Prover vor, eine neue Familie von Roboter-Mathematikern, die beweist, dass man kein riesiges Gehirn oder ein Millionen-Dollar-Budget braucht, um zu gewinnen. Sie erreichten dies durch drei clevere Tricks:

1. Das „Trainingslager“ (Curriculum Learning)

Anstatt den Roboter sofort in das tiefe Wasser mit den schwierigsten Problemen zu werfen, bauten die Forscher ein Trainingslager mit drei Stufen: Leicht, Mittel und Schwer.

Die Analogie: Stellen Sie sich vor, Sie bringen einem Kind das Fahrradfahren bei. Sie beginnen nicht auf einem Bergpfad. Sie beginnen auf einem flachen Bürgersteig (Leicht), dann auf einem sanften Hügel (M mittel) und schließlich auf dem Bergpfad (Schwer).
Wie sie es machten: Sie erstellten eine riesige Bibliothek mathematischer Probleme. Wenn ein Problem zu schwer für den Roboter war, warf man es nicht einfach weg. Sie nutzten ein „Rubrik“ (eine Checkliste gängiger Fehler), um das Problem in eine einfachere Version zu zerlegen, die der Roboter konnte. Dies ermöglichte es dem Roboter, Schritt für Schritt zu lernen und Selbstvertrauen sowie Geschick aufzubauen, bevor er die Giganten anpackte.

2. Die „Mad Libs“-Maschine (Augmented Lean Formalisation)

Das größte Problem in diesem Bereich ist der Mangel an guten Übungsproblemen. Die Forscher erkannten, dass sie mehr Übungsprobleme erschaffen konnten, ohne dass ein Mensch sie schreiben oder ein Supercomputer sie prüfen musste.

Die Analogie: Stellen Sie sich vor, Sie haben eine perfekte mathematische Geschichte. Anstatt eine völlig neue Geschichte von Grund auf neu zu schreiben, spielen Sie ein Spiel wie „Mad Libs“. Sie tauschen die Zahlen aus, ändern die Namen der Charaktere oder ordnen die Reihenfolge der Schritte neu an, aber die Logik der Geschichte bleibt dieselbe.
Wie sie es machten: Sie nahmen ihre verifizierten Probleme und nutzten ein Werkzeug namens ALF, um sie zu mutieren. Sie erstellten Variationen (einfachere Versionen, schwierigere Versionen oder einfach nur eine andere Formulierung), aber die Logik der Geschichte blieb dieselbe. Sie erstellten Variationen (einfachere Versionen, schwierigere Versionen oder einfach nur eine andere Formulierung), aber die Logik der Geschichte blieb dieselbe. Sie prüften nicht jede einzelne neue Variation mit dem strengen Computer (was langsam und teuer ist); sie prüften lediglich, ob die neue Aufgabe wie ein gültiges mathematisches Problem aussah. Dies vervielfachte ihre Bibliothek an Übungsproblemen um das 2,5-fache und gab dem Roboter viel mehr Material, von dem er lernen konnte.

3. Die „Selbstreflexions“-Schleife (Self-Distillation)

Sobald der Roboter die Grundlagen gelernt hatte, ließen sie ihn sich selbst beibringen.

Die Analogie: Stellen Sie sich einen Schüler vor, der hart studiert hat. Anstatt nur eine Prüfung abzulegen, versucht er, neue Variationen der Probleme zu lösen, die er gerade erst gelernt hat. Wenn er es richtig macht, schreibt er es als neues Beispiel für sich selbst auf, das er später studieren kann.
Wie sie es machten: Der Roboter generierte Beweise für diese „Mad Libs“-Variationen. Selbst wenn der Computer nicht jedes einzelne davon doppelt prüfte, bedeutete die Tatsache, dass der Roboter einen Beweis für eine mutierte Version generieren konnte, dass er die Logik wirklich verstand und nicht nur die Antwort auswendig lernte. Diese „selbstgelehrte“ Daten machten den Roboter noch intelligenter.

Die Ergebnisse: Kleines Gehirn, große Siege

Das Paper vergleicht ihre neuen Roboter mit den aktuellen „Giganten“ auf diesem Gebiet:

Der 4B-Roboter: Dieser Roboter hat 4 Milliarden „Neuronen“ (Parameter). Er ist etwa 167 Mal kleiner als der bisherige Champion (DeepSeek-Prover-V2, der 671 Milliarden Neuronen hat).
- Das Ergebnis: Trotz seiner geringen Größe löste der 4B-Roboter mehr Probleme korrekt als der riesige Roboter. Es ist, als würde ein mathematisches Genie aus der High School ein Team von PhDs besiegen, weil das Genie besser trainiert wurde.
Der 32B-Roboter: Dieser etwas größere Roboter wurde der beste Open-Source-Roboter, der jemals auf diesen Benchmarks getestet wurde, und löste 93 % der Probleme.

Das „Diffusion“-Experiment

Die Forscher probierten auch eine andere Denkweise namens Diffusion aus.

Die Analogie:
- Standard (Autoregressiv): Einen Satz Wort für Wort schreiben, von links nach rechts. Wenn man am Anfang einen Fehler macht, muss man alles neu schreiben.
- Diffusion: Stellen Sie sich eine verschwommene Skizze eines Satzes vor. Der Roboter betrachtet die gesamte Skizze und füllt die fehlenden Wörter alle auf einmal aus, indem er das Bild verfeinert, bis es klar ist. Er kann einen Fehler in der Mitte korrigieren, ohne den Anfang neu schreiben zu müssen.
Das Ergebnis: Dieser „Diffusion“-Roboter war 2,5 Mal schneller beim Generieren von Antworten als der Standard-Roboter, war jedoch etwas weniger präzise. Dies zeigt einen neuen Weg, um Geschwindigkeit gegen Präzision abzuwägen.

Der „Stresstest“ (MiniF2F-ALF)

Um zu sehen, ob die Roboter nur Antworten auswendig lernten oder tatsächlich lernten, erstellten die Forscher einen „Stresstest“. Sie nahmen die Testfragen und mutierten sie leicht (Änderung von Zahlen, Austausch von Variablen) mit derselben „Mad Libs“-Technik.

Das Ergebnis: Die meisten Roboter scheiterten an diesem Test, weil sie die ursprünglichen Fragen auswendig gelernt hatten. Pythagoras-Prover hingegen bewältigte diese Mutationen viel besser. Dies beweist, dass sie die Logik der Mathematik gelernt haben, nicht nur die spezifischen Antworten.

Zusammenfassung

Pythagoras-Prover zeigt, dass man keinen Supercomputer braucht, um schwierige mathematische Beweise zu lösen. Indem man einen klugen Trainingsplan nutzt, endlose Variationen von Übungsproblemen erstellt und den Roboter sich selbst lehren lässt, kann man einen kleinen, effizienten Roboter bauen, der die massiven, teuren Giganten der Vergangenheit übertrifft.

Technisches Resümee: Pythagoras-Prover

Problemstellung

Moderne Lean-Theorembeweiser haben eine starke Leistung erreicht, hängen jedoch stark von erheblichem Trainings- und Inferenz-Compute ab, was oft Frontiere-Skala-Modelle (Hunderte von Milliarden Parametern) oder rechenintensive Inferenzverfahren wie umfangreiche Suche, Selbstkorrektur und große Sampling-Budgets erfordert. Diese Abhängigkeit wird durch die Knappheit an verifizierten Beweisdaten und die langen Reasoning-Traces für die formale Beweissuche vorangetrieben, was Supervised Fine-Tuning (SFT) und Sampling teuer macht. Folglich besteht eine signifikante Lücke zwischen kleinen Open-Source-Provern und ihren größten Gegenstücken, was den Zugang für Forscher und Praktiker ohne massive Rechenressourcen einschränkt.

Methodik

Die Autoren führen Pythagoras-Prover ein, eine compute-effiziente Familie von Open-Source Lean 4 Theorembeweisern. Der Ansatz stützt sich auf eine gestufte, compute-sparende Datenpipeline und eine Trainingsstrategie statt auf rohe Modellskalierung.

1. Datenkonstruktion und Curriculum Learning

Der Trainingskorpus wird in drei Schwierigkeitsstufen (Easy, Medium, Hard) konstruiert, die alle durch den Lean-Typenprüfer zur Sicherstellung der Korrektheit gefiltert werden:

Easy und Medium Tiers: Generiert über eine dreistufige Pipeline, die von „Theorem Prover as a Judge“ inspiriert ist. Natürliche Sprachprobleme aus Datensätzen wie DART-Math-Hard, DeepScaleR und OpenR1-Math werden in Lean-Statements autoformalisiert. Fehlgeschlagene Beweise werden analysiert, und ein rubrikgesteuerter Destillationsprozess generiert vereinfachte synthetische Varianten, die gezielt bestimmte Fehlerkategorien adressieren (z. B. Taktik-Fehler, Typ-Fehlpaarungen). Dieser Prozess liefert eine relative Verbesserung der Erfolgsrate bei der Autoformalisierung um 30 %.
Hard Tier: Bezieht sich auf wettbewerbsrelevante Probleme (Olympiaden, AIME, AMC) aus Big-Math-RL-Verified. Im Gegensatz zu den leichteren Stufen werden diese nicht vereinfacht, um ihre Schwierigkeit für das Reinforcement Learning (RL) zu bewahren.
Curriculum SFT: Modelle werden mit einem nach Schwierigkeit geordneten Curriculum (Easy $\to$ Medium $\to$ Hard) unter Verwendung von LoRA (Low-Rank Adaptation) trainiert, um die Parametereffizienz beizubehalten. Während des SFT wird ein dynamisches Proof-Reasoning-Filterungsschema angewendet, um das 8k-Token-Kontextbudget zu verwalten: Wenn die Reasoning-Kette plus Beweis das Limit überschreitet, wird das Reasoning verworfen, während der Beweis erhalten bleibt; wenn allein der Beweis das Limit überschreitet, wird die Instanz verworfen.

2. Augmented Lean Formalisation (ALF) und Selbst-Destillation

Um den Flaschenhals des Lean-Verifikationsdurchsatzes zu überwinden, führen die Autoren die Augmented Lean Formalisation (ALF) ein.

Mechanismus: ALF wendet fünf strukturierte Mutationsoperatoren (Vereinfachung, Generalisierung, Lemma-Vorschlag, Beweisschritt-Dekomposition, Reformulierung) auf verifizierte Seed-Instanzen an.
Effizienz: Anstatt jede mutierte Instanz mit Lean zu verifizieren (was rechentechnisch prohibitiv wäre), nutzt ALF einen leichtgewichtigen Statement-Alignment-Check. Es verifiziert, dass der generierte Beweis das mutierte Statement referenziert, wodurch die strukturelle Validität ohne vollständige Kompilierung sichergestellt wird.
Selbst-Destillation: Das Post-RL-Modell generiert Beweise für diese mutierten Statements. Dies erweitert den Korpus um etwa das 2,5-Fache (auf ~2 Mio. Instanzen), ohne eine Verifikation pro Instanz zu erfordern. Dieser erweiterte Korpus wird für das fortgesetzte SFT und zum Training eines Diffusions-basierten Provers verwendet.

3. Modellarchitekturen

Die Familie umfasst zwei Generationsparadigmen:

Autoregressive Prover: 4B- und 32B-Parameter-Modelle, die mit der obigen Pipeline trainiert wurden.
Diffusions-basierter Prover: Pythagoras-Prover-Diffusion-4B, der erste Proof-of-Concept eines diffusionsbasierten Theorembeweisers für Lean. Er nutzt Taktik-basiertes Masking, bei dem ganze Lean-Takti als Einheiten statt als einzelne Token maskiert und gedenoised werden, wodurch das Denoising-Ziel mit diskreten Reasoning-Schritten übereinstimmt.

4. Reinforcement Learning (RL)

RL wird auf gehaltenen (held-out) Hard-Problemen mittels GRPO (Group Relative Policy Optimization) mit Full-Parameter Fine-Tuning durchgeführt. Die Belohnung (Reward) ist binär (Beweis kompiliert und stimmt mit dem Statement überein). Die Autoren stellen fest, dass RL nur moderate Gewinne gegenüber dem Curriculum-SFT-Modell liefert, was darauf hindeutet, dass der hochwertige supervidierte Korpus bereits ein starkes Proof-Search-Verhalten internalisiert hat.

Wichtigste Beiträge

Compute-effiziente Prover: Eine Familie von Open-Source Lean-Provern (4B, 32B und ein 4B Diffusionsmodell), die die Annahme infrage stellt, dass starkes formales Reasoning Frontiere-Skala-Modelle erfordert.
ALF-Datenpipeline: Ein strukturiertes Mutationsschema, das verifizierte Korpora durch leichte Sanity-Checks statt durch per-Instanz Lean-Verifikation um ~2,5 $\times$ erweitert und so die Korpus-Erweiterung vom Verifikationsdurchsatz entkoppelt.
MiniF2F-ALF Benchmark: Ein Kontaminations-sensitiver Perturbations-Benchmark, der durch Anwendung von ALF-Mutationen auf den MiniF2F-Test-Satz erstellt wurde. Er dient als Stresstest, um zu evaluieren, ob Modelle auf exakten Benchmark-Recall basieren oder über transferierbare Beweis-Verhaltensweisen verfügen.
Erster Diffusions-Theorembeweiser: Ein lebensfähiger diffusionsbasierter Beweiser für Lean, der zeigt, dass iteratives Refinement eine praktikable Decoding-Strategie für formale Beweise ist, wenngleich mit aktuellen Einschränkungen bei der Kontextlänge.

Experimentelle Ergebnisse

Evaluierung auf MiniF2F-Test, PutnamBench und MiniF2F-ALF:

MiniF2F-Test (Pass@32):
- Pythagoras-Prover-4B erreicht 86,1 % und übertrifft damit DeepSeek-Prover-V2-671B (82,4 %), obwohl es etwa 167 $\times$ kleiner ist. Es übertrifft zudem Goedel-Prover-V2-8B (84,6 %) und Kimina-Prover-70B (84,0 %).
- Pythagoras-Prover-32B erreicht 89,8 % und führt alle evaluierten Open-Source-Prover ohne Selbstkorrektur an.
MiniF2F-Test (Pass@2048):
- Pythagoras-Prover-32B erreicht 93,03 % und setzt einen neuen Stand der Technik (SOTA) für Open-Weight neuronale Lean-Prover ohne Selbstkorrektur, wobei es Goedel-Prover-V2-32B (92,2 % bei Pass@8192) mit einem Viertel des Sampling-Budgets übertrifft.
PutnamBench:
- Pythagoras-Prover-32B löst 93 von 672 Problemen bei Pass@2048, das stärkste Open-Source-Ergebnis, und übertrifft Goedel-Prover-V2 (86 bei Pass@184 mit Selbstkorrektur).
MiniF2F-ALF (Robustheit):
- Alle evaluierten Modelle zeigen eine Verschlechterung auf diesem perturbierten Benchmark, was bestätigt, dass hohe Genauigkeit im Original-Split keine Robustheit gegenüber strukturellen Varianten garantiert.
- Pythagoras-Prover-32B bleibt am stärksten (85,0 %), und Pythagoras-Prover-4B (83,2 %) erreicht Parität mit dem 8 $\times$ größeren Goedel-Prover-V2-32B (83,6 %) und degradiert unter Perturbation weniger stark.
Diffusions-Effizienz:
- Pythagoras-Prover-Diffusion-4B erreicht 63,25 % Pass@32 auf MiniF2F-Test. Obwohl es weniger genau ist als sein autoregressives Gegenstück, generiert es Beweise 2,58 $\times$ schneller (10,56 vs. 4,10 Tokens/Sek.), was einen höheren Durchsatz pro GPU-Sekunde bietet.

Bedeutung und Behauptungen

Das Paper behauptt, dass starkes Lean-Theorembeweisen nicht ausschließlich auf Frontiere-Skala-Modellen basieren muss. Die Ergebnisse zeigen, dass sorgfältige Datenkonstruktion (Curriculum Learning, ALF-Augmentierung, Selbst-Destillation) und effiziente Trainingsrezepte (LoRA, dynamisches Filtering) teilweise die rohe Modellskalierung ersetzen können.

Insbesondere heben die Autoren hervor:

Effizienz: Pythagoras-Prover-4B übertrifft ein 671B-Parameter-Modell, was darauf hindeutet, dass das vorgeschlagene Trainingsrezept sauber auf kleine Modellregime übertragbar ist, in denen Milliarden-Skala-Baselines unpraktikabel sind.
Robustheit: Die Verwendung von ALF-Mutationen während des Trainings verbessert die Robustheit gegenüber Statement-Level-Perturbationen, wie die geringere Leistungsabnahme auf MiniF2F-ALF im Vergleich zu Baselines zeigt.
Neue Paradigmen: Die Einführung eines diffusionsbasierten Beweisers etabliert eine erste Baseline für iteratives Refinement in der formalen Beweisführung und eröffnet eine komplementäre Richtung, in der Beweiser durch Durchsatz und Beweise-pro-GPU-Sekunde statt nur durch Genauigkeit verglichen werden können.

Die Autoren kommen zu dem Schluss, dass die „compute-sparende“ Datenpipeline der primäre Treiber dieser Ergebnisse ist, was eine State-of-the-Art-Leistung unter praktischen Compute-Budgets ermöglicht.