🤖 AI

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation

O artigo apresenta o $P^3$ , um fluxo de trabalho de agentes baseado em LLM que planeja conjuntamente programas e suas provas formais para superar as ineficiências da geração sequencial, alcançando desempenho de estado da arte e reduções significativas de custo em benchmarks de geração de código verificado, incluindo um novo conjunto de dados derivado de repositórios chamado Lean4Commit0.

Autores originais: Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang

Publicado 2026-08-11

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang

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á ensinando um robô superinteligente a escrever uma história. Você dá ao robô um tema, e ele cospe um conto. Mas aqui está o detalhe: você não quer apenas uma história; você quer uma história que seja matematicamente garantida como verdadeira, sem furos no roteiro, sem magia que quebre as leis da física e sem personagens que desaparecem sem explicação. Este é o mundo da geração de código verificado. É um canto da ciência da computação onde pedimos à Inteligência Artificial não apenas para escrever software, mas para escrever software que venha com sua própria "prova de correção" — um certificado matemático que diz: "Eu prometo que este código fará exatamente o que eu disse que faria, para todas as situações possíveis".

Por muito tempo, a maneira padrão de fazer isso era como uma dança de dois passos: primeiro, o robô escreve o código (a história) e, depois, uma equipe separada de revisores de provas de robôs tenta verificar se a história faz sentido. Se os revisores encontrarem um furo no roteiro, eles devolvem a história para o escritor consertar. O escritor remenda a história, envia de volta, e o ciclo se repete. Mas este artigo sugere que essa dança de "escrever-então-verificar" é frequentemente desajeitada e ineficiente. É como tentar construir uma ponte e, depois que ela está terminada, perceber que você esqueceu de colocar as vigas de suporte, forçando você a derrubá-la e reconstruí-la. Os autores deste artigo propõem uma nova maneira: em vez de escrever o código e depois a prova separadamente, o robô deve planejar a ponte inteira — tanto a estrada quanto os suportes — ao mesmo tempo, garantindo que eles se encaixem perfeitamente desde o primeiro esboço.

O Problema: A Armadilha do "Escrever-então-Verificar"

O artigo, intitulado "Joint Program-and-Proof Planning for Verified Code Generation" (Planejamento Conjunto de Programa e Prova para Geração de Código Verificado), aborda um gargalo frustrante na forma como a IA escreve software verificado. Atualmente, a maioria dos sistemas segue um fluxo de trabalho de "programa-então-prova". É como pedir a um chef para cozinhar uma refeja complexa e, depois que a comida está na mesa, perguntar a um crítico gastronômico se os ingredientes estavam frescos e se o método de cozimento foi seguro. Se o crítico encontrar um problema (como um frango mal cozido), o chef tem que voltar, recozinhar o prato e torcer para que o crítico goste desta vez.

Os autores argumentam que essa abordagem sequencial é falha. Quando a IA se compromete a escrever o código primeiro, ela pode escolher uma estrutura que parece boa na superfície, mas que é um pesadelo para provar. Por exemplo, imagine que a IA escreva um programa para encontrar o maior número em uma lista. Ela pode escolher um método que é curto e rápido de escrever, mas que exige uma regra matemática incrivelmente complexa e oculta para provar que funciona. Uma vez que o código é escrito, a IA está presa: ela tem que ou inventar uma prova super difícil para corresponder àquele código específico ou rasgar o código e começar de novo. Isso leva a muito tempo desperdiçado, dinheiro e "loops de reparo" onde a IA continua remendando o código e a prova, mas eles nunca se encaixam perfeitamente.

A Solução: P3 (O Planejador "Mão na Mão")

Para corrigir isso, os pesquisadores introduzem o P3, um novo fluxo de trabalho onde a IA atua como um mestre arquiteto que desenha a planta tanto do edifício quanto da inspeção de segurança antes de assentar um único tijolo.

Em vez de saltar diretamente para a escrita do código, o P3 cria primeiro um plano unificado. Este plano é um esboço de alto nível que responde a duas perguntas ao mesmo tempo:

Como o código funcionará? (O "Esboço do Programa")
Como provaremos que ele funciona? (O "Esboço da Prova")

