💬 NLP

DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

O artigo apresenta o DRIFT, um novo framework que melhora a formalização automática de teoremas matemáticos por modelos de linguagem ao decompor enunciados informais em subcomponentes para uma recuperação direcionada de premissas e teoremas ilustrativos, resultando em ganhos significativos de desempenho em diversos benchmarks.

Autores originais: Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras

Publicado 2026-04-08

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é um tradutor muito talentoso, capaz de transformar histórias complexas em uma linguagem de computador extremamente rigorosa (como o Lean, usado por matemáticos para provar teoremas sem erros). O problema é que, às vezes, essa história é tão cheia de detalhes e conceitos que o tradutor fica confuso: "O que é isso mesmo? Onde eu encontro a definição oficial disso no dicionário? E como eu uso essa palavra na frase?"

É exatamente para resolver esse caos que os autores criaram o DRIFT.

O nome é um acrônimo para as quatro etapas que o sistema segue: Decompor, Recuperar, Ilustrar e Formalizar. Vamos usar uma analogia de construir uma casa para entender como isso funciona.

O Problema: A Casa sem Planta

Antes do DRIFT, se você pedisse para um tradutor (uma Inteligência Artificial) transformar um teorema matemático em código, era como pedir para alguém construir uma casa complexa apenas olhando para uma foto de um prédio vizinho, sem ter a planta baixa.

A IA tentava adivinhar quais materiais (definições matemáticas) usar.
Ela muitas vezes pegava o material errado ou não sabia como encaixá-lo na estrutura.
O resultado era uma casa que parecia bonita por fora, mas que desmoronava ao ser inspecionada (o código não compilava ou estava logicamente errado).

A Solução: O DRIFT (O Arquiteto Inteligente)

O DRIFT não tenta adivinhar tudo de uma vez. Ele divide o trabalho em quatro passos inteligentes:

1. Decompor (Decompose) – "Quebrando o Projeto em Peças"

Em vez de olhar para a casa inteira de uma vez, o DRIFT pega a descrição do problema e a divide em pequenos blocos de construção.

Analogia: Imagine que você tem uma receita de bolo complexa. Em vez de tentar cozinhar tudo de uma vez, você separa: "preciso de farinha", "preciso de ovos", "preciso de fermento".
Na prática: A IA quebra a frase matemática em perguntas simples. Em vez de perguntar "Como escrevo esse teorema?", ela pergunta: "O que é um número primo?", "O que é uma raiz primitiva?". Isso torna a busca por informações muito mais precisa.

2. Recuperar (Retrieve) – "Ir à Loja de Materiais"

Com essas pequenas perguntas em mãos, o sistema vai até a "loja de materiais" (uma biblioteca gigante de matemática chamada Mathlib) e busca exatamente o que foi pedido.

Analogia: Como você já sabe que precisa de "farinha de trigo" e não apenas "farinha", você vai ao corredor certo e pega o pacote exato. Antes, a IA pegava qualquer pacote de farinha que parecesse parecido, o que estragava o bolo.
Na prática: O sistema encontra as definições formais corretas para cada conceito separado.

3. Ilustrar (Illustrate) – "Mostrar Exemplos de Montagem"

Aqui está o segredo do DRIFT. Só ter o material (a farinha e os ovos) não basta; você precisa saber como usá-los juntos.

Analogia: Imagine que você comprou os tijolos certos, mas nunca viu como eles se encaixam. O DRIFT vai até a biblioteca e pega 3 exemplos de casas prontas que usaram esses mesmos tijolos. Ele mostra: "Veja como o tijolo X foi usado na parede Y nesta casa aqui".
Na prática: O sistema busca teoremas anteriores que usaram as definições encontradas. Isso ensina à IA a sintaxe correta (como escrever o código) e o padrão de uso, evitando erros de formatação.

4. Formalizar (Formalize) – "Construindo a Casa"

Agora, com a lista de materiais exatos (Recuperar) e o manual de montagem visualizado (Ilustrar), a IA finaliza o trabalho.

Analogia: O tradutor pega todas as peças e os exemplos e escreve o código final. Como ele tem as peças certas e sabe como montá-las, a casa fica sólida e segura.
Na prática: A IA gera o teorema formal em Lean, que passa nos testes de verificação do computador.

Por que isso é um grande avanço?

