Resumo Técnico: VeriScale: Escalonamento de Suítes de Teste Adversariais para Geração de Código Verificável

Declaração do Problema

À medida que os Modelos de Linguagem de Grande Escala (LLMs) são cada vez mais implantados para engenharia de software, avaliar sua capacidade de gerar não apenas código funcional, mas também especificações e provas formalmente verificáveis tornou-se crítico. As benchmarks existentes para geração de código verificável, como VERINA e CLEVER, dependem fortemente da avaliação por suítes de teste para avaliar a Geração de Especificação (SpecGen) e a Geração de Código (CodeGen). No entanto, essas benchmarks sofrem de uma limitação fundamental: elas são restringidas pela escassez de casos de teste de alta qualidade, particularmente casos de teste negativos (entradas inesperadas e saídas inesperadas).

As benchmarks atuais tipicamente fornecem apenas um número limitado de pares de entrada-saída positivos. Consequentemente, os modelos podem alcançar taxas de aprovação infladas ao satisfazer esses testes esparsos sem realmente capturar a intenção do programa ou garantir a solidez e a completude de suas especificações geradas. Isso leva a uma superestimação das capacidades do modelo, onde implementações incorretas ou especificações não sólidas passam na avaliação simplesmente porque a suíte de teste falha em expor falhas lógicas ou violações de limites.

Metodologia: O Framework VeriScale

Para abordar essas limitações, os autores propõem o VeriScale, um framework inovador impulsionado por implementações adversariais para escalar e refinar sistematicamente as suítes de teste para geração de código verificável. O framework opera em duas etapas principais: Expansão da Suíte de Teste e Redução da Suíte de Teste.

1. Expansão da Suíte de Teste

O objetivo desta etapa é construir um pool diversificado e desafiador de casos de teste, incluindo pares de entrada-saída esperados, entradas inesperadas e saídas inesperadas.

• Geração de Sementes e Mutação Consciente de Tipo: Inspirando-se no EvalPlus, o VeriScale utiliza LLMs para sintetizar entradas iniciais (sementes). Essas sementes são então expandidas por meio de uma estratégia de mutação iterativa e consciente de tipo. O framework formaliza a mutação como um processo de cinco tuplas ($M = (T, D, O, p, q)$) que preserva os tipos de entrada enquanto introduz perturbações estruturais. Isso inclui reutilizar valores contextuais de um "pool de ingredientes" ou aplicar heurísticas específicas de tipo para gerar casos de borda complexos.
• Classificação de Entrada Guiada por Pré-condição: As entradas candidatas são rigorosamente classificadas contra pré-condições de verdade absoluta (ground-truth) usando um pipeline de verificação em duas etapas em Lean.
  • Filtro de Sintaxe: Garante que as candidatas sejam expressões Lean sintaticamente válidas.
  • Verificação Bidirecional: Utiliza #guard decide e busca de prova plausível para classificar as entradas como "esperadas" (satisfazendo a pré-condição) ou "inesperadas" (violando-a).
• Síntese Adversarial de Saídas Inesperadas: Esta é a inovação central. Em vez de confiar em LLMs para alucinar saídas incorretas aleatórias, o VeriScale sintetiza implementações adversariais.
  • Um modelo capaz atua como uma "equipe vermelha" (red team), gerando especificações formais para um problema.
  • Outro modelo (ou o mesmo em um papel diferente) tenta criar implementações adversariais projetadas para explorar fraquezas nessas especificações.
  • Essas implementações são executadas em entradas esperadas. Se uma implementação adversarial produzir uma saída que difere da verdade absoluta, mas é falsamente aceita pelas pós-condições geradas, essa saída é retida como uma "saída inesperada" de alta qualidade. Esse processo garante que os casos de teste sejam genuinamente informativos para expor a não solidez das especificações.

2. Redução da Suíte de Teste

Para gerenciar o custo computacional das suítes expandidas, o VeriScale emprega estratégias de redução para destilar o grande pool em suítes compactas, mas discriminativas.

• Redução Preservadora de Limites (para Entradas Inesperadas): Em vez de amostragem aleatória, esta estratégia prioriza entradas que correspondem a violações comuns de limites (por exemplo, contêineres vazios, valores zero, comprimentos incompatíveis). Ela retém exemplos representativos de buckets críticos de limites para garantir a cobertura de violações típicas de pré-condição.
• Redução de Eliminação de Adversário (para Entradas Esperadas): Esta estratégia reaproveita as implementações adversariais sintetizadas na fase de expansão. Cada par de entrada-saída esperado é avaliado com base em quantas implementações "mutantes" (adversariais) ele consegue "eliminar" (ou seja, produzir uma saída diferente). A redução é formulada como um problema de cobertura de conjuntos, selecionando greedymente pares que cobrem o máximo de mutantes previamente não eliminados. Isso garante que a suíte reduzida mantenha a capacidade de distinguir especificações falhas.