O plano decide a estrutura da solução. Ele escolhe a "forma" certa para o código (como escolher entre um loop recursivo ou um fold) e, simultaneamente, escolhe as regras matemáticas correspondentes (invariantes) necessárias para provar que essa forma é segura. É como decidir: "Construiremos uma ponte usando cabos de suspensão, portanto, nosso plano de prova deve incluir a verificação da tensão desses cabos".

Uma vez que esse plano compartilhado é travado, a IA então "elabora" os detalhes. Ela escreve o código real e a prova real, mas está apenas preenchendo as lacunas de um projeto previamente acordado. Se a prova falhar, a IA sabe exatamente onde olhar porque a estrutura já havia sido decidida. Se o próprio plano for ruim (por exemplo, o design da ponte é impossível), a IA volta à fase de planejamento para redesenhar o projeto, em vez de desesperadamente remendar o edifício acabado.

O Novo Campo de Teste: Lean4Commit0

Os autores perceberam que os testes anteriores para esses sistemas de IA eram fáceis demais, como pedir ao robô para resolver enigmas matemáticos de um livro didático. O software do mundo real é muito mais bagunçado. Para testar adequadamente o novo método, eles construíram um novo benchmark chamado Lean4Commit0.

Eles coletaram dados de 108 bibliotecas de software de código aberto do mundo real (escritas em Python, Rust, C/C++ e Java) e transformaram suas funcionalidades principais em desafios de "código verificado". Em vez de tarefas simples como "somar dois números", esses desafios envolvem relações complexas entre diferentes partes de um programa. Por exemplo, em um sistema de configuração, eles podem pedir à IA para provar que "se você definir uma configuração como 'Alta' e depois defini-la como 'Baixa', o sistema recordará corretamente a configuração 'Baixa'". Essas tarefas exigem que a IA entenda como diferentes funções se comunicam, tornando-as muito mais difíceis do que problemas de livros didáticos.

O Que Eles Descobriram: Planejar Juntos Vence

A equipe testou o P3 contra quatro dos modelos de IA mais poderosos disponíveis (incluindo versões do Codex, Gemini e Claude) através de três benchmarks diferentes: Verina, AlgoVeri e o seu novo Lean4Commit0.

Os resultados foram claros: Planejar juntos funciona melhor do que escrever separadamente.

Taxa de Sucesso: O P3 resolveu mais tarefas do que qualquer outro método em todos os testes. Nas tarefas mais difíceis, ele melhorou a taxa de sucesso em 4,6 a 11,2 pontos percentuais em comparação com os melhores métodos existentes.
Eficiência: Não se tratava apenas de resolver mais problemas; era sobre resolvê-los de forma mais rápida e barata. Em tarefas difíceis, o P3 reduziu o custo das chamadas de API em até 40% e diminuiu o tempo gasto em até 37%. Isso ocorre porque a IA não perdeu tempo tentando provar coisas impossíveis ou reescrevendo códigos que estavam estruturalmente errados.
A Vantagem do "Conjunto": Para provar que o "planejamento conjunto" era o ingrediente secreto, eles realizaram um teste onde a IA planejou o código, mas não planejou a prova antecipadamente. Este método de "planejamento apenas de código" teve um desempenho inferior ao P3, confirmando que pensar na prova enquanto planeja o código é o que faz a diferença.

Um Exemplo do Mundo Real: A Árvore Rubro-Negra

Para mostrar como isso funciona na prática, os autores analisaram um clássico problema da ciência da computação: deletar um nó de uma "árvore rubro-negra" (uma estrutura de dados complexa usada para organizar dados de forma eficiente).

O Jeito Antigo (Programa-então-Prova): A IA se comprometeu com uma forma específica de deletar o nó. Resultou que essa forma era tão estruturalmente bagunçada que a prova exigiu mais de 6.300 linhas de código apenas para consertar os buracos, ou falhou inteiramente.
O Jeito P3: A IA primeiro planejou a deleção. Ela percebeu que uma abordagem estrutural diferente seria mais fácil de provar. Ela manteve esse plano e resolveu o problema em apenas 1.105 linhas.

