Resumo Técnico: ImProver 2

Declaração do Problema

A rápida expansão de bibliotecas de matemática formal (por exemplo, Mathlib do Lean) criou um duplo desafio: a manutenibilidade dessas bibliotecas é ameaçada por estilos de prova heterogêneos e baixa modularidade, enquanto a qualidade dos dados de treinamento para provadores de teoremas neurais é degradada por provas que estão corretas, mas estruturalmente subótimas. Os métodos existentes de otimização automática de provas enfrentam obstáculos significativos, incluindo objetivos heterogêneos e definidos heurísticamente, escassez de dados de otimização de alta qualidade e custos proibitivos de treinamento e inferência para modelos em larga escala. Além disso, trabalhos anteriores frequentemente dependiam de modelos de propósito geral de código fechado ou focavam estreitamente em contagens de tokens, falhando em abordar métricas estruturais mais amplas, como modularidade e gerenciamento de dependências.

Metodologia

Os autores introduzem o ImProver 2, um framework neurosimbólico projetado para melhorar iterativamente e de forma autônoma modelos de linguagem pequenos (SLMs) para otimização de provas em Lean 4. O sistema opera por meio de um pipeline de múltiplos componentes:

1. Augmentação Neurosimbólica (Andaime)

Para preencher a lacuna entre o raciocínio informal e a verificação formal, o framework expõe o modelo a um contexto rico do ambiente Lean. Este "andaime" ($\Psi$) inclui:

• Fatias de Contexto: Definições, teoremas e lemas relevantes referenciados diretamente pela prova-alvo, serializados com metadados.
• Cadeia de Estados (CoS): Rastros explícitos dos estados de objetivo antes e após cada passo de tática, intercalados como comentários para revelar o fluxo lógico da prova.
• Auto-informalização: Resumos em linguagem natural dos passos da prova, gerados traduzindo a prova formal em uma sequência de descrições de alto nível.

2. Métricas de Otimização

O sistema visa três objetivos estruturais distintos, definidos como funções computáveis $\mu$:

• Comprimento: Minimizar o número de táticas utilizadas ("golfagem" de provas).
• Dependências: Minimizar a contagem de lemas externos únicos nomeados explicitamente na prova, incentivando provas autocontidas.
• Modularidade: Maximizar o número de "objetivos gerados efetivamente" (subprovas independentes introduzidas via have, calc, etc.), que serve como um proxy para decomposição de prova e manutenibilidade.

3. Pipeline de Otimização Iterativa de Preferência (IRPO)

O ImProver 2 emprega um loop de treinamento iterativo para inicializar SLMs:

1. Geração: O modelo atual $G_t$ gera $n$ reescritas candidatas para cada teorema no conjunto de treinamento, utilizando o andaime neurosimbólico.
2. Filtragem e Replay: Os candidatos são pontuados com base na correção (verificação pelo núcleo Lean) e na melhoria da métrica. Um buffer de replay é usado para equilibrar dados recém-gerados com dados históricos, prevenindo o colapso do modelo e garantindo melhoria monótona. Problemas triviais ou de baixa qualidade são filtrados.
3. Construção de Pares de Preferência: O conjunto de dados é partitionado em "vencedores" (provas que compilam e apresentam alta melhoria) e "perdedores" (falhas ou provas de baixa melhoria). Dois tipos de pares de preferência são formados: vencedor–vencedor (ordenados pela magnitude da melhoria) e vencedor–perdedor.
4. Treinamento: O modelo é atualizado usando Otimização Iterativa de Preferência de Raciocínio (IRPO), que combina uma perda de Otimização Direta de Preferência (DPO) com uma perda de verossimilhança negativa (NLL) nas provas vencedoras. Este processo se repete até a convergência ou esgotamento do orçamento.

Contribuições Principais

