Provas Lean para código gerado por IA quebram após refatoração em 13-27% dos casos

Quando um modelo de linguagem escreve código e anexa imediatamente a ele uma prova matemática formal de sua correção em Lean, o resultado parece à prova de falhas: o programa tem a garantia de fazer exatamente o que deveria. Mas todos os testes existentes verificam a prova apenas contra uma única versão fixa do código. No desenvolvimento real, o código é constantemente reescrito — lógica duplicada é extraída para uma função separada, operações são reordenadas, condições são invertidas —, enquanto o comportamento do programa permanece o mesmo. A questão é se a prova antiga resiste a esse tipo de reestruturação, mesmo quando o significado do código não mudou.

Os autores do trabalho propõem uma metodologia chamada RefactorProof para medir exatamente isso. Eles pegaram 185 problemas do conhecido benchmark VERINA (que verifica tanto o código quanto as provas em Lean) e aplicaram a cada problema cinco tipos de reescritas mecânicas e totalmente automáticas: extrair um trecho de lógica para uma função separada, trocar operandos em operações comutativas, inverter condições, entre outras. Para cada reescrita, provou-se separadamente, via Lean, que o comportamento do programa não havia mudado. O resultado foram 458 variantes de código verificadas. Cada variante foi então pareada com a prova original (idêntica byte a byte) para verificar se o Lean ainda a aceitava.

O que se mostrou frágil — e o que não

As provas de referência que os autores do VERINA escreveram manualmente para 46 problemas sobreviveram à refatoração quase sem perdas — uma taxa de quebra de apenas 4,3%. Mas isso não significa que as provas manuais sejam inerentemente mais robustas: esses 46 problemas são os mais simples do benchmark, com um comprimento mediano de código de uma única linha, e apenas 6,5% deles são recursivos.

As provas geradas por modelos especializados em demonstração de teoremas — DeepSeek-Prover-V2-7B e duas versões do Goedel-Prover-V2 (8B e 32B) — quebraram com muito mais frequência: as taxas de falha variaram de 13,3% a 26,8%. Mas, ao comparar os modelos com a referência em um conjunto de problemas idêntico e comparável, o quadro se inverte: as provas dos modelos sobrevivem à refatoração com mais frequência do que as de referência — 15,6 pontos a mais para o DeepSeek-7B, 18,8 pontos para o Goedel-32B e 20,3 pontos para o Goedel-8B. A diferença é estatisticamente significativa nos três casos.

Por que algumas provas desmoronam e outras resistem

Os pesquisadores identificaram um mecanismo concreto por trás dessa resiliência. As provas de referência geralmente começam com o comando `unfold`, que expande a definição da função diretamente no texto. As provas dos modelos, por outro lado, costumam começar afirmando explicitamente que uma chamada de função e seu corpo são iguais por meio da tática `rfl` (uma chamada "ponte definicional"), e só então demonstram o resto automaticamente.

Quando o código é movido para uma função separada (extração de lógica), essa "ponte" se mostra muito mais durável: no nível das tarefas, as provas com ponte sobrevivem em 6 de 6 casos, enquanto as demais estratégias conseguem apenas 6 de 31. Mas esse recurso tem um lado negativo: se a reescrita muda substancialmente o corpo da função (e não apenas sua localização), uma ponte amarrada ao texto específico daquele corpo deixa de passar a verificação de tipos — essas provas sobrevivem apenas 0 de 3 vezes, contra 17 de 19 em provas mais gerais, não atreladas a uma formulação específica.

Uma quebra não é uma catástrofe

A principal conclusão prática é que uma prova que deixa de ser aceita após uma refatoração não significa necessariamente uma reescrita cara. Os pesquisadores testaram isso diretamente: pegaram as provas quebradas e tentaram corrigi-las com uma única edição pontual simples: renomear um identificador. Das 54 quebras elegíveis em provas de referência, 51 foram corrigidas dessa forma; das 85 quebras em provas geradas por modelos, 58 foram corrigidas.

Para equipes que dependem da geração verificável de código por IA, a conclusão é direta: o simples fato de uma prova deixar de passar após uma refatoração não é motivo de pânico, nem indica que um modelo seja, em princípio, pior na geração de provas. É antes um sinal de que vale a pena incorporar ao pipeline de verificação uma checagem automática e um reparo leve das provas após qualquer mudança no código, em vez de tratar a quebra como um veredito definitivo sobre a qualidade do modelo.