💻 computer science

Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation

O artigo apresenta o **Diffusion-Proof**, o primeiro framework para aplicar Grandes Modelos de Linguagem baseados em difusão para a prova formal de teoremas, que supera os baselines autorregressivos tradicionais ao alavancar a denoização iterativa para coerência de longo alcance e correção local, alcançando melhorias significativas em benchmarks e resolvendo um problema da IMO que modelos de última geração não conseguiram resolver.

Autores originais: Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, Tong Zhang

Publicado 2026-06-19

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, Tong Zhang

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

A Grande Ideia: Consertando a "Via de Mão Única" da Matemática de IA

Imagine que você está tentando resolver um quebra-cabeça matemático muito complexo, como uma prova em uma linguagem formal chamada Lean. Essa linguagem é como um código de computador rigoroso, onde cada passo deve ser logicamente perfeito. Se você cometer um único erro minúsculo, toda a prova desmorona.

Durante anos, os melhores modelos de IA para esse trabalho têm sido os modelos Auto-Regressivos (AR). Pense nesses modelos como uma pessoa escrevendo uma história uma palavra de cada vez, estritamente da esquerda para a direita. Eles não conseguem ver o que estão prestos a escrever e não podem facilmente voltar e mudar uma palavra que escreveram cinco minutos atrás sem reescrever a frase inteira.

O Problema:
Em provas matemáticas longas, essa abordagem de "via de mão única" causa dois grandes problemas:

O Efeito Dominó: Se a IA cometer um pequeno erro no início, ela continuará construindo sobre esse erro, tornando o erro cada vez pior até que a prova se torne um lixo.
Sem "Olhar para Trás": Se a IA perceber no meio do caminho que o primeiro passo estava errado, ela não consegue consertar facilmente apenas esse primeiro passo. Ela tem que recomeçar ou tentar, de forma desajeitada, remendar o final da frase para que combine com o início.

A Solução: A Abordagem de "Difusão"

Os autores deste artigo propõem uma nova maneira de construir IA para matemática chamada Diffusion-Proof. Em vez de escrever palavra por palavra, eles usam um Modelo de Linguagem de Grande Escala de Difusão (dLLM).

A Analogia: O Escultor vs. O Copista

O Jeito Antigo (Modelo AR): Imagine um copista escrevendo uma carta. Uma vez que a tinta seca, ele não pode mudá-la. Se ele errar a grafia de uma palavra, tem que riscá-la e escrever uma nota bagunçada ao lado.
O Novo Jeito (Modelo de Difusão): Imagine um escultor trabalhando com um bloco de argila. Eles não apenas adicionam argila; eles começam com um bloco bruto e ruidoso e o refinam iterativamente. Eles podem olhar para a forma inteira de uma vez, suavizar uma saliência no lado esquerdo enquanto olham para a curva no lado direito, e corrigir erros "denoizando" (removendo o ruído) toda a imagem até que ela esteja perfeita.

Em termos técnicos, o modelo de Difusão gera texto em blocos (pedaços de palavras) em vez de palavras individuais. Ele pode olhar para o início e o fim de uma frase simultaneamente para entender o que se encaixa no meio.

Como o Diffusion-Proof Funciona: A Equipe de Dupla

O artigo introduz uma equipe de duas partes para resolver esses problemas matemáticos:

1. O Arquiteto (dLLM-Prover-7B)

Este é o construtor principal. Por usar o método do "escultor" (difusão de blocos), ele é muito melhor em planejamento de longo alcance.

Por que isso importa: Ao construir uma prova longa, o Arquiteto consegue ver o "quadro geral". Ele sabe que o passo final exige uma condição específica, então ele prepara o início da prova para corresponder perfeitamente a essa condição. Ele não se perde no meio porque consegue "ver" todo o bloco de texto de uma só vez.

2. O Inspetor (dLLM-Corrector-7B)

Até o melhor Arquiteto comete erros. Às vezes, a prova parece boa, mas um passo específico está errado.

O Jeito Antigo: Se um modelo AR comete um erro, ele geralmente tenta consertá-lo escrevendo mais texto após o erro, o que geralmente piora as coisas.
O Novo Jeito: O Inspetor é um modelo especial treinado para preencher lacunas. Se a prova falhar, o sistema pega a parte quebrada, cobre-a com uma "máscara" (como um espaço em branco) e pede ao Inspetor para reescrever apamente aquele pedaço específico.
O Superpoder: Como o Inspetor usa o método de difusão, ele pode olhar para o texto antes do erro e o texto depois do erro para descobrir exatamente qual deve ser a peça que falta. É como um editor que lê a frase antes e depois de um erro de digitação para adivinhar a palavra correta, em vez de apenas adivinhar baseando-se na palavra anterior.

Os Resultados: Vencendo os Gigantes

Os pesquisadores testaram este novo sistema em dois benchmarks matemáticos famosos:

MiniF2F: Uma coleção de problemas de matemática de nível de ensino médio e competições.
ProofNet: Uma coleção de problemas de matemática de nível universitário.

O Placar:

O novo sistema Diffusion-Proof venceu os melhores modelos tradicionais (Auto-Regressivos) treinados exatamente com os mesmos dados.
Ele resolveu 6,14% mais problemas no teste MiniF2F.
Ele resolveu 1,61% mais problemas no teste ProofNet.

O Momento "IMO":
O resultado mais emocionante foi um problema específico da Olimpíada Internacional de Matemática (IMO). Um modelo de IA muito avançado e famoso chamado DeepSeek-Prover-V2 (que usa raciocínio de "Cadeia de Pensamento") falhou em resolvê-lo. O Diffusion-Proof resolveu.

Por quê? O modelo DeepSeek ficou preso em um loop tentando consertar seu próprio plano, mas não conseguiu ver a conexão de longo alcance entre o início e o fim da prova. O modelo de Difusão, com sua capacidade de olhar para o "bloco" inteiro da prova de uma só vez, encontrou o caminho correto.

Resumo

O artigo afirma que, ao mudar de "escrever uma palavra por vez" para "esculpir blocos de texto", a IA pode se tornar muito melhor em matemática formal. Isso cria um sistema que planeja melhor a longo prazo e pode consertar seus próprios erros olhando para o contexto completo, não apenas para o passado imediato. Isso permite que resolva problemas matemáticos difíceis que modelos de IA anteriores simplesmente não conseguiam decifrar.

Resumo Técnico: Diffusion-Proof

Declaração do Problema

A prova de teoremas formais exige a manutenção de coerência de longo alcance e consistência lógica através de sequências complexas de passos de raciocínio. Embora os Grandes Modelos de Linguagem (LLMs) tenham avançado significativamente neste domínio, as abordagens de estado da arte atuais dependem fortemente de modelos Auto-Regressivos (AR). Estes modelos geram texto sequencialmente da esquerda para a direita, prevendo o próximo token baseando-se apenas nos tokens anteriores. Esta arquitetura sofre de limitações inerentes, incluindo:

Acumulação de Erros: Pequenos erros em tokens iniciais podem se acumular exponencialmente ao longo de sequências longas, levando a inconsistências lógicas.
Falta de Coerência de Longo Alcance: Modelos AR têm dificuldade em manter um plano global coerente para uma prova, frequentemente falhando em alinhar táticas intermediárias com o objetivo final.
Incapacidade de Realizar In-filling: Modelos AR não conseguem realizar naturalmente correções de "in-filling" (modificar uma seção central de uma prova enquanto preserva o contexto circundante), o que é crucial para corrigir erros locais sem reescrever toda a prova.

Embora os Diffusion LLMs (dLLMs) tenham mostrado promessa em codificação e geração de texto geral ao utilizar denoising iterativo e contexto bidirecional, sua aplicação à prova matemática formal permanece amplamente inexplorada.

Metodologia

Os autores propõem o Diffusion-Proof, o primeiro framework projetado para treinar e aplicar dLLMs especificamente para a prova de teoremas formais. O framework opera dentro do ambiente Lean4 e utiliza uma arquitetura de modelo duplo: dLLM-Prover-7B e dLLM-Corrector-7B.

1. Coleta e Pré-processamento de Dados

Dataset: Os autores coletaram 5,5 milhões de registros de prova de teoremas de trabalhos anteriores.
Limpeza: Eles padronizaram os dados usando métodos baseados em regras para separar declarações de Linguagem Natural (NL), declarações de Linguagem Formal (FL) e provas em FL.
Dataset SFT: 300.000 registros foram selecionados para criar um dataset de Ajuste Fino Supervisionado (SFT), mantendo uma proporção de 1:2 entre provas puras em Lean e aquelas com anotações em NL.
Dados do Corretor: Um subconjunto de dados apresentando decomposição de submetas (marcadas por palavras-chave have) foi processado. Blocos de prova foram preenchidos com tokens de placeholder para criar dados de treinamento para correções de "in-filling".

2. Arquitetura do Modelo e Treinamento

O framework é construído sobre o Fast-dLLM-V2-7B, um modelo de difusão baseado em blocos. Ao contrário dos dLLMs tradicionais que mascaram tokens independentemente, este modelo divide sequências em blocos de tamanho $B$ com atenção bidirecional restrita a blocos individuais, enquanto preserva as relações causais entre os blocos.