Por Que Isso Importa

Este artigo sugere que, para a IA escrever software verdadeiramente confiável, precisamos parar de tratar o "código" e a "prova" como dois trabalhos separados. Ao forçar a IA a pensar sobre a segurança matemática do código enquanto ela está projetando o próprio código, obtemos um software que não é apenas correto por construção, mas também mais barato e rápido de produzir. É uma mudança do "consertar depois" para o "construir certo da primeira vez", garantindo que o software em que confiamos seja tão sólido quanto a matemática que prova que ele funciona.

Resumo Técnico: P3 – Planejamento Conjunto de Programa e Prova para Geração de Código Verificado

1. Definição do Problema

O artigo aborda a geração de código verificado, uma tarefa na qual um Modelo de Linguagem de Grande Escala (LLM) deve sintetizar tanto um programa executável ( $\pi$ ) quanto uma prova verificável por máquina ( $\kappa$ ) que demonstre que o programa satisfaz uma especificação formal ( $\sigma = (P, Q)$ ). Diferente da geração baseada em testes, a correção deve ser válida para todas as entradas admissíveis, não apenas para um conjunto finito de exemplos.

Os autores identificam um gargalo crítico no fluxo de trabalho de fato atual, que segue um cronograma sequencial de "programa-então-prova":

O LLM compromete-se com uma implementação concreta.
Uma etapa de prova separada tenta realizar a descarga das obrigações de prova.
Se a verificação falhar, o sistema entra em um ciclo frágil de "correção e tentativa", alternando entre corrigir o código e corrigir as provas.

Esta abordagem sequencial sofre de dois problemas principais:

Efetividade: Um programa gerado sem antecipar sua prova pode carecer de propriedades estruturais necessárias (ex: estratégias de decomposição ou invariantes de indução específicos). Reparos locais frequentemente falham em recuperar uma estrutura amigável à prova que nunca foi planejada.
Eficiência: Recursos computacionais significativos (tokens e tempo) são desperdiçados explorando reparos para implementações que são estruturalmente incompatíveis com os requisitos de prova da especificação.

O artigo baseia-se no princípio de Dijkstra de que programas e seus argumentos de correção devem ser desenvolvidos "lado a lado", argumentando que a implementação e a estrutura da prova se restringem mutuamente.

2. Metodologia: O Framework P3

Os autores propõem o P3, um fluxo de trabalho agêntico que desacopla o planejamento da elaboração para garantir a consistência estrutural entre o programa e a prova antes que qualquer um deles seja totalmente realizado.

2.1 Planejamento Conjunto de Programa e Prova

Na primeira etapa, o agente de LLM gera um plano unificado ( $\rho$ ) baseado na especificação $\sigma$ . Este plano não é meramente código; é um esboço de alto nível contendo quatro compromissos específicos:

Contrato Formal: Instruções algorítmicas e restrições assintóticas.
Decomposição do Programa: A variável de recursão, estrutura de ramificação, representação de dados e medidas de terminação.
Dependências de Biblioteca: Funções concretas e lemas existentes a serem utilizados.
Obrigações de Prova: O predicado de ponte (bridging predicate), a estrutura de indução/caso e declarações de lemas auxiliares necessários.

O agente valida esses planos candidatos ao nível de esboço. Um plano é rejeitado se o esboço do programa violar instruções, se a decomposição falhar em preservar o predicado de ponte, ou se o predicado não implicar a pós-condição. O agente seleciona o plano que minimiza o ônus de prova antecipado.

2.2 Elaboração Guiada pelo Plano

Uma vez selecionado um plano $\rho$ , o agente entra na etapa de elaboração:

Implementação: O agente escreve o código ( $\pi$ ) aderindo estritamente à decomposição e estrutura fixadas em $\rho$ .
Esqueleto de Prova: O agente escreve um esqueleto de prova ( $\kappa$ ) que espelha a estrutura do plano (ex: princípios de indução específicos ou divisões de caso), deixando lacunas locais (representadas como sorry) para táticas detalhadas.
Refinamento: O agente utiliza o feedback do Lean 4 (via LSP/MCP) para preencher essas lacunas. Crucialmente, se os reparos locais falharem repetidamente ou se o predicado de ponte se mostrar muito fraco, o agente identifica isso como uma falha de nível de plano. Em vez de oscilar entre edições de código e prova, o agente recua à etapa de planejamento para revisar $\rho$ .

