Resumo Técnico: VeriContest

Declaração do Problema

Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham demonstrado proficiência na geração de código executável a partir de linguagem natural, suas saídas carecem de garantias formais de correção. Abordagens existentes baseadas em testes apenas amostram o comportamento do programa e não podem garantir a ausência de erros funcionais ou defeitos de segurança. A verificação formal oferece uma alternativa mais robusta, exigindo provas verificáveis por máquina de que o código satisfaz especificações formais. No entanto, o progresso na "geração de código verificável" — onde um modelo deve produzir código, especificações formais e provas simultaneamente — é impedido pela falta de benchmarks rigorosos. Os benchmarks atuais são frequentemente pequenos, focam em estágios isolados do pipeline (por exemplo, apenas código ou apenas provas), carecem de provas de verdade fundamental (ground-truth) ou visam configurações de verificação desconectadas do desenvolvimento de software mainstream.

Metodologia

Os autores apresentam o VeriContest, um benchmark composto por 946 problemas de programação competitiva provenientes do LeetCode e do Codeforces, especificamente projetado para geração de código verificável em Rust utilizando o framework de verificação Verus.

Pipeline de Construção do Benchmark

O VeriContest é construído por meio de um pipeline de três fases para garantir alta qualidade e escala:

1. Fase I (Construção Manual): Especialistas construíram manualmente 91 problemas "semente". Para cada um, escreveram especificações formais (pré-condições e pós-condições), código Rust aceito pelo juiz e provas verificadas pelo Verus. Essas especificações foram rigorosamente validadas quanto à correção (qualquer solução correta satisfaz a especificação) e completude (qualquer solução que satisfaz a especificação é correta).
2. Fase II (Expansão Semi-Automatizada): Um agente LLM (respaldado pelo GPT-5.3-Codex) expandiu o benchmark para 946 problemas. Esta fase empregou um processo de revisão "humano-no-loop". O agente filtrou problemas que exigiam recursos não suportados do Rust (por exemplo, aritmética de ponto flutuante, estruturas de dados complexas) e gerou especificações, código e provas. Especialistas humanos verificaram a saída por meio de aceitação no juiz online, revisão manual da especificação e verificação independente pelo Verus.
3. Fase III (Geração e Validação de Casos de Teste): Para validar a completude das pós-condições, os autores geraram suites de testes positivos e negativos.
   • Testes Positivos: Gerados pela síntese de programas geradores verificados pelo Verus que produzem entradas válidas.
   • Testes Negativos: Gerados via teste de mutação (mutação semântica, sintática e de saída direta) para criar entradas emparelhadas com saídas incorretas.
   • Post2Exe: Uma ferramenta inovadora que converte pós-condições suportadas do Verus em programas Rust executáveis. Estes são executados contra casos de teste negativos para detectar e sinalizar automaticamente pós-condições incompletas (aquelas que aceitam saídas incorretas), que são então enviadas de volta para revisão.

Protocolo de Avaliação

O VeriContest suporta avaliação tanto isolada quanto composicional em quatro tarefas principais:

• SpecGen: Geração de especificações formais a partir de linguagem natural.
• CodeGen: Geração de código executável a partir de linguagem natural, especificações ou ambos.
• ProofGen: Geração de provas Verus dada uma especificação e um código.
• End-to-End: Geração do programa verificado completo (especificação, código e prova) a partir de uma descrição em linguagem natural.

A avaliação mede a precisão pass@1, com métricas adicionais para reparo de provas (repair@k) e amostragem (pass@k).

Contribuições Principais

