Pythagoras-Prover: Fortschritte bei effizientem formalem Beweisen durch erweiterte Lean-Formalisierung

Zusammenfassung

Moderne Lean-Theorembeweiser erzielen nur mit erheblichem Trainings- und Inferenzrechenaufwand eine hohe Leistung, was unter anderem auf die spärlichen verifizierten Beweisdaten und die langen Ableitungsspuren der formalen Beweissuche zurückzuführen ist, was sowohl überwachtes Feintuning (SFT) als auch Sampling teuer macht. Wir stellen Pythagoras-Prover vor, eine recheneffiziente Open-Source-Familie von Lean-Theorembeweisern, die für praktische Rechenbudgets ausgelegt ist. Die Familie umfasst zwei Generationsparadigmen: autoregressive Modelle mit 4B und 32B Parametern sowie einen ersten Proof-of-Concept-diffusionsbasierten Beweiser (4B), der Lean-Beweise zur Inferenzzeit iterativ verfeinert. Für die Trainingseffizienz bauen wir ein Lean-verifiziertes Korpus auf, das für ein Curriculum-basiertes SFT in einfache, mittlere und schwere Probleme geschichtet ist, sodass Modelle Beweisfähigkeiten schrittweise von kürzeren, einfacheren Beweisen zu längeren, schwierigeren erwerben. Während des SFT sorgt ein dynamisches Beweis-Schlussfolgerungs-Filterungsschema dafür, dass informative Beweisspuren erhalten bleiben, während jede Instanz innerhalb eines Kontextbudgets von 8k-Token bleibt. Wir führen außerdem Augmented Lean Formalisation (ALF) ein, die spärliche verifizierte Korpora zu Varianten formaler Aussagen erweitert, die mittels Selbst-Destillation mit zusätzlichem Trainingssignal gefüllt werden, ohne jede mutierte Instanz formal zu verifizieren. Durch die Störung bekannter Probleme unter Beibehaltung ihres formalen Charakters reduziert ALF die Abhängigkeit von der Oberflächenform einer Aussage. Empirisch übertrifft Pythagoras-Prover-4B DeepSeek-Prover-V2-671B bei pass@32 auf MiniF2F-Test (86,1 % vs. 82,4 %) bei ~167x weniger Parametern, während Pythagoras-Prover-32B mit 93,0 % auf MiniF2F-Test den Open-Source-Stand der Technik setzt und 93 von 672 PutnamBench-Problemen löst. Wir veröffentlichen MiniF2F-ALF, einen ALF-mutierten, kontaminationsempfindlichen Benchmark, bei dem jedes evaluierte Modell an Genauigkeit verliert; hier bleibt unser 32B-Modell am stärksten und unser 4B-Modell erreicht den vorherigen Stand der Technik, Goedel-Prover-V2-32B.

English

Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both supervised fine-tuning (SFT) and sampling expensive. We introduce Pythagoras-Prover, a compute-efficient open-source family of Lean theorem provers built for practical compute budgets. The family spans two generation paradigms: autoregressive models at 4B and 32B parameters, and a first proof-of-concept diffusion-based prover (4B) that iteratively refines Lean proofs at inference time. For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT, so models acquire proof skills progressively from shorter, simpler proofs to longer, harder ones. During SFT, a dynamic proof-reasoning filtering scheme preserves informative proof traces while keeping each instance within an 8k-token context budget. We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements, populated via self-distillation for extra training signal without formally verifying every mutated instance. By perturbing known problems while preserving their formal character, ALF reduces reliance on any statement's surface form. Empirically, Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test (86.1% vs 82.4%) with ~167x fewer parameters, while Pythagoras-Prover-32B sets the open-source state of the art at 93.0% on MiniF2F-Test and solves 93 of 672 PutnamBench problems. We release MiniF2F-ALF, an ALF-mutated contamination-sensitive benchmark on which every evaluated model loses accuracy; here our 32B remains strongest and our 4B matches the prior state of the art, Goedel-Prover-V2-32B.