Can Large Language Models Model Programs Formally?

1. O Problema

A verificação formal é crucial para garantir a correção, segurança e confiabilidade de software, especialmente em infraestruturas críticas. Existem duas abordagens principais: prova de teoremas e model checking (verificação de modelos). Enquanto a prova de teoremas assistida por Grandes Modelos de Linguagem (LLMs) tem avançado significativamente, o model checking permanece subexplorado.

O principal gargalo é a dificuldade de modelagem automática de programas. Converter código de linguagens dinâmicas e ricas (como Python) em especificações formais verificáveis (como TLA+) é tecnicamente desafiador devido a:

• Comportamentos de tempo de execução complexos (aliasing mutável, funções de ordem superior, bibliotecas de terceiros).
• A necessidade de abstrair o código para um espaço de estados finito, mas fiel.
• O equilíbrio delicado entre concretude (para escalabilidade) e abstração (para evitar propriedades vazias ou não sólidas).

Atualmente, não existem benchmarks padronizados para avaliar a capacidade dos LLMs de realizar essa tradução direta de código-fonte para especificações de model checking.

2. Metodologia

Os autores introduzem o Model-Bench, um benchmark e um pipeline completo para avaliar e melhorar a capacidade de modelagem de programas dos LLMs.

A. Construção do Benchmark (Model-Bench)

• Fontes de Dados: O conjunto de dados é derivado de três benchmarks populares de Python: HumanEval, MBPP e LiveCodeBench.
• Processamento de Dados:
  1. Normalização: Coleta e padronização dos problemas.
  2. Simplificação e Reescrita: Filtragem de bibliotecas complexas (mantendo apenas typing e math), reescrita de recursos de linguagem difíceis (recursão, compreensão de listas, classes) e exclusão de tipos complexos.
  3. Execução: Validação de que os programas filtrados funcionam corretamente.
• Resultado Final: Um conjunto de 400 programas Python (reduzidos de um total inicial de 683 após filtragem) cobrindo níveis de dificuldade de fácil a difícil, com 1.639 casos de teste associados.

B. Pipeline de Avaliação

• Alvo: Os LLMs devem gerar especificações em TLA+ (Temporal Logic of Actions), que são verificadas pelo verificador TLC.
• Abordagens de Prompt:
  1. Código Original: Prompt com o código Python original.
  2. Código Transformado: O código Python é convertido em um Grafo de Fluxo de Controle (CFG) e reescrito em um padrão de máquina de estados (usando uma variável pc para controle de fluxo), tornando a estrutura mais similar ao TLA+.
• Métricas de Avaliação:
  • Runnable@k: A proporção de modelos gerados que passam na verificação do TLC sem falhas (baseado em Pass@k).
  • Similaridade de Estados: Uma métrica formal que compara os estados observados no modelo gerado pelo LLM com os estados do modelo "oráculo" (verificado manualmente), garantindo que a semântica seja preservada.

C. Transformação de Código

Para mitigar as dificuldades de abstração, os autores desenvolveram um transformador que converte Python para uma representação intermediária baseada em máquinas de estados (CFG), facilitando a tradução para TLA+ ao explicitar transições e blocos básicos.

3. Contribuições Principais

1. Model-Bench: O primeiro benchmark generalista focado na geração automática de especificações de model checking (TLA+) a partir de código-fonte (Python) usando LLMs.
2. Pipeline de Transformação: Uma abordagem inovadora que utiliza a transformação de código (Python para máquina de estados) para facilitar a tarefa de modelagem dos LLMs.
3. Avaliação Abrangente: Experimentos extensivos com múltiplos modelos (DeepSeek, Qwen, Gemma, Llama) e análises detalhadas de falhas, fornecendo direções para pesquisas futuras.

4. Resultados Chave

Os experimentos revelaram limitações significativas, mas também insights importantes:

• Desempenho Geral (RQ1):

  • Mesmo os melhores modelos (DeepSeek-V3) alcançaram apenas 66,25% de taxa de Runnable@3 (modelos executáveis) com few-shot learning.
  • A similaridade de estados média foi de 49,55%, indicando que muitos modelos que passam na verificação não capturam a semântica exata do programa original.
  • Modelos menores (ex: Llama-3.1-8B) tiveram desempenho quase nulo (Runnable@1 ~0%) sem exemplos de few-shot.
  • Aprendizado Few-shot é essencial, melhorando a taxa de sucesso em média de 9,25% (zero-shot) para 26,82% (few-shot).

• Eficácia da Transformação de Código (RQ2):

  • O uso de código transformado (padrão de máquina de estados) aumentou significativamente a similaridade de estados (ex: +18,99% para o DeepSeek-V3), pois guiou o LLM para uma estrutura mais alinhada com TLA+.
  • No entanto, houve uma leve queda na taxa de Runnable@k (devido ao aumento do comprimento do contexto e complexidade), mas a combinação de prompts (original + transformado) gerou o maior número total de modelos válidos.

• Impacto da Complexidade (RQ3):

  • A dificuldade de modelagem não está correlacionada com a dificuldade algorítmica do problema (ex: Hard vs. Easy em LiveCodeBench).
  • Existe uma correlação negativa forte com a complexidade sintática: maior complexidade ciclomática, profundidade de loops aninhados e número de variáveis resultam em taxas de sucesso menores.

• Análise de Casos de Falha (RQ4):

  • Erros de Compilação: Uso de operadores desconhecidos no TLA+ (ex: funções de bibliotecas Python que não existem em TLA+).
  • Erros de Runtime: Falhas na compreensão de especificações de linguagem, como a diferença entre indexação baseada em 0 (Python) e baseada em 1 (TLA+).
  • Erros de Asserção: Omissão de chamadas de função ou lógica de controle (ex: usar um limite constante em vez do tamanho dinâmico de um array).

5. Significado e Conclusão

O trabalho demonstra que, embora os LLMs atuais tenham potencial para auxiliar na verificação formal, eles ainda enfrentam barreiras significativas na modelagem precisa de programas complexos. O Model-Bench estabelece uma base crítica para o desenvolvimento de futuros LLMs com capacidades de raciocínio mais sofisticadas.

A descoberta de que a transformação de código pode melhorar a fidelidade semântica sugere que pré-processar o código para formas mais "formais" é uma estratégia viável para superar as limitações atuais dos modelos. O estudo conclui que a dificuldade de modelagem reside mais na complexidade estrutural do código (loops, variáveis) do que na lógica algorítmica em si, apontando para a necessidade de LLMs que entendam melhor a estrutura de controle e a semântica de linguagens formais.