Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

Título: Compile to Compress: Impulsionando Provedores de Teoremas Formais por Meios de Saídas de Compiladores

1. O Problema

Os Grandes Modelos de Linguagem (LLMs) demonstraram potencial significativo na prova formal de teoremas (especialmente no assistente de provas Lean). No entanto, o estado da arte enfrenta um gargalo de escalabilidade:

• Custo Computacional Excessivo: As melhores performances atuais exigem "roll-outs" massivos (muitas tentativas de geração) ou janelas de contexto extremamente longas para acumular histórico de tentativas de correção.
• Ineficiência na Retroalimentação: Abordagens existentes tendem a simplificar as mensagens de erro do compilador para indicadores binários (sucesso/fracasso) ou mensagens de texto plano. Isso ignora a rica estrutura semântica contida nos erros, forçando o modelo a depender de históricos de interação longos e custosos para corrigir erros.
• Limitação de Contexto: À medida que o modelo acumula tentativas falhas para tentar corrigi-las, a janela de contexto cresce rapidamente, limitando a profundidade da exploração dentro de orçamentos computacionais fixos.

2. Metodologia: O Framework "Learning-to-Refine"

Os autores propõem uma nova perspectiva: tratar o compilador Lean como um compressor de dimensões. Enquanto o espaço de programas Lean válidos é vasto e combinatorial, o espaço de mensagens de erro do compilador é compacto e estruturado.

Conceitos Chave:

• Compressão de Dimensão: O compilador mapeia um vasto espaço de tentativas de prova diversas para um conjunto compacto de "modos de falha" estruturados. Muitos programas sintaticamente diferentes geram a mesma assinatura de erro, revelando defeitos semânticos subjacentes.
• Refinamento Orientado por Modos de Falha: Em vez de gerar provas do zero, o modelo aprende a refinar (corrigir) programas falhos com base na mensagem de erro específica. Isso permite uma correção local e direcionada, sem a necessidade de relembrar todo o histórico de tentativas.
• Cadeia de Distribuições (Chain of Distributions - CoD): O processo de auto-correção não amostra de uma única distribuição fixa. Em vez disso, cada etapa de refinamento condiciona a próxima tentativa à mensagem de erro anterior, criando uma cadeia dinâmica de distribuições que explora regiões do espaço de programas que seriam "fora da distribuição" (OOD) para uma geração direta.

Pipeline de Treinamento:

1. Síntese de Dados (Cold-Start): Utiliza-se um modelo de IA (Claude-3.7-Sonnet) para analisar erros de compilação e gerar um "pensamento" (razão) que explica como corrigir o erro, criando pares de (estado falho + correção).
2. Ajuste Fino Supervisionado (SFT): O provador base é fine-tuned com esses dados de refinamento, aprendendo a mapear mensagens de erro para correções de código.
3. Iteração de Especialistas (Expert Iteration): O modelo é executado em problemas de treinamento, refinando suas próprias falhas iterativamente até encontrar uma solução. Os trajetos bem-sucedidos são usados para atualizar o modelo, adaptando-o à distribuição de erros que ele mesmo gera.
4. Estratégia de Busca em Tempo de Teste:
   • O sistema modela a correção como um problema de busca.
   • Busca Árvore Aleatória: Mistura geração direta (BFS) e refinamento (DFS).
   • Busca Guiada por Valor: Um modelo de valor neural estima o potencial de cada nó na árvore de busca (se vale a pena refinar ou gerar do zero), otimizando a alocação do orçamento computacional.

3. Contribuições Principais

• Novo Paradigma de Aprendizado: Introduz o conceito de usar mensagens de compilador como uma representação latente estruturada para guiar o refinamento, em vez de apenas como feedback binário.
• Eficiência Escalável: O método reduz drasticamente a dependência de janelas de contexto longas, permitindo que modelos menores (8B e 32B) alcancem desempenho de ponta com orçamentos de teste comparáveis.
• Framework Agnóstico ao Modelo: A abordagem funciona independentemente do modelo base, demonstrando ganhos consistentes ao escalar o tamanho do modelo e o orçamento de computação.
• Análise Teórica e Empírica: Demonstra matematicamente e empiricamente que o refinamento induz distribuições de amostragem estatisticamente distintas da geração direta, permitindo escapar de ótimos locais no espaço de provas.

4. Resultados Experimentais

Os experimentos foram conduzidos nos modelos Kimina-Prover-Distill-8B e Goedel-Prover-V2-32B em benchmarks padrão (MiniF2F, ProofNet, MathOlympiadBench e PutnamBench).

• Desempenho Geral: Os provadores aprimorados superaram consistentemente suas contrapartes base em todos os benchmarks. No Goedel-32B, houve melhorias relativas superiores a 50% em ProofNet, MathOlympiadBench e PutnamBench.
• PutnamBench (Estado da Arte):
  • Na categoria ~32B, o método resolveu 110 problemas, superando todas as outras soluções de escala comparável (incluindo Ax-Prover e o próprio Goedel-V2 em modo de auto-correção nativo).
  • Na categoria ~8B, o método resolveu 25 problemas, ficando em primeiro lugar entre modelos de tamanho similar.
• Eficiência de Busca: A estratégia de busca guiada por valor superou a busca aleatória e a geração direta (BFS) na maioria dos casos, especialmente em problemas difíceis onde a correção iterativa é necessária.
• Análise de Erros: A correção é mais eficaz para erros estruturais recorrentes e localizáveis (ex: "failed to synthesize"). Erros semânticos globais ou falhas profundas permanecem desafiadores, mas o método ainda oferece ganhos significativos.

5. Significado e Impacto

Este trabalho oferece um caminho escalável para a próxima geração de raciocínio guiado por verificadores. Ao explorar a estrutura intrínseca das mensagens de erro de compiladores, o método:

• Desacopla a complexidade do contexto: Permite que modelos profundos raciocinem sobre correções sem precisar reter todo o histórico de tentativas falhas.
• Democratiza o desempenho: Permite que modelos de tamanho médio (8B-32B) competam com sistemas massivos e caros em tarefas de prova formal complexas.
• Futuro: Abre caminho para sistemas de prova que aprendem a "aprender a corrigir", adaptando-se dinamicamente aos modos de falha específicos de cada problema, sugerindo que a integração de feedback estruturado de compiladores é crucial para o avanço do raciocínio formal em IA.

Em resumo, o artigo demonstra que a "compressão" de informações de falha via compilador é uma alavanca poderosa para transformar a geração de provas de um processo de tentativa e erro cego em um processo de refinamento inteligente e eficiente.