Towards Language Model Guided TLA+ Proof Automation

Título: Rumo à Automação de Provas em TLA+ Guiada por Modelos de Linguagem

Autores: Yuhao Zhou e Stavros Tripakis (Northeastern University)

1. Problema e Motivação

A verificação formal é crucial para garantir a correção de sistemas críticos, especialmente sistemas distribuídos. A linguagem TLA+ (Temporal Logic of Actions) é amplamente utilizada na indústria (Amazon, Microsoft, Intel) para especificação e verificação. No entanto, a construção de provas formais em TLA+ permanece um gargalo significativo devido à sua complexidade e à necessidade de expertise humana.

O desafio central abordado neste trabalho é a automação da geração de provas em TLA+. Diferentemente de provadores baseados em táticas (como Lean ou Coq), que transformam estados de prova sequencialmente, o sistema de prova TLA+ (TLAPS) utiliza uma estrutura hierárquica. As provas são organizadas como árvores de alegações (claims) e sub-alegações, onde o usuário deve descobrir e introduzir passos intermediários (lemas) para estabelecer o objetivo principal.

A aplicação direta de Modelos de Linguagem Grandes (LLMs) para gerar provas completas em TLA+ enfrenta dois obstáculos principais:

1. Erros de Sintaxe: LLMs tendem a gerar código TLA+ com erros sintáticos frequentes, impedindo a verificação automática pelo TLAPS.
2. Geração Monolítica: Tentar gerar a prova inteira de uma vez impede a verificação incremental; erros iniciais propagam-se, e a correção torna-se difícil.

2. Metodologia: LMGPA

Os autores propõem o LMGPA (Language Model Guided Proof Automation), uma abordagem que combina a capacidade de raciocínio dos LLMs com a verificação rigorosa de provadores simbólicos. A inovação central não é pedir ao LLM para escrever a prova, mas sim pedir que ele guie a decomposição da prova.

Arquitetura e Algoritmo

O sistema opera através de um algoritmo recursivo de geração de provas hierárquicas:

1. Tentativa de Prova Automática (Auto Proof): Para um objetivo dado, o sistema primeiro tenta provar diretamente usando provadores simbólicos (backend do TLAPS como Z3, Zenon, Isabelle) com diretivas simples como OBVIOUS ou BY DEF. Se funcionar, o processo termina.
2. Decomposição Guiada por LLM: Se a prova automática falhar, o LLM é acionado para decompor a alegação complexa em um conjunto de sub-alegações mais simples.
   • Estrutura Normalizada: Para mitigar erros de sintaxe, o LLM não gera código TLA+ livre. Ele é restringido a gerar uma estrutura normalizada (lista de suposições e um único objetivo) usando apenas caracteres ASCII e notações específicas. O sistema então converte essa saída normalizada em comandos TLA+ válidos (ASSUME... PROVE...).
3. Validação e Feedback:
   • O sistema verifica se as sub-alegações geradas, em conjunto, estabelecem a alegação pai.
   • Se a decomposição for inválida ou conter erros, o TLAPS fornece feedback de erro ao LLM, que tenta uma nova decomposição.
4. Recursão: O processo repete-se recursivamente para cada sub-alegação até que todas sejam provadas diretamente pelos provadores simbólicos.
5. Montagem: O sistema ensambla as provas validadas em uma estrutura hierárquica completa de TLA+.

3. Contribuições Principais

• Abordagem de Decomposição Normalizada: A principal contribuição é a restrição dos LLMs para gerar apenas a estrutura lógica das sub-alegações (decomposição) em um formato normalizado, em vez de provas completas. Isso reduz drasticamente os erros de sintaxe, que são a principal causa de falha em abordagens diretas.
• Adaptação à Estrutura Hierárquica do TLA+: O método respeita a filosofia de prova do TLA+ (descoberta de lemas intermediários), diferindo fundamentalmente das abordagens baseadas em táticas usadas em Lean/Coq.
• Benchmarks e Dataset: Os autores criaram um conjunto de benchmarks com 119 teoremas, incluindo:
  • 93 teoremas matemáticos adaptados de coleções como miniF2F e ProofNet.
  • 26 provas de indutividade de invariantes para protocolos distribuídos.
  • Nota: Devido à falta de formalizações TLA+ nessas coleções, os teoremas foram traduzidos manualmente para TLA+ para garantir a correção.
• Sistema Integrado: Uma implementação funcional que orquestra LLMs (via LangChain) e o TLAPS para verificação.

4. Resultados Experimentais

Os experimentos foram realizados com diversos LLMs de última geração (Claude 3.7, GPT-5, o3-mini, Gemini, DeepSeek) em comparação com três baselines:

1. TLAPS OBVIOUS: Tentativa direta de prova automática.
2. SAPG: Geração automática de provas simbólicas (heurística).
3. DLPG: Geração direta de provas completas pelo LLM.

Principais Achados:

• Taxa de Sucesso: O LMGPA superou consistentemente todas as baselines.
  • No conjunto de protocolos distribuídos, o LMGPA alcançou taxas de sucesso entre 38% e 50%, enquanto a DLPG (geração direta) ficou entre 0% e 15%.
  • No conjunto matemático, o LMGPA alcançou 53% a 59%, contra 17% a 29% da DLPG.
• Redução de Erros Sintáticos: A análise de validade sintática mostrou que a DLPG falha massivamente devido a erros de sintaxe (ex: 0,2% a 20% de validade). Em contraste, o LMGPA, ao gerar apenas decomposições normalizadas, atingiu taxas de validade sintática de 63% a 86%.
• Eficiência: O LMGPA reduziu significativamente o número de consultas ao LLM e o tempo total de execução em comparação com a tentativa de gerar provas completas repetidamente.
• Qualidade das Provas: As provas geradas são estruturalmente corretas e verificáveis, embora por vezes mais verbosas ou com sub-alegações menos "elegantes" do que as feitas por humanos (ex: introdução de lemas triviais).

5. Significado e Conclusão

O trabalho demonstra que a automação de provas em TLA+ é viável ao alinhar a capacidade dos LLMs com a estrutura específica da linguagem. A chave do sucesso foi não tentar substituir o provador simbólico, mas usá-lo como um verificador rigoroso, enquanto o LLM atua como um "arquiteto" que descobre os passos intermediários (lemas).

Implicações Futuras:

• O método abre caminho para tornar a verificação formal de sistemas distribuídos mais acessível.
• Trabalhos futuros incluem o fine-tuning de modelos específicos para TLA+, o uso de técnicas de Retrieval-Augmented Generation (RAG) para melhorar a qualidade das decomposições e a criação de benchmarks livres de vazamento de dados.

Em resumo, o LMGPA representa um avanço significativo ao resolver o problema da sintaxe e da estrutura hierárquica, provando que LLMs podem ser ferramentas eficazes para guiar a descoberta de provas em sistemas formais complexos como o TLA+.