🤖 AI

Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

O artigo apresenta o Goedel-Code-Prover, um modelo de linguagem unificado que utiliza uma busca de prova hierárquica e uma pontuação de decomposição principista para verificar código em Lean 4, alcançando uma taxa de sucesso de 62,0% em benchmarks e superando modelos significativamente maiores com maior eficiência.

Autores originais: Zenan Li (Mike), Ziran Yang (Mike), Deyuan (Mike), He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin

Publicado 2026-03-23

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Zenan Li (Mike), Ziran Yang (Mike), Deyuan (Mike), He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin

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ê pediu para um assistente de IA escrever um código de computador para resolver um problema difícil, como encontrar um número único em uma lista gigante. O assistente escreve o código e diz: "Pronto! Funciona!". Mas, na vida real, especialmente em coisas críticas como sistemas bancários ou de aviação, "parecer que funciona" não é suficiente. Você precisa ter a certeza absoluta de que não há erros ocultos.

É aqui que entra o Goedel-Code-Prover, o protagonista deste artigo. Vamos explicar como ele funciona usando uma analogia simples: construir um arranha-céu.

O Problema: O "Pulo do Gato" da IA

As IAs atuais (como o ChatGPT) são ótimas em escrever o código inicial, mas são péssimas em provar matematicamente que esse código é 100% seguro.

A tentativa antiga: Pedir para a IA escrever a prova inteira de uma vez, como se fosse um aluno tentando resolver uma equação complexa sem fazer os passos intermediários. A IA geralmente falha, inventa lógica ou se perde.
O problema real: Provar que um programa funciona é como construir um prédio de 100 andares. Se você tentar colocar o telhado antes de fazer a fundação, o prédio cai.

A Solução: O Arquiteto e o Mestre de Obras

O Goedel-Code-Prover não tenta fazer tudo de uma vez. Ele usa uma estratégia chamada Busca Hierárquica de Provas. Pense nele como uma equipe de construção com dois papéis principais:

O Arquiteto (Decomposição):
Antes de começar a construir, o Arquiteto olha para o prédio inteiro (o problema complexo) e diz: "Não podemos construir isso tudo de uma vez. Vamos dividir em partes menores."
Ele quebra o grande problema em pequenos "sub-problemas" (lemas), como: "A fundação está sólida?", "As paredes do 1º andar estão retas?", "O elevador funciona?".
- O Segredo: O Arquiteto não chuta. Ele usa uma régua de pontuação (o "Score de Decomposição") para garantir que cada pedaço pequeno seja realmente mais fácil de resolver do que o problema original e que, se todos os pedaços forem resolvidos, o prédio inteiro estará de pé.
O Mestre de Obras (Completude):
Depois que o Arquiteto divide o trabalho, o Mestre de Obras pega cada pequeno pedaço e tenta construí-lo. Se ele errar uma parede, o computador (o Lean 4) avisa: "Atenção, essa parede está torta!". O Mestre de Obras corrige e tenta de novo até que a peça esteja perfeita.

Como eles aprendem? (O Treinamento Híbrido)

O grande truque do artigo é como eles treinaram essa IA.

O Dilema: O "Arquiteto" precisa de muitos detalhes para aprender (como "essa divisão é 80% melhor que aquela"), mas o "Mestre de Obras" só recebe um "Sim" ou "Não" (o prédio caiu ou ficou de pé?). Isso confundiria a IA.
A Solução: Eles usaram um método híbrido. Primeiro, ensinaram a IA com exemplos de mestres humanos (Supervisão). Depois, usaram um sistema de recompensas onde o "Arquiteto" ganha pontos por fazer divisões inteligentes (baseado na régua de pontuação), enquanto o "Mestre de Obras" é mantido estável com exemplos de sucesso. Assim, eles aprendem juntos, sem se atrapalhar.

Os Resultados: O "Guerreiro Pequeno"

O mais impressionante é que eles criaram um modelo de IA com 8 bilhões de parâmetros (que é considerado "pequeno" no mundo das IAs atuais, que têm centenas de bilhões).

A Conquista: Esse modelo pequeno conseguiu provar códigos corretos com 62% de sucesso.
A Comparação: Ele superou modelos gigantes (até 84 vezes maiores) e os modelos mais famosos do mercado (como o GPT-5 ou Claude).
A Analogia: É como se um estudante de engenharia brilhante, usando apenas um caderno e uma régua, conseguisse resolver problemas de física que deixam os supercomputadores mais caros do mundo confusos.

Por que isso importa?

Hoje, confiamos em IAs para escrever código, mas não podemos confiar cegamente nelas para garantir segurança. O Goedel-Code-Prover é um passo gigante para transformar o código de "parece que funciona" para "provavelmente, matematicamente, é impossível falhar".

Em resumo: Em vez de tentar adivinhar a resposta final, a IA aprendeu a quebrar o problema em pedaços gerenciáveis, verificar se cada pedaço faz sentido, e só então construir a prova final. É a diferença entre tentar pular um rio de uma vez só e construir uma ponte pedra por pedra.

1. O Problema

A verificação formal de código é essencial para garantir a correção de sistemas críticos, mas a construção de provas verificáveis por máquina (usando assistentes de prova como o Lean 4) permanece um desafio de automação. Embora os Grandes Modelos de Linguagem (LLMs) sejam eficazes na geração de código, eles falham em garantir a ausência de erros lógicos sutis ou violações de especificação.

O artigo identifica três lacunas fundamentais que impedem a transferência de métodos de prova bem-sucedidos em matemática para a verificação de código:

Decomposição Desfundamentada (Ungrounded Decomposition): Ao contrário da matemática, onde há um vasto corpus de raciocínio formal em livros e artigos, não existe um corpus natural de linguagem sobre como provar a correção de programas. LLMs carecem da intuição para decompor objetivos complexos em subobjetivos válidos e mais simples.
Proliferação de Conceitos (Concept Proliferation): Cada programa introduz um novo "universo conceitual" (novas definições de funções, invariantes de estruturas de dados, comportamentos computacionais) sem suporte de bibliotecas compartilhadas (como o Mathlib na matemática), exigindo que o modelo descubra propriedades do zero.
Mudança na Distribuição de Táticas (Tactic Distribution Shift): As táticas necessárias para provar propriedades de código (lógica discreta, recursão, reflexão computacional) diferem significativamente das táticas algébricas predominantes em provas matemáticas. Modelos treinados em matemática frequentemente falham ao aplicar as ferramentas corretas para código.

2. Metodologia

Os autores propõem o Goedel-Code-Prover, um framework de busca de prova hierárquica que opera em duas fases principais, utilizando um único modelo de política unificado (8B parâmetros) para ambas as tarefas:

A. Framework de Busca Hierárquica

O processo é dividido em duas etapas sequenciais:

Decomposição de Lemas (Planejamento): O objetivo de verificação de alto nível é decomposto recursivamente em uma série de lemas intermediários estruturalmente mais simples.
Completude de Lemas (Prova): Cada lema folha (subobjetivo) é provado individualmente através da geração e refinamento iterativo de táticas, com feedback do compilador Lean.

B. A Pontuação de Decomposição (Decomposition Score)

O núcleo da abordagem é uma métrica principista que serve tanto como recompensa de treinamento quanto como critério de classificação na inferência. A pontuação $S$ combina dois eixos:

Justificativa Construtiva (Constructive Justification): Verifica se os lemas propostos implicam logicamente no teorema pai (reconstrução de prova) e se sobrevivem a uma busca de contraexemplos via quickcheck (garantindo que os lemas não sejam falsos ou triviais).
Eficácia Estrutural (Structural Effectiveness): Mede a redução na complexidade. Utiliza uma métrica de "pegada de operadores" (operator footprint) na Árvore de Sintaxe Abstrata (AST) para quantificar a dificuldade. A pontuação recompensa decomposições que reduzem significativamente o número de operadores lógicos e computacionais nos subobjetivos.

C. Treinamento Híbrido por Reforço (Hybrid RL)

Para superar o desajuste de recompensas (a decomposição tem um sinal contínuo e denso, enquanto a prova final é binária), os autores utilizam:

Inicialização Supervisionada (SFT): Treinamento em dados gerados por modelos de ponta para decomposição e completude.
Reforço Híbrido:
- Decomposição: Otimizada via Group Relative Policy Optimization (GRPO) usando a pontuação contínua de decomposição para guiar a exploração.
- Completude: Estabilizada através de replay supervisionado de trajetórias de prova de alta qualidade, evitando a instabilidade de sinais binários esparsos.

3. Principais Contribuições

Framework Hierárquico: Uma nova arquitetura para verificação de código que separa o planejamento (decomposição) da execução (prova de táticas), superando as limitações da geração de prova em uma única passada.
Métrica de Pontuação Unificada: Uma pontuação de decomposição que alinha estritamente a otimização durante o treinamento com os critérios de busca durante a inferência, garantindo que o modelo aprenda o que é realmente útil para a prova.
Política Unificada: Um único modelo (Goedel-Code-Prover-8B) capaz de realizar tanto a decomposição complexa quanto a geração de táticas, treinado com uma abordagem híbrida de RL.
Escalabilidade na Inferência: Demonstração de que o desempenho melhora monotonicamente com o aumento do orçamento de busca (iterações e amostragem paralela), indicando potencial de escalabilidade não saturado.

4. Resultados Experimentais

O framework foi avaliado em três benchmarks baseados em Lean 4 (Verina, Clever e AlgoVeri), totalizando 427 tarefas.

Desempenho Geral: O modelo de 8B parâmetros alcançou uma taxa de sucesso de 62,0% em todos os benchmarks.
Comparação com Baselines:
- Superou o modelo de raciocínio mais forte (GPT-5.3-Codex) e outros provadores neurais de ponta (como DeepSeek-Prover-V2-671B e Goedel-Prover-V2-32B).
- Representa uma melhoria de 2,6x em relação à melhor baseline existente.
- Desempenhou melhor do que provadores neurais até 84 vezes maiores em número de parâmetros.
Análise de Escala: A taxa de sucesso aumentou consistentemente com mais iterações de busca e maior orçamento de amostragem paralela (pass@k), demonstrando que o método não saturou dentro dos limites testados.
Qualidade das Provas: As provas verificadas geradas pelo sistema são profundas, exigindo em média 8 a 17 lemas decompostos e mais de 130 linhas de código de prova por tarefa.

5. Significado e Impacto

Este trabalho é significativo por fechar a lacuna entre a geração de código e a verificação formal rigorosa. Ao introduzir uma camada de planejamento explícito (decomposição) guiada por uma métrica de qualidade principista, o Goedel-Code-Prover demonstra que modelos menores, mas especializados e treinados com arquiteturas hierárquicas, podem superar modelos massivos genéricos em tarefas complexas de verificação de software.

A abordagem valida que a verificação de código não deve ser tratada apenas como um problema de geração de texto, mas como um processo de busca estruturada onde a decomposição correta do problema é o fator determinante para o sucesso. Isso abre caminho para a adoção mais ampla de verificação formal em ambientes de desenvolvimento de software críticos, reduzindo a dependência de testes empíricos insuficientes.