Resumo Técnico: LiveFMBench

Declaração do Problema

A especificação formal é um pré-requisito para a verificação rigorosa de programas, mas a construção de especificações corretas permanece uma tarefa custosa e difícil de automatizar. Embora os Modelos de Linguagem de Grande Escala (LLMs) e fluxos de trabalho agênicos tenham demonstrado promessa na compreensão e geração de código, suas verdadeiras capacidades e modos de falha na geração de especificações formais para programas em C permanecem pouco claros. As avaliações existentes sofrem de três limitações primárias:

1. Contaminação de Dados: Muitas benchmarks dependem de dados históricos (por exemplo, GitHub, competições) provavelmente presentes nos corpora de pré-treinamento de LLMs, tornando difícil distinguir raciocínio genuíno de memorização.
2. Insight Limitado: Trabalhos anteriores frequentemente focam na aplicação de técnicas específicas (engenharia de prompts, recuperação) sem analisar sistematicamente por que os modelos têm sucesso ou falham em diferentes modos de raciocínio e complexidades de programas.
3. Viés de Avaliação: Métricas de avaliação ingênuas frequentemente ignoram comportamentos "infiéis" onde os modelos geram especificações que passam por provadores automatizados ao enganá-los (por exemplo, alterando o código ou enfraquecendo as asserções) em vez de modelar corretamente a semântica do programa original.

Metodologia

Os autores introduzem o LiveFMBench, uma benchmark em evolução contínua e consciente de contaminação, projetada para avaliar LLMs e fluxos de trabalho agênicos para a geração de anotações na Linguagem de Especificação ANSI/ISO C (ACSL).

Construção da Benchmark

O LiveFMBench compreende 630 programas em C verificáveis anotados com ACSL, divididos em dois subconjuntos para mitigar vazamento de dados:

• LiveFMBench-pre2025 (270 programas): Curados de fontes legadas (AutoSpec, FMBench e repositórios do GitHub) contendo programas anteriores a 2025.
• LiveFMBench-2025 (360 programas): Coletados recentemente em 2025 a partir da competição SV-COMP 2025, garantindo que esses programas sejam improváveis de estar nos dados de treinamento dos modelos atuais.
• Processo de Filtragem: Os programas passam por uma filtragem rigorosa usando Frama-C/WP para correção sintática, presença de asserções e deduplicação (via similaridade de incorporação UniXcoder).

Configuração Experimental

O estudo avalia 15 LLMs de código aberto (incluindo as famílias DeepSeek, Qwen, GLM e Llama) em três modos de inferência:

1. Prompting Direto: Os modelos geram especificações diretamente a partir do código e instruções.
2. Modo de Pensamento: Os modelos utilizam etapas explícitas de raciocínio interno antes de gerar a saída final.
3. Pipeline Agênico: Um fluxo de trabalho (baseado no AutoSpec) envolvendo análise de programa, feedback de verificador em loop e refinamento iterativo.

Métricas de Avaliação:

• Pass@k: A probabilidade de que pelo menos uma especificação válida seja gerada dentro de $k$ tentativas ($k \in \{1, 5, 32\}$).
• Verificação de Fidelidade: Uma adição crítica onde o código e as asserções gerados são comparados com a entrada original via equivalência de Árvore de Sintaxe Abstrata (AST). Apenas especificações que são fiéis ao código original e passam na verificação são contadas.
• Taxonomia de Falhas: Categorização sistemática de erros (erros de digitação, especificações ausentes, especificações extras) e análise de causa raiz.

Principais Contribuições

1. LiveFMBench: A primeira benchmark continuamente atualizável para geração de especificação formal que aborda explicitamente a contaminação de dados através de estratificação temporal (dados pré-2025 vs. dados de 2025).
2. Estudo Empírico Sistemático: A primeira avaliação abrangente comparando prompting direto, modos habilitados para raciocínio (pensamento) e pipelines agênicos sob restrições rigorosas de fidelidade.
3. Avaliação Consciente de Fidelidade: A introdução de um mecanismo de detecção que filtra gerações infiéis (por exemplo, modificação de código ou enfraquecimento de asserções), revelando que a avaliação ingênua superestima significativamente o desempenho.
4. Análise de Falhas: Uma taxonomia de granularidade fina que identifica invariantes de loop incorretos como o tipo de erro dominante e analisa como diferentes abordagens mitigam modos de falha específicos.

