Pythagoras-Prover: Avanzando en la demostración formal eficiente mediante la formalización aumentada en Lean

Resumen

Los modernos demostradores de teoremas en Lean logran un alto rendimiento solo con un cómputo considerable en entrenamiento e inferencia, impulsado en parte por la escasez de datos de demostraciones verificadas y las largas trazas de razonamiento de la búsqueda formal de demostraciones, lo que encarece tanto el ajuste fino supervisado (SFT) como el muestreo. Presentamos Pythagoras-Prover, una familia de demostradores de teoremas en Lean de código abierto y eficientes en cómputo, diseñados para presupuestos computacionales prácticos. La familia abarca dos paradigmas de generación: modelos autorregresivos de 4B y 32B parámetros, y un primer demostrador basado en difusión como prueba de concepto (4B) que refina iterativamente demostraciones en Lean durante la inferencia. Para la eficiencia del entrenamiento, construimos un corpus verificado en Lean estratificado en problemas fáciles, medios y difíciles para un SFT curricular, de modo que los modelos adquieran habilidades de demostración progresivamente a partir de demostraciones más cortas y simples hacia otras más largas y complejas. Durante el SFT, un esquema de filtrado dinámico de razonamiento de demostraciones conserva trazas de demostración informativas, manteniendo cada instancia dentro de un presupuesto de contexto de 8k tokens. También introducimos la Formalización Aumentada de Lean (ALF), que expande los corpus verificados escasos en variantes de enunciados formales, pobladas mediante autodestilación para proporcionar una señal de entrenamiento adicional sin verificar formalmente cada instancia mutada. Al perturbar problemas conocidos preservando su carácter formal, ALF reduce la dependencia de la forma superficial de cualquier enunciado. Empíricamente, Pythagoras-Prover-4B supera a DeepSeek-Prover-V2-671B en pass@32 en MiniF2F-Test (86.1 % frente a 82.4 %) con ~167 veces menos parámetros, mientras que Pythagoras-Prover-32B establece el estado del arte de código abierto en un 93.0 % en MiniF2F-Test y resuelve 93 de los 672 problemas de PutnamBench. Publicamos MiniF2F-ALF, un punto de referencia sensible a la contaminación mutado con ALF en el cual todos los modelos evaluados pierden precisión; aquí nuestro modelo de 32B sigue siendo el más robusto y nuestro modelo de 4B iguala el estado del arte anterior, 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.