1. SLMs de Auto-aperfeiçoamento para Refatoração: O artigo demonstra que a otimização iterativa de preferência pode efetivamente inicializar modelos de linguagem pequenos (especificamente um modelo de 7 bilhões de parâmetros) para otimizar provas em bibliotecas de pesquisa especializadas, tornando-os competitivos com modelos significativamente maiores.
2. Métricas de Otimização Estrutural: Além da simples redução de comprimento, os autores introduzem e avaliam métricas de modularidade e dependência. Essas métricas aproveitam a estrutura da prova e o contexto da biblioteca para atingir objetivos de refatoração distintos relevantes para a manutenibilidade da biblioteca.
3. Augmentação Neurosimbólica: O framework extrai e integra rastros de estado de objetivo, contexto relevante e auto-informalizações. Os autores mostram que essa augmentação aumenta significativamente o desempenho tanto para modelos pequenos quanto para modelos de fronteira, facilitando a descoberta de reescritas válidas e de alto valor.

Resultados Experimentais

O sistema foi avaliado no miniCTX-v2, um benchmark de matemática de nível de pesquisa escrita por humanos, usando um modelo base de 7 bilhões de parâmetros (DeepSeek-R1-Distill-Qwen-7B).

• Desempenho vs. Escala: O ImProver 2 supera o modelo DeepSeek-R1 671B, muito maior, em todas as três métricas (Comprimento, Modularidade, Dependência) quando não andaimeado. Por exemplo, na modularidade, o ImProver 2 alcançou uma melhoria média de 0,143 comparado a 0,055 para o modelo de 671B.
• Comparação com Modelos de Fronteira: O modelo ImProver 2 de 7B é competitivo com modelos de fronteira de nível médio (por exemplo, GPT-5-mini) nas métricas de comprimento e dependência. Ele lidera todos os sistemas não andaimeados avaliados em modularidade.
• Impacto do Andaime: Adicionar o andaime neurosimbólico melhora significativamente o desempenho em todas as famílias de modelos. Por exemplo, a pontuação de melhoria de comprimento do modelo de 7B subiu de 0,118 (base) para 0,236 (andaimeado). Até mesmo modelos grandes como o GPT-5-high viram ganhos substanciais (de 0,660 para 0,875) com o andaime.
• Dinâmica de Iteração: A maioria dos ganhos de desempenho ocorre dentro das primeiras 2–3 iterações do IRPO. O sistema mostra que modelos pequenos podem aprender a reestruturar provas de nível de pesquisa de forma eficaz, embora o desempenho eventualmente se estabilize à medida que o modelo absorve padrões comuns de refatoração.
• Compensações de Precisão: O artigo nota uma compensação entre otimização e precisão de compilação. Embora provas otimizadas frequentemente resultem em maiores melhorias de métrica, elas podem ter taxas de compilação ligeiramente menores do que reescritas conservadoras, refletindo a natureza mais arriscada das transformações estruturais.

Significado e Alegações

O artigo postula que a otimização de provas não é exclusivamente uma função da escala do modelo, mas é significativamente impulsionada por especialização específica da tarefa e auto-aperfeiçoamento iterativo. Ao combinar um pipeline de otimização de preferência com buffer de replay e andaimes neurosimbólicos, o ImProver 2 estabelece que modelos pequenos e acessíveis podem efetivamente reestruturar provas complexas de nível de pesquisa.

Os autores afirmam que seu trabalho estabelece a otimização de provas como uma tarefa escalável e aprendível. Eles argumentam que sua abordagem atende à necessidade crítica de manter bibliotecas formais e melhorar a qualidade dos dados de treinamento para provadores futuros, oferecendo um caminho para automatizar a refatoração de provas para manutenibilidade sem depender exclusivamente de modelos de fronteira massivos e caros. O trabalho destaca que, com andaimes e treinamento adequados, modelos pequenos podem igualar ou superar o desempenho de sistemas substancialmente maiores em objetivos estruturais específicos.