Os testes mostraram que o DRIFT funciona muito melhor do que os métodos antigos, especialmente em problemas difíceis ou em áreas onde a IA nunca treinou antes (como um "oceano desconhecido" de matemática).

Precisão: Ele quase dobrou a pontuação de acerto na busca pelas definições certas.
Adaptabilidade: Funciona bem mesmo quando a IA não "sabe" a resposta de cabeça, porque ela aprende a buscar e usar as informações corretas no momento da prova.

Resumo Final

O DRIFT é como dar a um construtor de IA não apenas os materiais certos, mas também um guia de montagem passo a passo e exemplos visuais de como usar esses materiais. Em vez de tentar adivinhar, ele desmonta o problema, busca as peças certas, olha como outros as usaram e só então constrói a solução. Isso torna a tradução de matemática para código muito mais confiável e inteligente.

Título: DRIFT: Decompor, Recuperar, Ilustrar e, em seguida, Formalizar Teoremas

1. O Problema

A automação da formalização de declarações matemáticas (autoformalização) para provadores de teoremas (como Lean, Isabelle ou Rocq) permanece um desafio significativo para Grandes Modelos de Linguagem (LLMs). Os principais obstáculos identificados são:

Falta de Mapeamento Direto: Declarações informais (em linguagem natural) não possuem mapeamentos diretos para teoremas e lemas específicos em bibliotecas formais (como Mathlib).
Complexidade das Consultas: As declarações informais são frequentemente densas e multifacetadas. Quando usadas diretamente como consultas para recuperação de informações, elas falham em identificar definições atômicas e precisas necessárias para a formalização.
Falta de Contexto de Uso: Mesmo quando as definições formais corretas são recuperadas, os modelos frequentemente não sabem como utilizá-las sintaticamente ou como integrá-las corretamente na estrutura do teorema, levando a erros de sintaxe e semântica.
Limitações de Atualização: Modelos ajustados (fine-tuned) tornam-se obsoletos rapidamente devido às atualizações constantes das bibliotecas formais, resultando em alucinações sobre objetos que foram renomeados ou descontinuados.

2. Metodologia: O Framework DRIFT

O DRIFT é um framework inovador de quatro estágios projetado para superar as limitações dos métodos de recuperação aumentada (RAG) existentes, que tratam consultas como blocos monolíticos. O processo é ilustrado na Figura 1 do artigo:

Estágio 1: Decompor (Decompose)

Objetivo: Quebrar a complexidade da declaração informal.
Mecanismo: Um LLM (Decomposer) analisa a declaração informal e a divide em um conjunto de sub-consultas atômicas e focadas em conceitos.
Detalhe Técnico: Cada sub-consulta ( $q_i$ ) descreve um único conceito matemático em linguagem natural e inclui uma representação formal prevista ( $\hat{l}_i$ ) gerada pelo modelo. Isso serve como uma "âncora" sintática para guiar o recuperador, permitindo que ele aproveite tanto o significado semântico quanto as pistas sintáticas.

Estágio 2: Recuperar (Retrieve)

Objetivo: Identificar premissas dependentes precisas.
Mecanismo: Um recuperador denso (baseado em BGE-M3 e ajustado para a tarefa de recuperação de dependências) busca na biblioteca formal (ex: Mathlib) os objetos que correspondem a cada sub-consulta atômica.
Diferencial: Ao contrário de métodos que recuperam teoremas inteiros baseados em similaridade global, o DRIFT recupera definições atômicas (ex: IsPrimitiveRoot, ZMod) para cada conceito isolado, agregando os resultados e removendo duplicatas.

Estágio 3: Ilustrar (Illustrate)

Objetivo: Fornecer contexto de uso sintático e estrutural.
Mecanismo: O módulo seleciona um pequeno conjunto de teoremas exemplares que utilizam as premissas recuperadas.
Algoritmo: Utiliza um algoritmo ganancioso (greedy) para maximizar a cobertura das premissas recuperadas com um número limitado de teoremas (ex: $m=3$ ).
Importância: Isso preenche a lacuna entre "saber o que é uma definição" e "saber como usá-la na sintaxe Lean", fornecendo padrões de aplicação concretos ao modelo.

Estágio 4: Formalizar Teoremas (Formalize Theorems)

