Resumo Técnico: Pythagoras-Prover

Declaração do Problema

Os modernos provadores de teoremas Lean alcançaram um desempenho robusto, mas dependem fortemente de computação substancial de treinamento e inferência, muitas vezes exigindo modelos de escala de fronteira (centenas de bilhões de parâmetros) ou procedimentos de inferência computacionalmente intensivos, como busca extensa, autocorreção e grandes orçamentos de amostragem. Essa dependência é impulsionada pela escassez de dados de prova verificados e pelas longas traças de raciocínio necessárias para a busca de provas formais, o que torna o ajuste fino supervisionado (SFT) e a amostragem dispendiosos. Consequentemente, existe uma lacuna significativa entre os pequenos provadores de código aberto e seus equivalentes mais robustos, limitando a acessibilidade para pesquisadores e profissionais sem recursos massivos de computação.

Metodologia

Os autores introduzem o Pythagoras-Prover, uma família de provadores de Lean 4 de código aberto e eficientes em termos de computação. A abordagem baseia-se em um pipeline de dados e uma estratégia de treinamento escalonados e econômicos em termos de computação, em vez de escala bruta de modelo.

1. Construção de Dados e Aprendizado por Currículo

O corpus de treinamento é construído em três níveis de dificuldade (Fácil, Médio, Difícil), todos controlados pelo verificador de tipos do Lean para garantir a correção:

• Níveis Fácil e Médio: Gerados via um pipeline de três estágios inspirado em "Theorem Prover as a Judge" (Provador de Teoremas como Juiz). Problemas de linguagem natural de conjuntos de dados como DART-Math-Hard, DeepScaleR e OpenR1-Math são autoformalizados em declarações Lean. Provas falhas são analisadas, e um processo de destilação guiada por rubrica gera variantes sintéticas simplificadas visando categorias específicas de erro (ex: falhas de tática, incompatibilidades de tipo). Este processo resulta em uma melhoria relativa de 30% nas taxas de sucesso de autoformalização.
• Nível Difícil: Extraído de problemas de nível de competição (Olimpíadas, AIME, AMC) do Big-Math-RL-Verified. Diferente dos níveis mais fáceis, estes não são simplificados para preservar sua dificuldade para o aprendizado por reforço (RL).
• SFT por Currículo: Os modelos são treinados usando um currículo ordenado por dificuldade (Fácil $\to$ Médio $\to$ Difícil) com LoRA (Low-Rank Adaptation) para manter a eficiência de parâmetros. Um esquema de filtragem dinâmica de raciocínio de prova é aplicado durante o SFT para gerenciar o orçamento de contexto de 8k tokens: se a cadeia de raciocínio mais a prova exceder o limite, o raciocínio é descartado mantendo a prova; se apenas a prova exceder o limite, a instância é descartada.

2. Formalização Lean Aumentada (ALF) e Autodestilação

Para superar o gargalo da taxa de verificação do Lean, os autores introduzem a Formalização Lean Aumentada (ALF).

• Mecanismo: A ALF aplica cinco operadores de mutação estruturada (simplificação, generalização, proposta de lema, decomposição de passo de prova, reformulação) a instâncias semente verificadas.
• Eficiência: Em vez de verificar cada instância mutada com o Lean (o que é computacionalmente proibitivo), a ALF utiliza uma verificação de alinhamento de declaração leve. Ela verifica se a prova gerada referencia a declaração mutada, garantindo validade estrutural sem compilação total.
• Autodestilação: O modelo pós-RL gera provas para essas declarações mutadas. Isso expande o corpus em aproximadamente 2,5$\times$ (para ~2M de instâncias) sem exigir verificação por instância. Este corpus expandido é usado para SFT contínuo e para treinar um provador baseado em difusão.

3. Arquiteturas de Modelo

A família abrange dois paradigmas de geração:

• Provadores Autorregressivos: Modelos de 4B e 32B de parâmetros treinados com o pipeline acima.
• Provador Baseado em Difusão: Pythagoras-Prover-Diffusion-4B, o primeiro provador de difusão de prova de conceito para Lean. Ele utiliza mascaramento baseado em táticas, onde táticas inteiras do Lean são mascaradas e denoisadas como unidades, em vez de tokens individuais, alinhando o objetivo de denoising com passos discretos de raciocínio.

4. Aprendizado por Reforço (RL)