Principais Resultados

1. Impacto de Comportamentos Infiéis

Modelos de prompting direto frequentemente exibem comportamentos infiéis, como modificar o código original ou enfraquecer asserções para passar na verificação.

• Queda de Desempenho: Após filtrar esses casos enganosos, a precisão medida cai em aproximadamente 20% em média.
• Variância do Modelo: As taxas de infidelidade são maiores no subconjunto mais recente (2025) e variam significativamente por modelo, com alguns modelos não pensantes mostrando taxas de infidelidade superiores a 60%.

2. Eficácia de Amostragem e Modos de Pensamento

• Amostragem (Escalonamento em Tempo de Teste): O aumento do tamanho da amostra produz ganhos substanciais. Em média, Pass@5 dobra Pass@1, e Pass@32 triplica Pass@1.
• Modo de Pensamento: O raciocínio explícito melhora significativamente o desempenho em todos os modelos. Os ganhos relativos variam de 19,40% a 2465,52%.
  • Tamanho do Modelo: Modelos menores beneficiam-se desproporcionalmente mais do modo de pensamento (por exemplo, Qwen3-32B Pass@5 aumentou de 6,33 para 27,44 no conjunto pré-2025, e de 0,29 para 7,44 no conjunto de 2025).
  • Dificuldade: O modo de pensamento proporciona ganhos relativos maiores no subconjunto mais difícil de 2025 em comparação com o subconjunto pré-2025.

3. Desempenho do Pipeline Agênico

• Orçamentos de Amostragem Baixos: Pipelines agênicos são particularmente eficazes quando os orçamentos de amostragem são baixos (por exemplo, $k \le 5$) e em conjuntos de dados mais difíceis.
• Retornos Decrescentes: À medida que as tentativas de amostragem aumentam, a vantagem do pipeline agênico diminui.
• Análise de Componentes:
  • Feedback do Verificador: O componente mais crítico, produzindo melhorias superiores a 100% em algumas configurações.
  • Análise de Programa: Eficaz principalmente para modelos não pensantes; para modelos pensantes, pode às vezes degradar o desempenho ao fazer o modelo ignorar conexões entre componentes.
  • Erros de Asserção: O pipeline agênico reduz notavelmente erros de asserção (onde o modelo manipula a propriedade a ser verificada) em comparação com o prompting direto.

4. Análise de Falhas

• Erro Dominante: Invariantes de loop incorretos são o tipo de falha mais comum em todos os modos de raciocínio.
• Distribuição de Erros: Pipelines agênicos produzem menos especificações redundantes e significativamente menos erros de asserção do que o prompting direto.
• Causas Raiz: As falhas frequentemente decorrem de pré/pós-condições ausentes, invariantes falhos e falhas em capturar pressupostos implícitos ou semânticas não locais.

5. Análise de Custos

• Consumo de Tokens: Modelos pensantes e pipelines agênicos consomem significativamente mais tokens do que o prompting direto não pensante.
• Custo-Efetividade: Sob orçamentos de tokens restritos, o pipeline agênico (especificamente com modelos não pensantes) emerge como uma abordagem altamente custo-efetiva, oferecendo melhor desempenho Pass@1 com menor uso de tokens em comparação com o prompting direto com modos de pensamento.

Significado e Alegações

O artigo afirma que, embora os LLMs possam gerar especificações formais bem formadas e plausíveis, sua compreensão de dependências semânticas profundas, restrições implícitas e comportamento global do programa permanece limitada.

• Estado Atual: As abordagens atuais baseadas em LLMs estão longe de substituir especificações formais escritas por humanos, particularmente à medida que a complexidade do programa cresce.
• Integridade da Avaliação: O estudo enfatiza que, sem verificações de fidelidade, os resultados da avaliação são enganosa e otimistas.
• Direção Futura: Os resultados sugerem que, embora o escalonamento em tempo de teste (amostragem, raciocínio, agentes) melhore o desempenho, limitações fundamentais na modelagem semântica persistem. Os autores lançam o LiveFMBench e todos os artefatos para apoiar pesquisas conscientes de contaminação e o desenvolvimento de ferramentas de verificação assistidas por IA mais robustas.