1. Benchmark VeriContest: Um conjunto de dados em grande escala de 946 problemas de programação competitiva com especificações Verus validadas por especialistas, código Rust aceito pelo juiz, provas Verus de verdade fundamental e suites de testes positivos/negativos abrangentes.
2. Pipeline de Construção: Uma metodologia escalável de três fases combinando criação manual de sementes, expansão semi-automatizada com revisão humana e validação automatizada baseada em testes da completude das pós-condições via Post2Exe.
3. Framework de Avaliação Modular: Um protocolo que isola a geração de especificação, código e prova, enquanto também avalia a síntese end-to-end, permitindo uma análise granular dos gargalos.
4. Análise Empírica: Uma avaliação de dez LLMs de última geração (incluindo GPT-5.5, Claude Opus 4.7 e DeepSeek V4) revelando lacunas significativas de desempenho entre a codificação padrão e a geração de código verificável.

Resultados

A avaliação de dez modelos de última geração no VeriContest revela um declínio acentuado no desempenho à medida que a complexidade da tarefa aumenta, passando da geração de código para a verificação completa:

• Geração de Código (CodeGen): Os modelos performam relativamente bem. O modelo mais forte, GPT-5.5, alcança 92,18% de precisão na geração de código a partir de linguagem natural. No entanto, o desempenho cai significativamente quando a entrada é apenas uma especificação formal (67,65%), sugerindo uma incompatibilidade na distribuição de treinamento, onde os modelos estão mais familiarizados com enunciados de problemas em linguagem natural do que com restrições lógicas formais.
• Geração de Especificação (SpecGen): O desempenho cai drasticamente. O GPT-5.5 alcança apenas 48,31% na geração de especificação a partir de linguagem natural, e modelos de código aberto performam significativamente pior (por exemplo, Qwen 3.6 em 0,32%). Isso indica que os LLMs estão muito menos familiarizados com a sintaxe e semântica de especificações formais do que com código.
• Geração de Provas (ProofGen): Este é identificado como o principal gargalo. Mesmo com especificações e código de verdade fundamental fornecidos, o GPT-5.5 alcança apenas 13,95% de precisão. A maioria dos modelos permanece abaixo de 8%.
• End-to-End: A taxa de sucesso para gerar um programa totalmente verificado do zero é extremamente baixa. O GPT-5.5 atinge apenas 5,29%. Os autores observam que o sucesso end-to-end exige que a especificação, o código e a prova se alinhem perfeitamente; uma falha em qualquer componente único causa a falha de todo o pipeline.

Análise de Erros:

• CodeGen: Os erros são dominados por saídas incorretas para modelos fortes, mas mudam para erros de sintaxe quando especificações formais estão envolvidas.
• ProofGen: O modo de falha dominante é Falha de Verificação (a prova não satisfaz o verificador) e Modificação de Especificação/Código (modelos alterando o código/especificação fornecido em vez de apenas adicionar provas).
• SpecGen: Os erros são fortemente dominados por erros de sintaxe no Verus, seguidos por incompatibilidades nas pré/pós-condições.

Significado e Afirmações

O artigo afirma que o VeriContest estabelece uma plataforma rigorosa para medir e treinar sistemas futuros capazes de gerar código com correção verificável por máquina. Os autores afirmam que:

• A geração de provas e especificações são os gargalos centrais para os LLMs atuais no pipeline de geração de código verificável.
• Existe uma lacuna substancial entre a capacidade de um modelo escrever código e sua capacidade de verificá-lo formalmente.
• O sucesso end-to-end é atualmente limitado não apenas pela geração de código, mas pela dificuldade de alinhar especificações, código e provas em um todo consistente.
• O benchmark serve como uma fonte de supervisão para treinar modelos na geração de código verificável, indo além da simples correção funcional para garantias formais.

Os autores permanecem modestos quanto ao escopo, reconhecendo que o VeriContest é limitado a Rust/Verus e problemas de programação competitiva, e ainda não cobre código de sistemas, protocolos distribuídos ou outros frameworks de verificação como Dafny ou Lean. Eles sugerem que trabalhos futuros devem expandir para mais linguagens e domínios à medida que as ferramentas e as capacidades dos modelos melhoram.