Benchmark Vero de Berkeley: na melhor das hipóteses, só 27 de 43 projetos concluídos

O laboratório RDI da Universidade da Califórnia em Berkeley lançou um benchmark chamado Vero. Ele exige que agentes de IA façam, na escala de um repositório inteiro, duas coisas ao mesmo tempo: implementar cada API exigida e provar que cada especificação dada é válida, mantendo código, prova e build sempre consistentes entre si. Os benchmarks anteriores de verificação formal basicamente paravam no nível de um único teorema ou função; este é o primeiro no nível de repositório.

A tarefa é composta por 43 projetos Lean 4 multimódulo, portados de código existente em Python, Dafny, Verus e Coq, cobrindo ao todo 743 APIs e 2.705 especificações formais. A avaliação roda em dois modos: no modo somente prova, uma implementação de referência é fornecida e o agente só precisa prová-la; no modo código e prova, o agente precisa escrever a própria implementação e depois provar que ela satisfaz a especificação.

Tabela de pontuação

Número de instâncias totalmente resolvidas (de um total de 43) com orçamento de 90 minutos:

Vale a pena olhar com atenção para o fosso entre a primeira e a terceira linha: com o mesmo GPT-5.5 e o mesmo Codex, apenas ao mudar o nível de raciocínio de medium para xhigh, a pontuação no modo código e prova salta de 2 para 27. Nesse tipo de tarefa, o retorno marginal do orçamento de raciocínio está longe de saturar.

A dificuldade não está em provar uma especificação isolada

A linha do topo traz ainda outro conjunto de números. O GPT-5.5 (xhigh) passa em 87,3% das especificações individuais no modo código e prova, e em 85,8% no modo somente prova, mas, no critério de 'instância totalmente concluída', restam apenas 27/43 e 25/43. O julgamento dos pesquisadores é direto: provar cada especificação isolada já não é mais o ponto difícil; o difícil é manter todo o repositório de provas consistente.

A diferença entre esses dois números tem implicações práticas de engenharia. Uma taxa de acerto de 87% por especificação, projetada para um projeto com dezenas de especificações, significa que quase todo projeto vai deixar algumas especificações travadas. E a verificação formal é do tipo tudo ou nada: falta provar uma única especificação e o repositório inteiro não compila, sem que as partes já corretamente provadas recebam qualquer crédito parcial. Isso é completamente diferente de um projeto com 87% dos testes unitários passando, que ainda assim pode ir para produção.

Outro detalhe está na composição do código de prova. Nas execuções totalmente resolvidas, os lemas auxiliares representam uma mediana de 73,6% do código de prova. Ou seja, três quartos do que os agentes escrevem é andaime montado às pressas para sustentar a prova principal. Essa proporção sugere que os modelos atuais seguem um caminho de amplitude, empilhando lemas na força bruta, em vez de encontrar uma estrutura de prova enxuta.

Escolher o próprio algoritmo: ajudou 5 vezes, atrapalhou 17

O modo código e prova dá ao agente um grau de liberdade: como a implementação pode ser escrita por ele mesmo, é possível escolher um algoritmo mais fácil de provar. Os pesquisadores mediram o efeito líquido dessa liberdade e, em comparações pareadas, 5 casos tiveram sucesso graças à troca de algoritmo, enquanto 17 fracassaram por causa dela.

Esse 5 contra 17 diz bastante. Em teoria, poder escolher a própria implementação só deveria ajudar — na pior das hipóteses, bastaria copiar a implementação de referência. Na prática, o modelo frequentemente escolhe uma abordagem que julga 'esperta', mas que acaba sendo mais difícil de provar, e depois fica preso nela dentro dos 90 minutos. Saber escrever código e saber que tipo de código é fácil de provar são duas habilidades diferentes, e os agentes atuais só dominam a primeira.

O ranking ainda deixa uma nota: das 43 instâncias, 10 nunca foram resolvidas por nenhuma configuração, em nenhum dos dois modos. Esse grupo constitui o teto rígido atual do método e é também onde a próxima rodada de trabalho mais precisa se concentrar.

Para quem constrói ferramentas de programação com IA, o valor de referência do Vero não está no ranking, mas no fato de transformar a 'consistência em nível de repositório' — algo antes só percebido pela experiência — em uma métrica mensurável. Benchmarks do tipo SWE-bench medem se é possível corrigir corretamente um bug; o Vero mede se é possível suportar todas as restrições de um projeto de engenharia por completo. As duas coisas não estão no mesmo nível de dificuldade.

Fontes: blog público do laboratório RDI de Berkeley, CocoLoop; a escala do benchmark, o número de instâncias totalmente resolvidas nos dois modos, a taxa de acerto por especificação, a proporção de lemas auxiliares e as estatísticas de comparação pareada foram todos conferidos conforme o relatório público.