Pythagoras-Prover : Avancées dans la preuve formelle efficace via la formalisation Lean augmentée

Résumé

Les prouveurs de théorèmes Lean modernes n’atteignent des performances élevées qu’avec des ressources computationnelles importantes en entraînement et en inférence, en partie à cause de la rareté des données de preuves vérifiées et des longues traces de raisonnement issues de la recherche de preuves formelles, ce qui rend coûteux à la fois le fine-tuning supervisé (SFT) et l’échantillonnage. Nous présentons Pythagoras-Prover, une famille de prouveurs Lean open source économes en calcul, conçue pour des budgets computationnels pratiques. Cette famille couvre deux paradigmes de génération : des modèles autorégressifs de 4B et 32B paramètres, ainsi qu’un premier prouveur basé sur la diffusion (4B) à titre de preuve de concept, qui affine itérativement les preuves Lean au moment de l’inférence. Pour l’efficacité de l’entraînement, nous construisons un corpus vérifié Lean stratifié en problèmes faciles, moyens et difficiles pour un SFT curriculaire, permettant aux modèles d’acquérir progressivement des compétences en preuve, depuis des preuves plus courtes et simples jusqu’à des preuves plus longues et complexes. Pendant le SFT, un mécanisme de filtrage dynamique du raisonnement de preuve préserve les traces informatives tout en maintenant chaque instance dans un budget de contexte de 8k tokens. Nous introduisons également l’Augmented Lean Formalisation (ALF), qui étend les corpus vérifiés rares en variants d’énoncés formels, peuplés via auto-distillation pour un signal d’entraînement supplémentaire sans vérifier formellement chaque instance mutée. En perturbant des problèmes connus tout en préservant leur caractère formel, ALF réduit la dépendance à la forme de surface d’un énoncé. Empiriquement, Pythagoras-Prover-4B surpasse DeepSeek-Prover-V2-671B à pass@32 sur MiniF2F-Test (86.1 % contre 82.4 %) avec environ 167 fois moins de paramètres, tandis que Pythagoras-Prover-32B établit un nouvel état de l’art open source à 93.0 % sur MiniF2F-Test et résout 93 des 672 problèmes de PutnamBench. Nous publions MiniF2F-ALF, un benchmark sensible à la contamination par mutation ALF sur lequel chaque modèle évalué perd en précision ; ici, notre modèle 32B reste le plus fort et notre modèle 4B égale l’état de l’art précédent, 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.