Resumo Técnico: Verus-SpecGym

Declaração do Problema

Embora os agentes de codificação com IA estejam cada vez mais capazes de gerar código verificado (código acompanhado de provas verificadas por máquina), um gargalo fundamental permanece: a fidelidade da própria especificação formal. A geração de código verificado garante que o código satisfaça uma determinada especificação formal, mas não garante que a especificação capture com precisão a intenção informal do usuário. Se um agente gerar uma especificação muito fraca, pode certificar código incorreto; se for muito forte, pode rejeitar código correto.

O artigo aborda a autoformalização de especificações: a tarefa de traduzir problemas de programação informais (descrições em linguagem natural) em especificações formais fiéis. O desafio central é a avaliação. Os métodos existentes dependem de especificações de referência caras, escritas por especialistas, ou de juízes aproximados baseados em LLM, ambos dos quais lutam para detectar erros semânticos sutis ou escalar de forma eficaz. Há uma necessidade de um mecanismo de avaliação escalável e determinístico que possa verificar se uma especificação gerada aceita exatamente as entradas válidas e as saídas corretas definidas pelo problema informal.

Metodologia

1. O Benchmark: VERUS-SPECBENCH

Os autores introduzem o VERUS-SPECBENCH, um benchmark composto por 581 tarefas de escrita de especificações derivadas de problemas de programação do Codeforces. Esses problemas foram selecionados para visar o Verus, um framework de verificação para Rust.

• Estrutura da Tarefa: Cada tarefa fornece a um agente uma declaração de problema informal, um esqueleto formal Verus (definindo tipos de entrada/saída e funções vazias pre_spec e post_spec), casos de teste amostrais e documentação.
• Fontes de Dados: O benchmark aproveita duas fontes distintas para casos de teste:
  • Testes Oficiais do Codeforces: Usados principalmente para verificações de completude (entradas válidas e saídas corretas).
  • "Hacks" do Codeforces: Entradas adversariais escritas por competidores humanos para quebrar soluções incorretas que passaram nos testes oficiais. Estes são críticos para verificações de correção (identificando entradas inválidas ou saídas incorretas que os modelos poderiam erroneamente aceitar).

2. O Ambiente: VERUS-SPECGYM

A avaliação ocorre no VERUS-SPECGYM, um ambiente agêntico onde os modelos interagem com o Verus, um shell bash e um sistema de arquivos.

• Refinamento Iterativo: Os agentes leem o problema, escrevem especificações e as refinam iterativamente com base no feedback de um comando de avaliação personalizado (verus_gym_specgen_check).
• Especificações Executáveis: Uma inovação técnica chave é a extensão do mecanismo exec_spec do Verus. As especificações do Verus são tipicamente predicados lógicos para um provador de teoremas e não podem ser executadas em entradas concretas. Os autores estenderam o exec_spec (introduzindo especificamente exec_spec_unverified!) para compilar especificações geradas em código Rust executável. Isso permite que o sistema execute a especificação contra casos de teste concretos para determinar a aceitação ou rejeição de forma determinística.

3. Framework de Avaliação

A avaliação decompõe a fidelidade em quatro categorias de casos de teste:

1. Completude Prévia: Entradas válidas devem ser aceitas pelo pre_spec.
2. Correção Prévia: Entradas inválidas devem ser rejeitadas pelo pre_spec.
3. Completude Pós: Pares (entrada, saída) corretos devem ser aceitos pelo post_spec.
4. Correção Pós: Pares (entrada, saída) incorretos devem ser rejeitados pelo post_spec.

O avaliador utiliza uma estratégia de resolução em dois níveis:

• Verificação Simbólica: Tenta provar o comportamento da especificação usando o solucionador SMT do Verus.
• Fallback Executável: Se a prova simbólica for inconclusiva, a especificação é compilada para Rust executável e executada no caso de teste concreto. Isso garante que até mesmo especificações complexas possam ser avaliadas de forma determinística.

