Resumo Técnico: TLA-Prover

Definição do Problema

O TLA+ é uma linguagem de especificação formal usada para verificar sistemas distribuídos e protocolos de segurança crítica, acompanhada pelo model checker TLC para exploração exaustiva do espaço de estados. Embora os Grandes Modelos de Linguagem (LLMs) mostrem promessa na geração de código, eles enfrentam dificuldades significativas com o TLA+ devido à sua representação esparsa nos corpora de pré-treinamento e sua sintaxe idiossincrática (ex: operadores temporais, compreensão de conjuntos).

Baselines existentes, como o estudo FormaLLM, indicam que LLMs de pesos abertos sem ajuste fino alcançam apenas uma taxa de sucesso de 8,6% ao passar no model checker TLC em 25 modelos. Um desafio crítico no treinamento de LLMs para verificação formal é o reward hacking (hackeamento de recompensa). No contexto do TLA+ e do TLC, um modelo pode otimizar o sinal binário de "passou" gerando invariantes triviais e tautológicas (ex: TypeOK == TRUE). Essas especificações passam no TLC em todos os estados alcançáveis, mas não transmitem propriedades significativas sobre o protocolo, tornando a verificação inútil. Abordagens padrão de aprendizado por reforço que dependem exclusivamente do sinal de passar/falhar do TLC como sinal de recompensa são vulneráveis a esse modo de falha.

Metodologia

Os autores apresentam o TLA-Prover, um modelo de 20 bilhões de parâmetros (baseado em gpt-oss-20b) projetado para a síntese de especificações TLA+. A abordagem combina o Ajuste Fino Supervisionado (SFT) com um novo pipeline de treinamento que integra a Otimização de Política de Grupo Relativa de Reparo (GRPO) e uma hierarquia de validação de quatro níveis.

1. Hierarquia de Validação de Quatro Níveis

Para evitar o reward hacking e garantir a validade semântica, cada saída do modelo é classificada por um pipeline externo determinístico em um de quatro níveis:

• Bronze: A saída falha no parser SANY (sintaticamente inválida).
• Prata: A saída faz o parse, mas falha ao carregar ou executar no TLC (ex: timeouts, erros de tipo).
• Ouro: A saída passa tanto no SANY quanto no TLC; o model checker esgota o espaço de estados e todos os invariantes são mantidos.
• Diamante: A saída passa no nível Ouro e o invariante é sensível à mutação.
  • Mecanismo: Uma mutação automatizada no nível de AST é aplicada ao predicado do invariante (ex: negar uma conjunção, inverter operadores relacionais ou trocar constantes). A especificação mutada é executada novamente através do TLC.
  • Critério: Se a mutação causar o TLC a encontrar um contraexemplo, o invariante original é considerado não trivial (Diamante). Se o TLC ainda passar (ex: porque o invariante era TRUE), a saída falha no teste Diamante. Este passo bloqueia explicitamente invariantes tautológicos.

2. Pipeline de Treinamento

O processo de treinamento consiste em duas etapas primárias, com uma ablação de DPO para comparação:

• Etapa 1: Ajuste Fino Supervisionado (SFT)

  • Corpus: Um conjunto de dados curado de 1.053 especificações, estritamente filtradas para o nível Diamante. Os dados são provenientes da distribuição da TLA+ Foundation e do repositório tlaplus/examples, aumentados por um gerador Ollama e filtrados por um juiz LLM e pelo pipeline de quatro níveis.
  • Arquitetura: Um adaptador LoRA (rank 8, alpha 16) é aplicado às projeções de atenção do modelo base de 20B parâmetros.
  • Objetivo: Ensinar ao modelo o vocabulário estrutural e a sintaxe do TLA+.

