Resumo Técnico: TLA+-Bench

Declaração do Problema

O campo da geração de especificações formais a partir de linguagem natural enfrenta uma lacuna crítica de medição. Embora os grandes modelos de linguagem (LLMs) sejam cada vez mais incumbidos de gerar especificações TLA+ a partir de descrições em linguagem natural, o progresso é difícil de quantificar com precisão. Os recursos existentes tipicamente avaliam os resultados com base na semelhança textual com uma referência ou no simples sucesso de análise sintática (parsing). Esses métodos falham em verificar a corretude, frequentemente superestimando a capacidade do modelo. Ao contrário da geração de código geral, onde os testes são aproximados, o TLA+ possui um oráculo decidível (o model checker TLC) que pode determinar a satisfação de propriedades sobre todo o espaço de estados alcançável. No entanto, conjuntos de dados anteriores não utilizaram este oráculo exato em escala, nem forneceram os metadados necessários para controlar variações de entrada ou níveis de dificuldade.

Metodologia

Construção do Conjunto de Dados (TLA+-Bench)

Os autores construíram um conjunto de dados e um benchmark compreendendo 1.300 especificações extraídas de 13 repositórios públicos. O conjunto de dados é estratificado em dois níveis:

• Nível Gold (403 especificações): Contém módulos TLA+ pareados com configurações de model-checking executáveis. Estes são verificados pelo model checker TLC para garantir que satisfaçam as propriedades declaradas sobre todo o espaço de estados alcançável.
• Nível Silver (897 especificações): Contém módulos que realizam o parsing com sucesso, mas carecem de configurações executáveis, suportando estudos de taxa de parsing em larga escala.

Metadados e Aumentação:
Cada especificação é aumentada com:

• Quatro Descrições em Linguagem Natural: Geradas por dois provedores (GPT-5 e Claude Opus 4.5) em dois estilos distintos:
  • Declarativo: Revela os nomes reais do módulo (testando a recuperação de interface).
  • Intento: Esconde os nomes, declarando apenas os requisitos do sistema (testando o design do zero).
• Rótulos: Rótulos de dificuldade (Básico, Intermediário, Avançado) e rótulos de categoria (Sistema vs. Utilitário).
• Identificação de Fixtures Triviais: Especificações válidas que possuem apenas um estado alcançável (que passam trivialmente) são identificadas e excluídas do conjunto de avaliação primário para evitar pontuações infladas.

Protocolo de Avaliação

O benchmark avalia os modelos usando uma abordagem baseada em execução em vez de sobreposição textual:

1. Portão de Validade: A especificação gerada deve realizar o parsing sob o parser SANY.
2. Portão Semântico: A especificação é executada contra a configuração de referência usando o model checker TLC. O TLC explora todo o espaço de estados alcançável para decidir se propriedades nomeadas são violadas.
3. Definição de Corretude: Uma especificação é "correta" apenas se passar por ambos os portões.

O Envelope de Corretude:
O artigo introduz o conceito de "envelope de corretude" para demonstrar que um único número de corretude é insuficiente. Os autores medem a corretude sob quatro regimes distintos no mesmo conjunto de saídas:

• Consciente de Configuração (Configuration-Aware): O modelo recebe os nomes das interfaces (constantes/propriedades) no prompt.
• Padrão (Default): O modelo deve recuperar os nomes das interfaces apenas pela descrição.
• Substantivo (Substantive): As aprovações devem exercitar o comportamento real (múltiplos estados) e verificar propriedades não tautológicas.
• Sobrevivência à Mutação (Mutation-Surviving): A propriedade verificada deve ser "estrutural" (verificada via teste de mutação onde a propriedade é substituída por TRUE).

Resultados Principais

1. O Envelope de Corretude

A escolha do regime de graduação altera drasticamente os resultados reportados. No mesmo conjunto de saídas de modelos de fronteira:

• Taxa Consciente de Configuração: 18,7% (Modelo recebe nomes de interface).
• Taxa Padrão: 10,0% (Modelo recupera nomes de interface).
• Taxa Substantiva: 4,0% (As aprovações devem exercitar o comportamento).
• Taxa de Sobrevivência à Mutação: 1,7% (As propriedades devem verificar propriedades não triviais).

Isso representa uma diferença de onze vezes (18,7% para 1,7%) baseada meramente nas escolhas de graduação, destacando que benchmarks anteriores que reportam um único número selecionam silenciosamente um desses regimes.

2. Validade vs. Corretude

Existe uma lacuna significativa entre validade sintática e corretude semântica.

• Modelos de Fronteira: As taxas de parsing variam de 63% a 89%, mas as taxas de corretude (sob o regime padrão) variam de 4% a 16%.
• Modelos Abertos: As taxas de parsing são significativamente menores (7% a 29%), com taxas de corretude de 0% a 1%.
• Conclusão: Modelos escrevem TLA+ válido com muito mais frequência do que escrevem TLA+ correto. Um benchmark que pare na fase de parsing falsamente classificaria esses modelos como capazes.

3. Dificuldade e Modos de Falha

• Abismo de Dificuldade: A corretude cai drasticamente conforme a dificuldade do problema aumenta. Para modelos de fronteira, a taxa de corretude cai de 25% em especificações básicas para 2% em especificações intermediárias e avançadas.
• Taxonomia de Falhas: O modo de falha dominante é a Vinculação de Configuração (mismatch de nomes entre o módulo gerado e a referência de configuração), representando até 74% das falhas para alguns modelos. Outras falhas incluem erros de parsing, violações de segurança e violações de vivacidade (liveness).
• Consistência de Falha: Modelos frequentemente falham nas mesmas categorias nas mesmas especificações, sugerindo que a dificuldade reside tanto na estrutura da tarefa quanto na capacidade do modelo.

Significância e Alegações

O artigo afirma que o TLA+-Bench fornece o primeiro benchmark baseado em execução para geração de linguagem natural para TLA+ que utiliza um oráculo exato. Sua principal contribuição não é apenas o conjunto de dados, mas a percepção metodológica de que um oráculo exato não gera um único número de corretude.

Em vez disso, a corretude é um intervalo (o "envelope de corretude") dependente de:

1. Se o modelo é informado dos nomes das interfaces.
2. Se a aprovação exercita o comportamento real.
3. Se a propriedade verificada é estrutural (load-bearing).

Os autores afirmam que benchmarks anteriores inflaram a capacidade aparente ao usar oráculos fracos (ex: parsing ou conjuntos de testes finitos) ou ao fazer escolhas de graduação implícitas. Ao tornar essas escolhas explícitas e medir os limites, o TLA+-Bench permite que pesquisadores:

• Meçam a lacuna real entre geração válida e correta.
• Estudem modos de falha específicos (ex: recuperação de interface vs. lógica de modelagem).
• Estratifiquem resultados por dificuldade para entender onde os modelos falham.

O artigo conclui que, embora os modelos mostrem promessa na geração de TLA+ sintaticamente válido, eles atualmente lutam significativamente para gerar especificações semanticamente corretas, particularmente conforme a complexidade do problema aumenta ou quando a recuperação de interface é necessária. O lançamento inclui as especificações, descrições, saídas de modelos e ferramentas de graduação para permitir pesquisa reprodutível e estendida.