Resumo Técnico: Refatoração Lean

Declaração do Problema

Modelos de Linguagem de Grande Escala (LLMs) treinados com aprendizado por reforço (RL) para prova formal de teoremas em Lean frequentemente geram provas que são corretas, mas notoriamente verbosas, frágeis e computacionalmente caras. Embora esforços de refatoração existentes estejam disponíveis, eles enfrentam três limitações fundamentais ao serem aplicados ao ecossistema Lean:

1. Tensão Multiobjetivo: A refatoração em Lean é inerentemente multiobjetivo. A otimização do comprimento da prova frequentemente entra em conflito com a minimização do custo de compilação (por exemplo, provas mais curtas podem invocar táticas pesadas que inflacionam o tempo de compilação), e os métodos existentes carecem de mecanismos principiais para equilibrar essas compensações ou adaptar-se a objetivos de usuário não vistos no momento da inferência.
2. Fragilidade de Versão: Lean e sua biblioteca padrão, Mathlib, evoluem em uma base quase semanal com mudanças frequentes de API e renomeações de lemas. LLMs de fronteira possuem cortes de conhecimento estáticos, levando a alucinações de táticas obsoletas e incompatibilidade com as ferramentas atuais.
3. Escassez de Dados: Ao contrário das linguagens de programação mainstream, Lean carece de conjuntos de dados emparelhados em grande escala (pares de código ruidoso-limpado) necessários para pipelines de refatoração baseados em treinamento. Além disso, abordagens baseadas em treinamento exigem ajuste fino repetido para cada novo lançamento de LLM, falhando em escalar com a rotatividade de modelos ou o ciclo de lançamento do Lean.

Metodologia: Lean Refactor

Os autores propõem o Lean Refactor, um framework agente de recuperação aumentada plug-and-play projetado para refatorar provas Lean sem ajustar finamente o LLM subjacente. O sistema desacopla a lógica de refatoração do modelo ao externalizar o conhecimento em um banco de dados estruturado e densamente anotado.

1. Banco de Estratégias Densamente Anotado

O núcleo do framework é um banco de dados curado de 9.237 estratégias de refatoração únicas destiladas de mais de 200.000 pares de provas longas-curtas.

• Estrutura: Cada estratégia inclui um título, descrição, pré-condição ("quando aplicar"), guia de aplicação passo a passo e exemplos abstratos antes/depois.
• Metadados: Crucialmente, cada estratégia é anotada com metadados que o LLM não pode inferir a partir de dados de treinamento:
  • Redução do Tempo de Compilação: A aceleração relativa mediana observada ao aplicar a estratégia.
  • Compatibilidade de Versão: Um conjunto de ferramentas Lean/Mathlib validadas (por exemplo, v4.14.0, v4.16.0, v4.22.0) sob as quais a prova refatorada compila com sucesso. Isso é determinado recompilando provas encurtadas em múltiplas versões.

2. Recuperação e Reordenamento Multiobjetivo

Na inferência, o framework emprega um pipeline de recuperação que se adapta a objetivos especificados pelo usuário sem retreinamento do modelo:

• Prova Mais Curta: Recupera estratégias baseadas puramente na similaridade semântica (similaridade de cosseno) ao segmento da prova.
• Consciente do Tempo de Compilação: Recupera um amplo conjunto de candidatos semanticamente similares e depois reordena-os com base nos metadados anotados de redução de custo de compilação.
• Específico de Versão: Filtra o conjunto de candidatos para incluir apenas estratégias cujos metadados de compatibilidade incluam a versão alvo do Lean do usuário.

3. Loop Agente

O framework envolve esses componentes em um loop de agente agnóstico ao modelo consistindo de:

• Planejador: Decompõe a tarefa de refatoração em etapas específicas com base nas estratégias recuperadas.
• Refatorador: Executa o plano para gerar uma prova mais curta.
• Depurador: Usa feedback do compilador para corrigir erros em um loop fechado (até $D$ rodadas).
• Agnosticismo da Base: O planejador, o refatorador e o depurador podem ser instanciados por qualquer LLM de fronteira congelado (por exemplo, Gemini, Claude, série GPT), permitindo que o sistema se transfira entre modelos sem retreinamento.

Contribuições Principais

1. Lançamento de Conjunto de Dados: Os autores lançam o maior conjunto de dados de refatoração Lean até a data, compreendendo mais de 200 mil pares de provas longas-curtas e 9 mil estratégias de refatoração, cada uma anotada com custo de compilação e compatibilidade de versão.
2. Desempenho: O Lean Refactor alcança >70% de compressão em nível de token em benchmarks de competição (miniF2F, PutnamBench) e >20% em repositórios de pesquisa (Analysis, FLT, PhysLean). Também reduz o tempo de compilação em até 60% em benchmarks de competição.
3. Controlabilidade e Robustez: O sistema suporta controle multiobjetivo (comprimento vs. velocidade vs. compatibilidade) via regras de recuperação em vez de pesos do modelo. Provas refatoradas exibem transferência zero-shot mais forte para futuras versões do Lean em comparação com contrapartes não refatoradas e métodos de otimização anteriores.
4. Agnosticismo de Modelo: O framework melhora o desempenho em diferentes bases de LLM (Gemini 3 Flash, Claude Haiku 4.5) e supera agentes de codificação de propósito geral como o Claude Code, mesmo quando este último tem acesso à mesma ferramenta de recuperação de estratégias.

Resultados Experimentais

• Redução de Comprimento: Em benchmarks de competição, o Lean Refactor supera o estado da arte anterior, ProofOptimizer, alcançando 88,40% de redução no miniF2F e 70,38% no PutnamBench (vs. 57,20% para o ProofOptimizer). Em provas de nível de pesquisa, alcança uma redução média de 20–33%, superando significativamente as linhas de base de ablação.
• Tempo de Compilação: Ao reordenar estratégias com base em metadados de custo de compilação, o framework alcança uma redução relativa de 42,62% no tempo de compilação no PutnamBench, comparado a 37,11% para a abordagem padrão de recuperação.
• Compatibilidade de Versão: Ao mirar versões específicas do Lean (por exemplo, v4.16.0), a recuperação filtrada por versão produz consistentemente melhor redução de comprimento do que a recuperação não filtrada. Provas refatoradas mantêm a capacidade de verificação de tipo em mais futuras versões do Lean (até v4.29.0) do que aquelas produzidas pelo ProofOptimizer ou provas verbosas originais.
• Redução de Dependências: As provas refatoradas reduzem dependências externas e intra-projeto em 42–67% dos casos, indicando simplificação lógica genuína em vez de mera transferência para lemas pesados de bibliotecas.

Significado

O artigo argumenta que o Lean Refactor aborda os gargalos críticos da manutenção de bibliotecas matemáticas formais: a tensão entre concisão da prova e eficiência de compilação, e a fragilidade do código em ferramentas em rápida evolução. Ao externalizar o conhecimento de refatoração em um banco de estratégias rico em metadados, o framework permite otimização multiobjetivo controlável sem a necessidade de ajuste fino de modelo caro. Essa abordagem permite que o sistema permaneça robusto contra a deriva de versão do Lean/Mathlib e adaptável a novas bases de LLM imediatamente, estabelecendo as bases para provas formais mais mantíveis e resilientes a versões.