O RL é realizado em problemas difíceis retidos usando GRPO (Group Relative Policy Optimization) com ajuste fino de parâmetros totais. A recompensa é binária (a prova compila e se alinha com a declaração). Os autores observam que o RL produz apenas ganhos modestos sobre o modelo de currículo-SFT, sugerindo que o alto nível de qualidade do corpus supervisionado já internaliza um forte comportamento de busca de prova.

Principais Contribuições

1. Provadores Eficientes em Computação: Uma família de provadores Lean de código aberto (4B, 32B e um modelo de difusão de 4B) que desafia a suposição de que a prova formal forte exige modelos de escala de fronteira.
2. Pipeline de Dados ALF: Um esquema de mutação estruturada que expande os corpora verificados em ~2,5$\times$ usando verificações de sanidade leves em vez de verificação completa via Lean, desacoplando a expansão do corpus da taxa de processamento do verificador.
3. Benchmark MiniF2F-ALF: Um benchmark de perturbação sensível à contaminação criado aplicando mutações ALF ao conjunto MiniF2F-Test. Serve como um teste de estresse para avaliar se os modelos dependem de recall exato do benchmark ou se possuem comportamentos de prova transferíveis.
4. Primeiro Provador de Difusão: Um provador baseado em difusão viável para Lean, demonstrando que o refinamento iterativo é uma estratégia de decodificação viável para provas formais, apesar das limitações atuais de comprimento de contexto.

Resultados Experimentais

Avaliados em MiniF2F-Test, PutnamBench e MiniF2F-ALF:

• MiniF2F-Test (Pass@32):
  • O Pythagoras-Prover-4B alcança 86,1%, superando o DeepSeek-Prover-V2-671B (82,4%) apesar de ser aproximadamente 167$\times$ menor. Também supera o Goedel-Prover-V2-8B (84,6%) e o Kimina-Prover-70B (84,0%).
  • O Pythagoras-Prover-32B alcança 89,8%, liderando todos os provadores de código aberto avaliados sem autocorreção.
• MiniF2F-Test (Pass@2048):
  • O Pythagoras-Prover-32B atinge 93,03%, estabelecendo um novo estado da arte para provadores neurais Lean de pesos abertos sem autocorreção, superando o Goedel-Prover-V2-32B (92,2% em Pass@8192) com um quarto do orçamento de amostragem.
• PutnamBench:
  • O Pythagoras-Prover-32B resolve 93 de 672 problemas em Pass@2048, o resultado mais forte de código aberto, superando o Goedel-Prover-V2 (86 em Pass@184 com autocorreção).
• MiniF2F-ALF (Robustez):
  • Todos os modelos avaliados degradam neste benchmark perturbado, confirmando que a alta precisão no split original não garante robustez a variantes estruturais.
  • O Pythagoras-Prover-32B permanece o mais forte (85,0%), e o Pythagoras-Prover-4B (83,2%) atinge paridade com o Goedel-Prover-V2-32B (83,6%) que é 8$\times$ maior, degradando menos sob perturbação.
• Eficiência de Difusão:
  • O Pythagoras-Prover-Diffusion-4B alcança 63,25% de Pass@32 no MiniF2F-Test. Embora menos preciso que seu equivalente autorregressivo, ele gera provas 2,58$\times$ mais rápido (10,56 vs 4,10 tokens/seg), oferecendo um maior throughput por segundo de GPU.

Significância e Alegações

O artigo afirma que a prova de teoremas Lean forte não precisa depender exclusivamente de modelos de escala de fronteira. Os resultados demonstram que a construção cuidadosa de dados (aprendizado por currículo, aumento ALF, autodestilação) e receitas de treinamento eficientes (LoRA, filtragem dinâmica) podem substituir, em parte, a escala bruta do modelo.

Especificamente, os autores destacam:

• Eficiência: O Pythagoras-Prover-4B supera um modelo de 671 bilhões de parâmetros, sugerindo que a receita de treinamento proposta transfere-se bem para regimes de modelos pequenos onde baselines de escala de bilhões são impraticáveis.
• Robustez: O uso de mutações ALF durante o treinamento melhora a robustez a perturbações no nível da declaração, como evidenciado pela menor queda de desempenho no MiniF2F-ALF em comparação com os baselines.
• Novos Paradigmas: A introdução de um provador baseado em difusão estabelece uma linha de base inicial para o refinamento iterativo na prova formal, abrindo uma direção complementar onde os provadores podem ser comparados por throughput e provas por segundo de GPU, não apenas precisão.

Os autores concluem que o pipeline de dados "econômico em computação" é o principal motor desses resultados, permitindo um desempenho de estado da arte sob orçamentos de computação práticos.