Pythagoras-Prover: Vooruitgang in efficiënt formeel bewijzen via uitgebreide Lean-formalisatie

Samenvatting

Moderne Lean-stellingbewijzers behalen sterke prestaties alleen met aanzienlijke rekenkracht voor training en inferentie, deels gedreven door schaarse geverifieerde bewijsdata en de lange redeneersporen van formeel bewijszoeken, waardoor zowel gesuperviseerde fijnafstelling (SFT) als bemonstering duur worden. Wij introduceren Pythagoras-Prover, een rekenefficiënte open-sourcefamilie van Lean-stellingbewijzers, gebouwd voor praktische rekenbudgetten. De familie omvat twee generatieparadigma’s: autoregressieve modellen met 4B en 32B parameters, en een eerste proof-of-concept diffusiegebaseerde bewijzer (4B) die tijdens inferentie iteratief Lean-bewijzen verfijnt. Voor trainingsefficiëntie bouwen we een Lean-geverifieerd corpus, gestratificeerd in eenvoudige, middelmatige en moeilijke problemen voor curriculum SFT, zodat modellen progressief bewijsvaardigheden verwerven van kortere, eenvoudigere bewijzen naar langere, moeilijkere. Tijdens SFT behoudt een dynamisch filteringsschema voor bewijsredeneringen informatieve bewijssporen, terwijl elk exemplaar binnen een contextbudget van 8k tokens blijft. We introduceren ook Augmented Lean Formalisation (ALF), dat schaarse geverifieerde corpora uitbreidt tot varianten van formele beweringen, gevuld via zelfdistillatie voor extra trainingssignaal zonder elke gemuteerde instantie formeel te verifiëren. Door bekende problemen te verstoren terwijl hun formele karakter behouden blijft, vermindert ALF de afhankelijkheid van de oppervlaktevorm van een bewering. Empirisch overtreft Pythagoras-Prover-4B DeepSeek-Prover-V2-671B bij pass@32 op MiniF2F-Test (86,1% versus 82,4%) met ~167x minder parameters, terwijl Pythagoras-Prover-32B de open-source stand der techniek vestigt op 93,0% op MiniF2F-Test en 93 van de 672 PutnamBench-problemen oplost. We brengen MiniF2F-ALF uit, een ALF-gemuteerde contaminatiegevoelige benchmark waarop elk geëvalueerd model aan nauwkeurigheid inboet; hier blijft onze 32B het sterkst en evenaart onze 4B de eerdere stand der techniek, 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.