Contribuições Principais

1. Framework VeriScale: Os autores propõem um framework geral que alavanca implementações adversariais para impulsionar tanto a expansão sistemática quanto a redução de suítes de teste para geração de código verificável.
2. VERINAPLUS e VERINALITE: O framework é instanciado na benchmark VERINA para criar dois novos conjuntos de dados:
   • VERINAPLUS: Uma benchmark expandida com suítes de teste escalonadas em mais de 83× (especificamente 62,83× para entradas esperadas, 87,79× para saídas inesperadas e 183,08× para entradas inesperadas).
   • VERINALITE: Uma variante leve escalonada em 14×, otimizada por meio das estratégias de redução para manter o poder discriminativo com custos de avaliação mais baixos.
3. Validação Empírica: O artigo demonstra que as benchmarks originais superestimam significativamente as capacidades dos modelos. As benchmarks aprimoradas revelam fraquezas substanciais em LLMs de última geração que estavam anteriormente ocultas.

Resultados Experimentais

Os autores avaliaram oito LLMs de última geração (incluindo GPT-5.5, Claude-Sonnet-4.6 e DeepSeek-V4-Pro) em VERINA, VERINAPLUS e VERINALITE.

• Exposição de Fraquezas do Modelo: As benchmarks aumentadas causaram quedas acentuadas de desempenho. Por exemplo, o GPT-5.5 viu sua pontuação de SpecGen despencar de 68,78% no VERINA para 44,44% no VERINAPLUS, e sua pontuação de CodeGen cair de 96,83% para 86,24%. Isso indica que os casos de teste esparsos da benchmark original permitiam que os modelos passassem sem compreensão real.
• Redução da Incerteza de Avaliação: As suítes de teste expandidas estreitaram significativamente as barras de erro na avaliação de SpecGen. Na benchmark original, resultados de verificação indeterminados criavam grandes lacunas entre os limites superior e inferior (por exemplo, uma lacuna de 13,23% para o Claude-Opus-4.7). No VERINAPLUS, essa ambiguidade foi resolvida, reduzindo a lacuna para 4,76%, fornecendo uma avaliação estatisticamente mais confiável.
• Lacuna de Robustez: Os resultados destacam uma disparidade fundamental: os modelos são significativamente mais proficientes em CodeGen do que em SpecGen. Enquanto as pontuações de CodeGen sofreram declínios moderados, as pontuações de SpecGen sofreram quedas precipitadas, sugerindo que sintetizar especificações formais sólidas e completas permanece um grande gargalo para os LLMs atuais.
• Eficiência da Redução: O VERINALITE alcançou perfis de degradação de desempenho quase idênticos ao VERINAPLUS, mas com sobrecarga computacional significativamente reduzida. O tempo de avaliação para o VERINALITE foi apenas 1,38× (SpecGen) e 1,05× (CodeGen) da linha de base, comparado a 1,80× e 1,50× para a suíte completa do VERINAPLUS.

Significado e Alegações

O artigo afirma que o VeriScale fornece um padrão crucial e altamente confiável para avançar a geração de código verificável baseada em LLM. Ao ir além de testes positivos esparsos para incluir casos negativos sintetizados adversarialmente, o framework oferece uma avaliação mais rigorosa que previne a superestimação das capacidades do modelo.

Os autores posicionam o VeriScale como complementar aos esforços existentes; em vez de introduzir novas tarefas, ele fortalece as benchmarks existentes ao escalar a qualidade e a quantidade dos sinais de teste. O trabalho sublinha a necessidade de escalonamento de testes adversariais para expor a fragilidade dos modelos atuais em tarefas de raciocínio formal.

Limitações Reconhecidas:
Os autores observam que o VeriScale depende da disponibilidade de pré-condições de verdade absoluta e implementações de referência. Além disso, a qualidade das saídas inesperadas sintetizadas é limitada pelas capacidades de raciocínio do LLM atuando como a "equipe vermelha". Finalmente, a fase de construção permanece intensiva em computação, exigindo amostragem massiva de LLM e execuções em Lean.

Trabalho Futuro:
Os autores propõem evoluir o VeriScale para um sistema de reparo em malha fechada para guiar os modelos na correção de especificações falhas. Eles também planejam usar o VeriScale como um motor de dados adversarial para sintetizar corpora de treinamento para modelos de autoformalização dedicados e generalizar o framework para outros backends de verificação, como Dafny.