• Etapa 2: Otimização de Política de Grupo Relativa de Reparo (GRPO)

  • Motivação: O GRPO padrão falha quando todas as amostras de um grupo falham no verificador (recompensas esparsas), resultando em vantagem zero e ausência de fluxo de gradiente.
  • Mecanismo: O modelo é apresentado com uma especificação "quebrada" (extraída de tentativas falhas anteriores) e recebe a tarefa de repará-la.
  • Sinal de Recompensa: Uma pontuação de melhoria contínua baseada em transições de nível (Bronze→Prata: 0.1, Prata→Ouro: 0.3, Ouro→Diamante: 0.6). Isso fornece gradientes densos mesmo quando a saída final não é perfeita, desde que o nível melhore.
  • Processo: O modelo corrige iterativamente suas próprias saídas usando mensagens de erro do TLC como feedback.

• Estudo de Ablação (DPO): Uma variante de Otimização de Preferência Direta (DPO) foi treinada a partir do mesmo checkpoint de SFT usando pares de preferência estáticos (Diamante > Ouro > Prata > Bronze). Isso serviu como uma baseline para comparar contra a abordagem dinâmica de GRPO baseada em reparo.

Principais Resultados

O modelo foi avaliado em um benchmark de 30 problemas retidos utilizando decodificação gulosa de disparo único (single-shot greedy decoding).

• Desempenho: O TLA-Prover (checkpoint final de reparo-GRPO) alcançou uma taxa de passagem de 30% (9/30) tanto nos níveis Ouro quanto no Diamante.
• Comparação com Baseline: Isso representa uma melhoria de 3,5x sobre a baseline de 8,6% do FormaLLM não ajustado.
• Comparação de Ablação: A variante DPO alcançou uma taxa de passagem Diamante de 20%, sendo superada pela abordagem de reparo-GRPO (30%).
• Validação Anti-Reward-Hacking: Crucialmente, as taxas de passagem Ouro e Diamante coincidiram em cada checkpoint no pipeline de produção (diferença de 0). Isso indica que o modelo não aprendeu a gerar invariantes tautológicos que passam no TLC, mas falham no teste de mutação. A única exceção foi um único caso na ablação DPO, que o nível Diamante detectou com sucesso.
• Estratégias de Inferência:
  • Amostragem Best-of-8 aumentou a taxa de passagem Diamante para 37% (11/30).
  • A união Greedy ∪ Best-of-8 sugere um teto de 43% (13/30), indicando que o modelo possui a capacidade de resolver mais problemas dadas múltiplas tentativas.
  • A autocorreção (feedback de 3 disparos do TLC) não apresentou melhoria, sugerindo que as falhas se devem a lacunas de conhecimento, e não a erros de amostragem aleatória.

Significância e Contribuições

O artigo reivindica três contribuições primárias:

1. TLA-Prover com uma Hierarquia de Quatro Níveis: A introdução de uma hierarquia de validação onde o nível superior (Diamante) utiliza testes de mutação para excluir invariantes tautológicos. Isso aborda o risco específico de reward-hacking inerente ao uso do TLC como sinal de recompensa, garantindo que o "passar" implica uma especificação não trivial.
2. Pipeline de GRPO Baseado em Reparo: Um pipeline de treinamento de duas etapas combinando SFT em um corpus de nível Diamante com GRPO baseado em reparo. Esta abordagem aproveita o feedback online do verificador para fornecer sinais de recompensa densos, superando as ablações estáticas de DPO.
3. Análise Empírica de Anti-Reward-Hacking: A observação de que as taxas de passagem Ouro e Diamante coincidem em todos os checkpoints fornece evidência empírica de que o pipeline impede com sucesso o modo de falha de "invariante sempre verdadeiro".

Os autores posicionam este trabalho como o primeiro estudo de treinamento voltado para TLA+ que excede substancialmente as baselines do FormaLLM. Eles enfatizam que, embora o modelo melhore significamente a síntese de especificações, ele atualmente se especializa em especificações de estilo invariante com espaços de estados pequenos e tem dificuldade com protocolos complexos que exigem análise de casos ou manipulação de quantificadores. O trabalho ressalta que o treinamento guiado por verificador sem validação anti-reward-hacking (como o nível Diamante) é insuficiente para produzir especificações formais significativas.