dLLM-Prover-7B:
- Objetivo: Realizar a geração de uma prova completa com uso de táticas coerentes de longo alcance.
- Treinamento: Ajustado via SFT no dataset de 300k utilizando um framework padrão de texto-para-texto.
- Estratégia: Emprega aprendizado por currículo, organizando os dados de treinamento por complexidade de prova (aumentando o comprimento da prova) para estabilizar a curva de perda. O tamanho do bloco de difusão é definido como 32.
dLLM-Corrector-7B:
- Objetivo: Realizar correção local de provas usando informação bidirecional.
- Treinamento: Ajustado via SFT no dataset de decomposição de submetas de 128k.
- Inovação: Introduz um método de Correção de Grande Bloco (Large Block Correction). O tamanho do bloco de difusão é estendido de 32 para 512. O modelo é treinado para substituir provas de submetas errôneas por uma sequência de tokens de máscara e, em seguida, regenerar o bloco usando o contexto estendido (prefixo e sufixo) para realizar correções de in-filling.

3. Pipeline de Inferência

Geração: O dLLM-Prover-7B gera uma prova completa para uma determinada declaração de teorema usando geração por difusão de blocos.
Verificação: A prova é verificada pelo Lean.
Correção: Se a prova falhar na verificação, mas o esqueleto de alto nível (declarações de submetas) estiver correto, o dLLM-Corrector-7B é invocado. Ele substitui as provas de submetas errôneas por tokens de máscara e as regenera usando um bloco de difusão de 512 tokens, aproveitando o contexto bidirecional para corrigir erros locais enquanto mantém a coerência global.

Principais Contribuições

Primeiro Framework dLLM para Prova de Teoremas: O Diffusion-Proof é o primeiro framework que adapta modelos de difusão para a prova de teoremas formais, abordando os desafios específicos de coerência de longo alcance e correção de erros no raciocínio matemático.
Treinamento de Correção de Grande Bloco: Os autores introduzem um novo método de treinamento que utiliza grandes blocos de difusão (512 tokens) e informação bidirecional para permitir correções de in-filling eficazes, uma capacidade nativa de modelos de difusão, mas ausente em modelos AR.
Sinergia de Modelo Duplo: O framework demonstra uma abordagem sinérgica onde um provedor lida com o planejamento global e um corretor lida com o refinamento local, superando baselines de modelo único.

Resultados Experimentais

O framework foi avaliado no MiniF2F-Test (244 problemas) e ProofNet-Test (186 problemas) usando a métrica pass@32.

Ganhos de Desempenho: Comparado a um modelo AR baseline (Qwen-2.5-Lean-SFT-7B) treinado no exato mesmo dataset:
- MiniF2F-Test: O Diffusion-Proof alcançou 50,00% de acurácia, um aumento absoluto de 6,14% sobre o baseline (43,85%).
- ProofNet-Test: O Diffusion-Proof alcançou 7,53% de acurácia, um aumento absoluto de 1,61% sobre o baseline (5,91%).
Análise de Tipo de Problema: O modelo mostrou ganhos significativos em categorias desafiadoras, particularmente em problemas de IMO (Olimpíada Internacional de Matemática), onde melhorou de 5,00% para 15,00%.
Estudo de Caso: Notavelmente, o Diffusion-Proof resolveu com sucesso o problema de IMO imo_1962_p2, que o mais avançado DeepSeek-Prover-V2-7B (equipado com raciocínio de Cadeia de Pensamento Longa - CoT) não conseguiu resolver sob pass@32. A análise indicou que o modelo AR teve dificuldades com as dependências de longo alcance e o planejamento coerente de táticas exigidos, enquanto o corretor de difusão utilizou com sucesso o contexto bidirecional para resolver a prova.
Estudos de Ablação:
- Remover o corretor reduziu o desempenho em 1,64% no MiniF2F, confirmando o valor da etapa de correção.
- Mesmo sem o corretor, o dLLM-Prover sozinho superou o baseline AR em 4,51%, validando as vantagens inerentes da arquitetura de difusão para o raciocínio formal.

Significância e Alegações

O artigo afirma que o Diffusion-Proof destaca as vantagens únicas dos modelos de difusão na prova de teoremas formais, especificamente sua capacidade de manter a coerência de longo alcance e realizar correções de in-filling bidirecionais.

Vantagem Arquitetural: Os resultados sugerem que o paradigma de geração por difusão oferece uma vantagem estrutural sobre modelos AR para tarefas que exigem consistência lógica rigorosa em sequências longas, como evidenciado pelas distribuições de perda de validação mais baixas e taxas de sucesso mais altas em provas complexas.
Potencial Futuro: Os autores posicionam este trabalho como um passo fundamental, demonstrando que dLLMs podem superar baselines AR mesmo sem Aprendizado por Reforço (RL) ou CoT Longa. Eles observam que, embora as limitações atuais incluam escala computacional e a falta de integração com RL, o framework fornece uma direção promissora para pesquisas futuras em modelos com capacidades de raciocínio aprimoradas.

Os autores enfatizam que seu objetivo principal era investigar o potencial arquitetural dos dLLMs, em vez de alcançar o estado da arte através de escalonamento massivo ou RL, tornando as melhorias observadas um forte indicador da eficácia do paradigma de difusão no raciocínio formal.