Objetivo: Gerar a declaração formal final.
Mecanismo: Um formalizador (LLM) recebe um prompt concatenado contendo: instruções de formalização, as premissas recuperadas, os teoremas ilustrativos e a declaração informal original.
Resultado: O modelo sintetiza a declaração formal correta (em Lean 4), condicionada a todo o contexto enriquecido.

3. Principais Contribuições

Framework DRIFT: Introdução de uma abordagem de recuperação aumentada guiada por decomposição, que transforma consultas monolíticas em um processo alinhado com a estrutura de dependência da matemática formal.
Recuperação de Dependências Aprimorada: O método supera significativamente as linhas de base atuais (como DPR/RAuto) na precisão da recuperação de premissas, especialmente em cenários fora da distribuição (OOD).
Análise de Limites de Conhecimento: O estudo revela que a eficácia da recuperação depende criticamente do "gap" entre o conhecimento paramétrico do modelo e a complexidade da declaração. Isso destaca a necessidade de estratégias adaptativas que decidam quando recuperar conhecimento externo.
Desempenho SOTA: Estabelecimento de novos estados da arte (SOTA) em benchmarks de autoformalização, demonstrando robustez tanto em modelos de ponta (GPT-4.1, DeepSeek-V3.1) quanto em modelos especializados de código aberto (Goedel-V2-8B).

4. Resultados Experimentais

Os experimentos foram conduzidos em três benchmarks distintos: ProofNet (distribuição interna), MiniF2F-test (problemas autocontidos) e ConNF (fora da distribuição/OOD).

Recuperação de Dependências:
- No ProofNet, o DRIFT dobrou quase o F1-score em comparação com a linha de base DPR (de ~13.77% para ~27.68% com Claude-Opus-4).
- A decomposição permitiu uma recuperação mais precisa de definições atômicas, superando a abordagem de consulta monolítica.
Autoformalização (Correção Semântica - BEq+):
- ConNF (OOD): O DRIFT demonstrou ganhos massivos. Com o GPT-4.1, o BEq+@10 aumentou em 55.57% em relação à linha de base zero-shot, superando inclusive o limite superior aproximado (Oracle) em alguns casos. Isso ocorre porque os teoremas ilustrativos fornecem o contexto de uso que o Oracle (apenas premissas) não oferece.
- ProofNet: Melhoria consistente em todos os modelos, com o GPT-4.1 alcançando 21.93% em BEq+@10 (vs. 19.25% do DPR).
- MiniF2F-test: Em problemas com baixa dependência de bibliotecas, a recuperação pode atuar como ruído. O DRIFT manteve desempenho competitivo, embora a análise de ablação tenha mostrado que, para problemas muito simples, a remoção de contexto pode às vezes melhorar a sintaxe (Typecheck), mas degradar a lógica.
Análise de Ablação:
- Remover o módulo Illustrate causou queda significativa na precisão semântica (BEq+), confirmando que exemplos de uso são cruciais.
- Remover o módulo Decompose (usando a consulta original) reduziu a precisão da recuperação, mas em alguns casos, a recuperação "monolítica" foi menos distrativa em problemas simples. Isso sugere uma sinergia: a decomposição traz precisão, mas exige a ilustração para guiar o modelo através da diversidade de informações recuperadas.

5. Significado e Conclusão

O trabalho DRIFT representa um avanço fundamental na interseção entre LLMs e matemática formal. Ao demonstrar que a decomposição de consultas combinada com contextualização via exemplos de uso supera métodos de recuperação tradicionais, o artigo oferece um novo paradigma para sistemas de provadores de teoremas assistidos por IA.

Generalização: O framework é agnóstico ao modelo e à linguagem, sugerindo aplicabilidade em outros sistemas formais.
Adaptabilidade: A descoberta de que a utilidade da recuperação varia conforme o modelo e a complexidade do problema aponta para o futuro de sistemas agentes adaptativos, que podem decidir dinamicamente se devem ou não recuperar informações externas.
Impacto Prático: A capacidade de superar o Oracle (que tem acesso às dependências verdadeiras, mas não ao contexto de uso) em benchmarks OOD demonstra que a qualidade do contexto (ilustrações) é tão crítica quanto a precisão da recuperação das definições.

Em resumo, o DRIFT não apenas melhora a precisão técnica da formalização, mas também resolve o problema de "como usar" as definições recuperadas, tornando-se uma ferramenta essencial para a próxima geração de assistentes matemáticos automatizados.