🤖 AI

Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

Goedel-Architect é um framework agêntico para prova de teoremas em Lean 4 que utiliza uma estratégia de geração e refinamento de blueprints para alcançar um desempenho de estado da arte em benchmarks matemáticos desafiadores como MiniF2F, Putnam e IMO com custos significativamente menores do que pipelines existentes.

Autores originais: Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fo

Publicado 2026-06-05

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fowl, Sanjeev Arora

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ê está tentando construir um castelo massivo e intrincado feito de peças de LEGO. Você tem um projeto, mas não é um desenho; é uma lista de instruções que diz: "Para construir a torre, primeiro você precisa de uma fundação, depois de uma parede, depois de uma janela".

O problema é que, se você tentar construir a torre inteira em um único salto gigante, pode ficar travado, ou pode perceber no meio do caminho que a fundação foi construída errada.

Goedel-Architect é uma nova e inteligente equipe de robôs projetada para construir esses "castelos" matemáticos (provas formais) em uma linguagem chamada Lean 4. Em vez de tentar construir todo o castelo de uma só vez, ela utiliza uma estratégia chamada Geração e Refinamento de Projetos (Blueprint Generation and Refinement).

Veja como funciona, dividido em etapas simples:

1. O Projeto (O Plano Mestre)

Antes de o robô começar a construir, ele desenha um Projeto (Blueprint).

O que é? Pense nisso como um mapa de dependências. Ele lista cada pequeno passo (chamado de "lema") necessário para provar o grande problema matemático.
Como funciona: Ele desenha setas mostrando quais passos dependem de outros. Por exemplo: "Você não pode construir o telhado até que as paredes estejam prontas".
A Reviravolta: Às vezes, se o problema matemático for muito difícil, o robô recebe uma Prova em Linguagem Natural. Isso é como um matemático humano dando ao robô um esboço bruto ou uma história sobre como resolver o problema. O robô usa essa história para desenhar um projeto melhor e mais preciso desde o início.

2. A Equipe de Construção (Prova em Paralelo)

Uma vez que o projeto esteja pronto, o robô não constrói um passo de cada vez. Ele envia uma equipe inteira de construtores especializados (um "provador Lean") para trabalhar em todos os pequenos passos ao mesmo tempo.

Cada construtor olha apenas para seu passo específico e para os passos que ele tem permissão para usar (suas "dependências").
Eles tentam construir sua parte. Se tiverem sucesso, tornam essa parte do projeto Verde.
Se falharem, tornam-na Azul (travado) ou Vermelha (quebrado).

3. O Ciclo de Conserto (Refinamento)

É aqui que o Goedel-Architect se diferencia de outros robôs.

O Jeito Antigo: Muitos outros sistemas de IA tentam resolver um problema, ficam travados e então tentam quebrar aquela única peça travada em partes menores repetidamente. Isso é como tentar consertar uma parede quebrada apenas martelando com mais força no mesmo lugar. Frequentamente, isso leva a um beco sem saída.
O Jeito Goedel: Se um construtor ficar travado, toda a equipe para e olha para o projeto inteiro.
- Diagnóstico: O robô pergunta: "Por que isso falhou?"
  - Caso A (Vermelho): "Ah, este passo é na verdade falso!" (O projeto tinha uma ideia errada). O robô corrige a afirmação.
  - Caso B (Azul): "Este passo é verdadeiro, mas é difícil demais para construir agora." O robô divide este passo grande em dois ou três passos auxiliares menores e mais fáceis.
- Revisão: O robô reescreve o projeto com esses novos passos menores e envia a equipe novamente.
- Eficiência: Crucialmente, qualquer parte do castelo que já foi construída com sucesso (Verde) permanece Verde. O robô não joga fora o trabalho bom; ele apenas conserta as partes quebradas e adiciona novos passos auxiliares.

Por que isso é importante?

O artigo afirma que esta abordagem é um "divisor de águas" por dois motivos principais:

É incrivelmente inteligente e precisa:
- Em um teste padrão de problemas matemáticos do ensino médio (MiniF2F), resolveu 99,2% deles. Com um pouco de ajuda de uma história em linguagem natural, resolveu 100%.
- Em matemática de nível universitário mais difícil (PutnamBench), resolveu 75,6% por conta própria e 88,8% com um pouco de ajuda.
- Conseguiu até resolver problemas de competições muito recentes e super difíceis (como IMO 2025 e Putnam 2025) que nenhum outro robô de código aberto resolveu antes.
É incrivelmente barato:
- Outros robôs de alto nível que resolvem esses problemas frequentemente utilizam modelos de "caixa preta" que custam milhares de dólares para rodar.
- O Goedel-Architect utiliza um cérebro de código aberto mais barato (DeepSeek-V4-Flash).
- O Custo: Para resolver todo o teste PutnamBench, o Goedel-Architect custou cerca de US$ 294. O próximo melhor competidor de código aberto custou cerca de US$ 163.000. Isso representa uma economia de 500x.

A Conclusão

O Goedel-Architect é como um mestre arquiteto que não tenta apenas martelar um prego; ele desenha um mapa, envia uma equipe para construir em paralelo e, quando algo quebra, ele redesenha todo o mapa para corrigir a lógica, mantendo as partes boas e alterando apenas o que é necessário. Ele prova que você não precisa do IA mais caro e secreto para resolver os problemas matemáticos mais difíceis; você só precisa de uma maneira mais inteligente de organizar o trabalho.

Resumo Técnico: Goedel-Architect

Declaração do Problema

O artigo aborda o desafio da prova formal de teoremas em Lean 4, visando especificamente preencher a lacuna entre sistemas proprietários de alto desempenho e pipelines de código aberto acessíveis. Embora os sistemas de IA de fronteira tenham demonstrado capacidades matemáticas significativas (ex: medalhas de ouro no IMO, resolução de problemas abertos de Erdős), a verificação dessas provas requer formalização rigorosa. As soluções de pesos abertos existentes frequentemente lutam com benchmarks difíceis como o PutnamBench (pontuando <15%), enquanto sistemas de alto desempenho dependem de modelos não lançados ou APIs proprietárias caras (custando milhares de dólares por execução de benchmark). A dificuldade central reside em decompor eficientemente teoremas complexos em lemas prováveis sem ficar preso em becos sem saída recursivos ou incorrer em custos computacionais proibitivos.

Metodologia

Goedel-Architect é um framework agêntico centrado na geração e refinamento de blueprints (projetos). Diferente de abordagens que dependem de decomposição recursiva descendente ou geração de prova em uma única etapa, este sistema opera sobre um grafo de dependência global.

1. Geração de Blueprint

O processo começa com a geração de um blueprint, definido como um grafo de dependência de definições e lemas formulados formalmente que constroem até o teorema alvo.

Estrutura: O teorema alvo é o sumidouro único do grafo. Cada nó representa uma definição ou lema, e as arestas representam dependências declaradas (ou seja, quais lemas a prova tem permissão para utilizar).
Entrada: A declaração formal do teorema sempre inicia a geração. Opcionalmente, uma prova em linguagem natural (gerada por um modelo mais forte ou fornecida como solução) pode atuar como um guia estrutural para problemas difíceis.
Validação: O gerador itera contra o compilador Lean para garantir que o arquivo emitido faça o parse, que todos os nós sejam bem tipados e que o grafo seja acíclico e conectado.

2. Prova de Teoremas em Paralelo

Uma vez que o blueprint inicial ( $G_0$ ) é gerado, o sistema despacha cada nó de lema para um provador Lean equipado com ferramentas em paralelo.

Contexto: O provador de um lema específico vê apenas o próprio lema e suas dependências declaradas (disponíveis como fatos), não o grafo inteiro.
Ferramentas: O provador utiliza o compilador Lean para verificação de tipos e um serviço de recuperação de Mathlib para busca de lemas.
Diagnóstico: Se um lema falha, o provador retorna um diagnóstico estruturado. Isso inclui:
- Negação: Se o provador encontrar um contraexemplo, ele registra uma prova da afirmação negada.
- Análise de Lacunas: Se o lema não for provado, mas acredita-se que seja verdadeiro, o provador identifica onde a cadeia de prova se quebra.

3. Refinamento de Blueprint

