Evaluating LLM-Generated ACSL Annotations for Formal Verification

Título e Contexto

O artigo avalia empiricamente a capacidade de ferramentas de análise formal de gerar e verificar automaticamente especificações ACSL (ANSI/ISO C Specification Language) para programas em C, sem assistência humana ou baseada em aprendizado. O estudo foca na comparação entre métodos tradicionais baseados em regras e novas abordagens utilizando Grandes Modelos de Linguagem (LLMs).

1. O Problema

• Desafio da Especificação Formal: Embora as especificações formais sejam cruciais para sistemas de software verificáveis e confiáveis, a geração de especificações precisas e verificáveis para programas C do mundo real continua sendo um gargalo.
• Limitações Atuais: Métodos formais são caros e difíceis de aplicar. A escrita e manutenção de especificações são complexas, e técnicas puramente simbólicas lutam com bases de código modernas e em evolução.
• Oportunidade dos LLMs: Com o avanço da IA, existe a promessa de que LLMs possam automatizar a geração de especificações. No entanto, falta evidência empírica robusta sobre a qualidade, estabilidade e viabilidade de verificação automática dessas especificações geradas por IA, especialmente em comparação com ferramentas tradicionais.

2. Metodologia

O estudo foi conduzido como uma análise controlada e reprodutível:

• Conjunto de Dados: Utilizou-se um novo conjunto de dados lançado em novembro de 2025 (CASP), contendo 506 programas C. O conjunto foi filtrado para reter apenas 355 arquivos C puros e completos, removendo arquivos vazios ou incompletos.
• Sistemas de Geração de ACSL Comparados: Cinco abordagens foram testadas para gerar as anotações:
  1. Script Python Baseado em Regras: Uma abordagem determinística simples.
  2. Plugin RTE do Frama-C: Uma ferramenta de detecção de erros em tempo de execução que gera contratos automaticamente.
  3. DeepSeek-V3.2: Um modelo de linguagem grande (LLM).
  4. GPT-5.2: Um modelo de linguagem grande.
  5. OLMo 3.1 32B Instruct: Um modelo de linguagem aberto.
• Ambiente de Verificação:
  • Todas as especificações geradas foram verificadas usando o plugin WP (Weakest Precondition) do Frama-C.
  • Foram utilizados múltiplos solucionadores SMT (Satisfiability Modulo Theories) para testar a sensibilidade: Alt-Ergo, CVC4, CVC5 e Z3.
  • A análise incluiu métricas de sucesso de prova, contagem de timeouts (tempo esgotado) e tempos de execução (Qed time).

3. Contribuições Principais

• Avaliação Empírica Direta: Fornece uma comparação direta entre anotações geradas por ferramentas (Rule-based/RTE) e por LLMs em um conjunto de dados moderno e padronizado.
• Análise de Estabilidade do Solucionador: Vai além da simples taxa de sucesso, analisando a sensibilidade dos solucionadores SMT a diferentes tipos de especificações (variabilidade de tempo, dispersão e robustez).
• Benchmarks Reprodutíveis: O estudo estabelece uma linha de base concreta para futuras pesquisas em síntese de especificações assistida por aprendizado, disponibilizando logs e scripts publicamente.

4. Resultados Chave

A. Desempenho Geral e Taxas de Sucesso

• Ferramentas Tradicionais (Python Script e RTE): Apresentaram o melhor desempenho. O plugin RTE atingiu taxas de sucesso de prova próximas a 99% com baixíssimos timeouts, demonstrando contratos robustos e amigáveis à verificação. O script baseado em regras também teve alto desempenho (~72-73% de sucesso médio, mas com alta consistência).
• LLMs:
  • DeepSeek: Mostrou o melhor desempenho entre os LLMs, com taxas de sucesso próximas às ferramentas tradicionais (média de ~94-95%), mas com maior variabilidade.
  • GPT-5 e OLMo3: Apresentaram taxas de sucesso menores (GPT-5 ~81%, OLMo3 ~83%) e sofreram significativamente mais com timeouts, especialmente com o solucionador Alt-Ergo.

B. Estabilidade e Sensibilidade dos Solucionadores

• RTE: Gerou especificações que resultaram nos menores tempos de verificação e menor variabilidade, confirmando sua natureza conservadora e estável.
• LLMs (Geração Heterogênea): As especificações geradas por GPT-5 e DeepSeek introduziram maior complexidade e heterogeneidade. Isso levou a:
  • Aumento significativo nos tempos de execução (Qed time).
  • Maior dispersão (desvio padrão) nos tempos de prova.
  • Maior frequência de timeouts, indicando que as especificações eram semanticamente mais difíceis ou ambíguas para os solucionadores.
• Comparação de Solucionadores:
  • CVC4 e CVC5: Demonstraram maior estabilidade e consistência geral, especialmente em entradas mais simples.
  • Alt-Ergo: Sofreu com as maiores taxas de timeout em cenários complexos (especialmente com GPT e DeepSeek).
  • Z3: Mostrou variabilidade central menor, mas flutuações mais amplas em entradas complexas.

C. Trade-off: Expressividade vs. Estabilidade

O estudo identificou um trade-off fundamental:

• Técnicas disciplinadas e baseadas em estrutura (RTE, Scripts) produzem especificações rápidas, previsíveis e altamente consistentes.
• LLMs aumentam a expressividade e a riqueza das especificações, mas isso correlaciona-se diretamente com redução na estabilidade do solucionador, tempos de verificação mais longos e maior imprevisibilidade.

5. Significado e Conclusões

• Viabilidade Limitada da Automação Total: Embora os LLMs possam gerar especificações sintaticamente válidas e, em alguns casos (como DeepSeek), semanticamente fortes, eles ainda não substituem ferramentas tradicionais para verificação em larga escala devido à instabilidade introduzida.
• Necessidade de Refinamento: A geração de especificações por LLMs requer refinamento adicional para melhorar a consistência e a compatibilidade com solucionadores SMT.
• Futuro da Pesquisa: O trabalho sugere que o caminho ideal não é a substituição pura, mas a criação de fluxos de trabalho híbridos que combinem a riqueza semântica dos LLMs com a robustez das ferramentas de análise estática tradicionais.
• Impacto: Os resultados desafiam a ideia de que LLMs são imediatamente superiores para tarefas de verificação formal, destacando que a "qualidade" de uma especificação não deve ser medida apenas pela sua capacidade de passar em uma prova, mas também pela eficiência e estabilidade do processo de verificação.

Em resumo, o artigo fornece evidências concretas de que, embora os LLMs sejam promissores para a geração de especificações, as ferramentas baseadas em regras e análise estática (como o RTE do Frama-C) continuam sendo superiores em termos de confiabilidade e eficiência para verificação formal automatizada.