Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees

1. O Problema

A autoformalização de enunciados é a tarefa de traduzir automaticamente problemas matemáticos escritos em linguagem natural (NL) para linguagens formais (FL) utilizadas por provadores de teoremas interativos (ITPs), como o Lean 4.

Apesar dos avanços recentes em Grandes Modelos de Linguagem (LLMs), as abordagens atuais tratam a formalização como uma tarefa de geração de sequência monolítica e plana (end-to-end). Isso ignora a estrutura hierárquica e lógica intrínseca das declarações matemáticas. Ao tratar o código formal apenas como uma string plana, os modelos frequentemente falham em capturar precedência de operadores, escopos lógicos aninhados e dependências semânticas, resultando em erros de sintaxe e, mais criticamente, em inconsistências semânticas (o código compila, mas não representa a matemática correta). Além disso, a correção de erros (reparo) costuma ser feita no nível de todo o enunciado, o que é ineficiente e pode corromper partes corretas do código.

2. Metodologia: O Framework DSR

Os autores propõem o DSR (Decompose, Structure, and Repair), um framework neuro-simbólico que reestrutura o processo de autoformalização em um pipeline modular de três etapas:

A. Decompor (Decompose)

O enunciado em linguagem natural é decomposto em componentes lógicos distintos antes da tradução:

1. Canonização Semântica: Remove ruído linguístico e explicita contextos implícitos (como tipos de variáveis) necessários para a formalização rigorosa.
2. Alinhamento de Papel Estrutural: Segmenta o enunciado em Condições (premissas/hipóteses) e Conclusão (o objetivo a ser provado). Isso garante que o modelo entenda a estrutura lógica (ex: "Se A e B, então C") antes de gerar o código.

B. Estruturar (Structure)

Em vez de gerar apenas o código Lean, o modelo gera simultaneamente:

1. Componentes FL: Fragmentos de código linear correspondentes às condições e conclusão.
2. Árvores de Operadores (OPTs - Operator Trees): Uma representação hierárquica da estrutura lógica do código.
   • Motivação Teórica: A OPT atua como uma "âncora semântica", forçando o modelo a modelar explicitamente a topologia recursiva e a precedência dos operadores, em vez de depender apenas de correlações estatísticas lineares.
   • Motivação Prática: A OPT serve como um "plano topológico" para a etapa de reparo, permitindo localizar erros com precisão cirúrgica em sub-árvores específicas.

O treinamento utiliza Aprendizado de Currículo (Curriculum Learning), onde o modelo é treinado progressivamente: primeiro em componentes atômicos simples, depois em componentes moderados e, finalmente, em estruturas complexas, misturando dados de diferentes níveis de dificuldade para evitar o esquecimento catastrófico.

C. Reparar (Repair)

Após a geração inicial, o código é compilado. Se houver erros, o framework utiliza uma estratégia de Reparo Guiado por Árvore:

1. Montagem Estrutural: O código é reconstruído priorizando a estrutura da OPT para evitar erros de sintaxe comuns (como parênteses desbalanceados).
2. Localização Hierárquica: Se a compilação falhar, a mensagem de erro é mapeada para um nó específico na árvore de operadores.
3. Reparo Cirúrgico: O modelo tenta corrigir o erro em três níveis de granularidade, do mais específico ao mais geral:
   • Nível de Subcomponente: Corrige apenas o sub-árvore afetada.
   • Nível de Componente: Se falhar, reescreve o componente inteiro (condição ou conclusão).
   • Nível de Enunciado: Última tentativa, reescrevendo todo o teorema.
     Essa abordagem evita reescrever partes corretas do código, preservando a integridade semântica global.

3. Contribuições Principais

1. Framework DSR: Uma nova arquitetura neuro-simbólica que desacopla a tradução em decomposição, estruturação (via OPTs) e reparo guiado, superando a abordagem "caixa preta" end-to-end.
2. Benchmarck PRIME: Introdução de um novo conjunto de dados de avaliação contendo 156 teoremas de nível universitário e de pós-graduação, extraídos de livros-texto canônicos e formalizados manualmente por especialistas em Lean 4. O PRIME cobre Álgebra, Análise e Teoria dos Números, preenchendo uma lacuna em benchmarks existentes focados em problemas mais simples.
3. Novo Estado da Arte (SOTA): Demonstração de que a incorporação de supervisão estrutural (OPTs) e aprendizado de currículo é essencial para lidar com a complexidade da matemática avançada.

4. Resultados Experimentais

Os resultados foram avaliados em três benchmarks: ProverBench (problemas introdutórios), ProofNet (nível de graduação) e PRIME (nível de pós-graduação).

• Desempenho Geral: O DSR estabeleceu o novo estado da arte em todos os benchmarks, superando modelos base (como Kimina, StepFun, Goedel-V2 e Qwen3-Max) tanto em Taxa de Sucesso de Verificação de Sintaxe (SC) quanto em Taxa de Sucesso de Verificação de Consistência (CC).
  • No benchmark PRIME, o DSR alcançou 67,95% de CC, superando o segundo melhor (Goedel-V2-32B) em 1,28 pontos percentuais.
  • No ProofNet, alcançou 79,51% de CC, com uma margem de +8,62% sobre o segundo melhor.
• Robustez em Teoremas Complexos: A vantagem do DSR aumentou conforme a complexidade dos teoremas cresceu, indicando que a decomposição e a estrutura hierárquica são cruciais para a matemática avançada.
• Fidelidade Semântica: O DSR apresentou a menor queda entre a taxa de sintaxe e a de consistência, provando que a estrutura OPT ajuda a gerar código que não apenas compila, mas também reflete corretamente a lógica natural.
• Estudos de Ablação:
  • A adição de árvores de operadores sem aprendizado de currículo causou estagnação em benchmarks difíceis (PRIME), confirmando que a estrutura complexa exige um treinamento progressivo.
  • A estratégia de reparo guiado por árvore superou significativamente o reparo no nível de enunciado (global), pois evita a introdução de novos erros ao alterar partes corretas do código.

5. Significância e Impacto

Este trabalho representa um avanço fundamental na área de autoformalização ao demonstrar que incorporar representações estruturadas explícitas (neuro-simbólicas) é superior à geração puramente sequencial para tarefas de raciocínio matemático complexo.

• Para a Comunidade de IA: Oferece um novo paradigma para tarefas de tradução de alto risco onde a precisão semântica é crítica, mostrando que a decomposição modular e o reparo hierárquico são estratégias eficazes.
• Para a Matemática Formal: O benchmark PRIME fornece um recurso valioso e rigoroso para avaliar futuros modelos, elevando o padrão de avaliação para além de problemas de nível de ensino médio.
• Aplicabilidade: O framework DSR pode ser adaptado para outras linguagens formais e tem potencial para estender a autoformalização de enunciados para a geração de provas completas, facilitando a verificação formal de grandes corpos de conhecimento matemático.

Em resumo, o DSR não apenas melhora as métricas de desempenho, mas resolve um problema fundamental de arquitetura: como alinhar a natureza hierárquica da matemática com a natureza sequencial dos modelos de linguagem.