Se algum lema permanecer não provado, um modelo de refinamento reescreve o blueprint global ( $G_{k+1}$ ) com base nos sinais de falha.

Estratégias: O refinamento inclui a decomposição de lemas difíceis em lemas auxiliares, o reajuste de dependências para conceder acesso a resultados necessários, ou a alteração/remoção de afirmações que o provador provou serem falsas.
Preservação: Lemas comprovados com sucesso do ciclo anterior são preservados (nós verdes) com suas assinaturas intactas, garantindo que o esforço computacional não seja descartado.
Iteração: O blueprint revisado é novamente provado em paralelo. Este loop continua até que todos os nós sejam resolvidos ou que o orçamento de iteração seja esgotado.

Principais Contribuições

Arquitetura Centrada em Blueprint: O artigo introduz uma abordagem de grafo de dependência global que contrasta com a decomposição recursiva. Isso permite que tentativas de prova paralelas compartilhem contexto e possibilita que o refinamento atue sobre toda a estratégia simultaneamente, em vez de apenas localmente.
Estado da Arte de Pesos Abertos: O sistema atinge o estado da arte em desempenho utilizando o backbone de pesos abertos DeepSeek-V4-Flash (284B-A13B), evitando a necessidade de modelos não lançados ou modelos proprietários de fronteira.
Eficiência de Custo: O pipeline é significativamente mais econômico que sistemas comparáveis de alto desempenho. O artigo reporta um custo por problema de ~$0,44, o que é até 500 vezes menor que outros pipelines de código aberto e ordens de magnitude mais barato que alternativas proprietárias.
Semeio por Linguagem Natural: O framework demonstra que provas opcionais em linguagem natural podem servir como scaffolds estruturais eficazes para o blueprint inicial, particularmente para problemas com estruturas não locais (ex: somas cíclicas, cadeias de divisibilidade), ajudando a ancorar a estratégia para o loop de refinamento.

Resultados Experimentais

O sistema foi avaliado em cinco benchmarks: MiniF2F-test, PutnamBench, IMO 2025, Putnam 2025 e USAMO 2026.

MiniF2F-test: Alcançou 99,2% pass@1 (242/244 problemas) sem orientação de linguagem natural. Com o semeio opcional de linguagem natural, resolveu todos os 244 problemas (100%), estabelecendo um novo recorde para sistemas de pesos abertos.
PutnamBench: Alcançou 75,6% pass@1 (508/672 problemas), superando o pipeline Hilbert (70,0% em pass@1840) e o AxProverBase (54,7% em pass@1). Com orientação de linguagem natural (pass@4), a taxa de resolução aumentou para 88,8% (597/672).
IMO 2025: Resolveu 4/6 problemas.
Putnam 2025: Resolveu 11/12 problemas.
USAMO 2026: Resolveu 3/6 problemas (um benchmark livre de contaminação, dado que os problemas são posteriores aos cortes de treinamento do modelo).

Análise de Custo: No PutnamBench, o Goedel-Architect resolveu o conjunto completo de 672 problemas por $294 em custos de API. Em contraste, o próximo melhor pipeline aberto (Hilbert) reportou ter gasto aproximadamente $163k–$ 170k para uma única execução, destacando um enorme diferencial de eficiência.

Significância e Alegações

Os autores afirmam que o Goedel-Architect estabelece uma nova fronteira de Pareto para a prova formal de teoremas. Demonstra que um alto desempenho (rivalizando com sistemas proprietários massivos como AlphaProof ou sistemas que utilizam Claude Opus 4.5) pode ser alcançado com um backbone de pesos abertos altamente eficiente e um design de pipeline inovador.

O artigo enfatiza que a combinação do grafo de dependência global (permitindo o refinamento holístico) e dos modelos de pesos abertos (DeepSeek-V4-Flash) é o motor principal deste sucesso. O sistema fecha efetivamente a lacuna entre a acessibilidade acadêmica e o desempenho de fronteira, tornando a prova formal de alto nível viável a uma fração do custo anterior. Os autores observam que, embora a orientação por linguagem natural aumente significativamente o desempenho nos problemas mais difíceis, o núcleo do pipeline permanece robusto e eficaz sem ela em benchmarks padrão.