Essa separação permite que o agente distinga entre erros de nível de elaboração (corrigíveis localmente) e erros de nível de plano (que exigem um novo pensamento estrutural), reduzindo significativamente o espaço de busca.

3. Benchmark: Lean4Commit0

Para avaliar a geração de código verificado em configurações realistas além de algoritmos de livros didáticos, os autores introduzem o Lean4Commit0.

Fonte: Derivado de 108 bibliotecas de código aberto do mundo real através de Python, Rust, C/C++ e Java.
Escopo: Ele extrai APIs principais e codifica seus comportamentos como tarefas de Lean, incluindo especificações relacionais que restringem o comportamento conjunto de múltiplas funções (ex: consistência entre operações set e get).
Controle de Qualidade: Um pipeline de três estágios garante a qualidade da especificação:
1. Satisfação de Referência: Verifica se a implementação original da biblioteca satisfaz a especificação em Lean.
2. Rejeição de Mutação: Garante que a especificação rejeite comportamentos alterados por mutações (evitando especificações sub-restritas).
3. Revisão por LLM: Sinaliza especificações triviais ou irrelevantes.
Escala: O benchmark final contém 511 placeholders de implementação e 519 placeholders de teorema.

4. Resultados Experimentais

Os autores avaliaram o P3 contra dois baselines — um agente PLAIN (sem estratégia específica) e um agente SEQ (programa-então-prova) — utilizando quatro backends de LLM de fronteira (Codex-GPT-5.5, Gemini-3-Pro, Claude-Sonnet-4.6, Claude-Opus-4.7) através de três benchmarks: Verina, AlgoVeri e Lean4Commit0.

Taxas de Solução: O P3 alcançou a maior taxa de solução em cada configuração (benchmark, modelo).
- Comparado ao baseline mais forte, o P3 melhorou as taxas de solução em 4,6 a 11,2 pontos percentuais.
- No subconjunto difícil dos benchmarks, o P3 reduziu os custos de API por tarefa em até ~40% e o tempo de execução em até ~37%.
Estudo de Ablação: Uma comparação com o PLAN-SEQ (que planeja escolhas de implementação, mas não a estrutura da prova) mostrou que o planejamento conjunto contribui especificamente com um ganho adicional de 3,3 a 8,3 pontos percentuais. Isso isola o benefício de antecipar a estrutura da prova durante a fase de planejamento.
Estudo de Caso: Em uma tarefa de deleção de árvore rubro-negra inclinada à esquerda, o baseline programa-então-prova ou falhou após gerar 6.344 linhas de código ou obteve sucesso apenas com invariantes de reconstrução redundantes (1.176 linhas). O P3, ao comparar planos antes de se comprometer, resolveu a tarefa em 1.105 linhas.

5. Significância e Alegações

O artigo afirma que o P3 demonstra que a geração de código verificado pode ser tornada mais eficaz e eficiente ao tratar o programa e a prova como artefatos co-projetados, em vez de saídas sequenciais.

Consistência Estrutural: Ao estabelecer um plano estrutural compartilhado, o P3 garante que a implementação e a prova sejam consistentes "por construção", evitando a necessidade de reconciliação a posteriori.
Escalabilidade para Código do Mundo Real: A introdução do Lean4Commit0 preenche a lacuna entre benchmarks acadêmicos (algoritmos de livros didáticos) e software de produção (restrições de API relacionais), mostrando que o planejamento conjunto é particularmente benéfico para tarefas complexas de nível de biblioteca.
Eficiência: O framework reduz o comportamento de "oscilação" comum em loops de reparo iterativos, levando a economias significativas de recursos computacionais e tempo.

Os autores concluem que, embora o verificador (Lean 4) permaneça a autoridade final, a capacidade do agente de planejar o programa e a prova conjuntamente aumenta significativamente a probabilidade de produzir uma solução verificada dentro de limites de recursos práticos.