RefactorProof: provas geradas por LLMs quebram depois da refatoração de código

Os benchmarks de geração verificável de código costumam checar a prova em uma única implementação fixa. Os autores do RefactorProof quiseram saber o que acontece quando a implementação é reescrita com o mesmo comportamento. Das 185 tarefas do VERINA que compilam no ambiente fixado por eles, os pesquisadores construíram 458 variantes certificadas pelo Lean. A especificação e a prova a ser verificada não mudaram nem um byte. O resultado: nas refatorações estruturais, as provas deixam de passar na verificação em massa. Para as provas de referência do VERINA, a taxa de sobrevivência (task-normalized structural PSR) é de 4,3%; para os verificadores LLM especializados, fica entre 13,3% e 26,8%.

Como funciona o teste de fragilidade

A ideia é simples e implacável. Uma prova formal está amarrada ao texto específico do programa: nomes, ordem das definições, estrutura das expressões. Se o desenvolvedor extrai uma função, muda a forma de um cálculo ou renomeia uma variável, nada muda do ponto de vista lógico, mas a prova em Lean pode deixar de compilar. No desenvolvimento real, a refatoração acontece o tempo todo, então saber se a prova sobrevive a uma edição é uma questão prática.

O VERINA fornece provas de referência apenas para 46 tarefas, todas do split básico. Por isso, as principais comparações entre modelo e referência se apoiam em 21–25 tarefas curtas e não recursivas, escolhidas para que todos os participantes partam do mesmo terreno. A amostra é restrita, e o alcance das conclusões deve ser lido com essa ressalva.

As máquinas são frágeis, mas os humanos são mais

A reviravolta é que as provas dos modelos se mostraram mais estáveis que as de referência. Em tarefas comparáveis, a taxa geral de provas inalteradas que sobrevivem é maior nos modelos do que nos artefatos do VERINA. Os intervalos de confiança de 95% para os três modelos não incluem o zero.

• DeepSeek-Prover-V2-7B: +15,6 pontos em relação à referência
• Goedel-Prover-V2-32B: +18,8 pontos
• Goedel-Prover-V2-8B: +20,3 pontos

A ordem se mantém ao excluir as variantes T1, que todas as provas sobrevivem, ao agregar com balanceamento por família de refatoração e ao usar regras alternativas, aplicáveis na prática, para selecionar a prova válida. A causa provável é que as provas de referência foram escritas para uma forma específica de código e são muito dependentes dela, enquanto os modelos tendem a gerar provas mais diretas e menos ligadas aos detalhes da construção. Isso é uma hipótese: os autores não demonstram esse mecanismo.

Quebrar não significa que consertar seja caro

A principal ressalva do artigo diz respeito ao custo da quebra. Correções predefinidas de um único identificador consertam 51 de 54 falhas estruturais elegíveis nas provas de referência e 58 de 85 falhas elegíveis nas provas dos modelos. Ou seja, a maior parte da "fragilidade" é eliminada com um ajuste barato, e nas provas de referência quase tudo é consertado. Para os modelos, o quadro é pior: cerca de 68% contra 94%.

Por isso, o RefactorProof mede especificamente a estabilidade da prova inalterada diante da refatoração. Ele não avalia o custo de manter a prova depois que ela quebra, e os autores deixam isso explícito.

Principais parâmetros do estudo

• Benchmark: RefactorProof, derivado do VERINA
• Tarefas de origem: 185 (compilam no ambiente Lean fixado)
• Variantes certificadas: 458
• Provas de referência do VERINA: 46 tarefas, apenas o split básico
• Amostra comparável: 21–25 tarefas curtas e não recursivas
• PSR estrutural das provas de referência: 4,3%
• PSR estrutural dos verificadores especializados: 13,3–26,8%
• Modelos avaliados: DeepSeek-Prover-V2-7B, Goedel-Prover-V2-32B, Goedel-Prover-V2-8B
• Reparo com edição de um único identificador: 51/54 nas provas de referência, 58/85 nas provas dos modelos
• Evento: NeurIPS 2026 Workshop on AI for Verifiable Coding; categorias cs.AI, cs.LO, cs.SE

O que muda na prática

Equipes que montam pipelines do tipo "o LLM escreve o código e a prova, o Lean verifica" recebem um sinal claro: validar em uma única implementação fixa superestima a confiabilidade. Inclua no CI variantes refatoradas do programa e rode a prova contra elas. Se a prova falhar, tente primeiro correções automáticas e baratas de identificadores: segundo os dados do trabalho, elas resolvem uma parcela significativa dos casos. Ao avaliar modelos prover, olhe não só a proporção de tarefas resolvidas, mas também a sobrevivência das provas quando o código muda. Para quem cria benchmarks, a conclusão também é direta: é preciso medir tanto a estabilidade quanto o custo de reparo. O RefactorProof ainda não tem essa segunda métrica.