Principais Contribuições

1. VERUS-SPECGYM & VERUS-SPECBENCH: O primeiro ambiente agêntico e benchmark projetados especificamente para avaliar a autoformalização de especificações usando especificações executáveis e casos de teste adversariais de "hack".
2. Avaliador de Especificação Executável: Uma extensão novel do mecanismo exec_spec do Verus que permite testes determinísticos da fidelidade da especificação sem exigir especificações de referência escritas por especialistas ou depender exclusivamente de juízes LLM.
3. Suite de Avaliação Adversarial: A construção de uma suite de avaliação abrangente usando "hacks" do Codeforces escritos por humanos, demonstrando que essas entradas adversariais expõem falhas de especificação que os testes oficiais perdem.
4. Análise Empírica de Modos de Falha: Uma análise detalhada mostrando que até mesmo modelos de ponta capazes de gerar código correto frequentemente falham em escrever especificações fiéis, com falhas agrupadas em: omissão de suposições de entrada, aceitação de saídas incorretas e rejeição de entradas válidas.

Resultados

Os autores avaliaram seis modelos de linguagem de ponta e de código aberto (incluindo gemini-3.1pro, gpt5.3-codex, opus4.6 e vários modelos de código aberto) sob um orçamento fixo de computação e tempo.

• Diferença de Desempenho: O modelo mais forte, gemini-3.1pro, resolveu 77,8% das tarefas. Outros modelos de ponta resolveram entre 51,1% e 57,8%, enquanto modelos de código aberto alcançaram apenas 21,5%–25,5%.
• Código vs. Especificação: Em um subconjunto de problemas onde o gpt5.3-codex pôde gerar código executável correto (81,8% de sucesso), ele falhou em escrever uma especificação fiel para o mesmo problema em muitos casos. Isso indica que a autoformalização de especificações é um gargalo distinto, separado da geração de código.
• Importância dos Testes de Correção: Avaliar apenas em testes de completude superestima significativamente o desempenho. Adicionar testes de correção (derivados de hacks) fez o Pass@1 do gpt5.3-codex cair de 77,8% para 58% e do gemini-3.1pro de 82% para 78%.
• Limitações do LLM como Juiz: Ao usar um LLM como juiz para avaliar especificações, ele perdeu 26% das falhas detectadas pelo avaliador executável. Isso sugere que o teste executável é um sinal mais confiável para os erros sutis inerentes a esta tarefa.
• Modos de Falha: A análise qualitativa revelou três padrões de falha recorrentes:
  1. Omissão de Suposições de Entrada: Falta de promessas estruturais globais (por exemplo, assumir que uma solução existe quando não existe).
  2. Aceitação de Saídas Incorretas: Falha em impor restrições de otimalidade ou correção (por exemplo, aceitar pares não coprimos).
  3. Rejeição de Saídas Válidas: Escrever especificações excessivamente complexas ou restritivas que rejeitam respostas corretas.

Significado e Alegações

O artigo alega que a autoformalização de especificações está ao alcance de agentes de ponta, mas permanece frágil, mesmo em problemas onde eles podem gerar com sucesso código correto. O trabalho demonstra que:

• A geração fiel de especificações é uma capacidade distinta da geração de código.
• O teste executável usando entradas adversariais (hacks) é essencial para uma avaliação confiável, pois expõe casos extremos que testes padrão e juízes LLM perdem.
• Os modelos atuais lutam com a nuance de traduzir intenção informal em predicados lógicos precisos, frequentemente falhando em capturar restrições implícitas ou critérios de otimalidade.

Os autores posicionam este trabalho como um passo em direção a uma geração de código verificado mais robusta, destacando que o "gargalo" mudou de escrever código para escrever a especificação certa. Eles enfatizam que sua abordagem fornece um sinal escalável e determinístico para fidelidade, sem o custo proibitivo de especificações de referência de especialistas.