Pythagoras-Prover: Avançando na Prova Formal Eficiente via Formalização Lean Aumentada

Resumo

Os modernos provadores de teoremas Lean alcançam alto desempenho apenas com custo computacional substancial de treinamento e inferência, impulsionado em parte pela escassez de dados de provas verificadas e pelos longos traços de raciocínio da busca formal de provas, tornando tanto o ajuste fino supervisionado (SFT) quanto a amostragem caros. Apresentamos o Pythagoras-Prover, uma família de provadores de teoremas Lean eficientes em termos computacionais e de código aberto, projetada para orçamentos computacionais práticos. A família abrange dois paradigmas de geração: modelos autorregressivos com 4B e 32B de parâmetros, e um primeiro protótipo de provador baseado em difusão (4B) que refina iterativamente provas Lean em tempo de inferência. Para eficiência de treinamento, construímos um corpus verificado em Lean estratificado em problemas fáceis, médios e difíceis para SFT curricular, de modo que os modelos adquiram habilidades de prova progressivamente, passando de provas mais curtas e simples para provas mais longas e complexas. Durante o SFT, um esquema dinâmico de filtragem de raciocínio de provas preserva traços de prova informativos, mantendo cada instância dentro de um orçamento de contexto de 8 mil tokens. Também introduzimos a Formalização Aumentada Lean (ALF), que expande corpora verificados escassos em variantes de declarações formais, preenchidas por meio de autodestilação para sinal de treinamento extra, sem verificar formalmente cada instância mutada. Ao perturbar problemas conhecidos enquanto preserva seu caráter formal, a ALF reduz a dependência da forma superficial de qualquer declaração. Empiricamente, o Pythagoras-Prover-4B supera o DeepSeek-Prover-V2-671B no pass@32 do MiniF2F-Test (86,1% vs 82,4%) com aproximadamente 167x menos parâmetros, enquanto o Pythagoras-Prover-32B estabelece o estado da arte de código aberto com 93,0% no MiniF2F-Test e resolve 93 dos 672 problemas do PutnamBench. Disponibilizamos o MiniF2F-ALF, um benchmark sensível a contaminação com mutações ALF no qual todos os modelos avaliados perdem precisão; aqui, nosso modelo de 32B permanece o mais forte, e o de 4B iguala o estado da 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.