Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

Imagine que você está tentando ensinar um robô muito inteligente e culto a escrever uma receita matemática rigorosa para uma máquina complexa. Esta máquina é um "sistema distribuído" (como os servidores na nuvem que rodam a Amazon ou a Microsoft), e a receita é escrita em uma linguagem especial chamada TLA+.

Esta linguagem é como um quebra-cabeça de alto risco. Se você perder um único símbolo ou errar levemente a lógica, a máquina pode funcionar na receita, mas falhar na vida real. O problema é que escrever essas receitas à mão é difícil e lento. Por isso, pesquisadores perguntaram: Podemos simplesmente pedir a uma IA moderna (um Grande Modelo de Linguagem, ou LLM) para escrever essas receitas para nós?

Este artigo é o primeiro grande relatório sobre essa questão. Aqui está o que eles descobriram, explicado de forma simples:

1. A Lacuna entre "Gramática vs. Significado"

Os pesquisadores pediram a 30 IAs diferentes para escreverem essas receitas de TLA+ baseadas em descrições em inglês simples.

• A Boa Notícia (Gramática): Cerca de 26% das vezes, a IA escreveu uma receita que parecia correta superficialmente. O "corretor ortográfico" (chamado SANY) disse: "Ok, as palavras e símbolos estão na ordem correta".
• A Má Notícia (Significado): No entanto, quando eles realmente rodaram a receita através de um "testador de lógica" (chamado TLC) para ver se ela realmente funcionava, apenas 8,6% das vezes ela passou.

A Analogia: Imagine pedir a um estudante para escrever um contrato jurídico. O estudante usa ortografia e gramática perfeitas (2cesso de 26%), mas o contrato que ele escreveu diz, na verdade, o oposto do pretendido, ou deixa de fora uma cláusula crucial, tornando-o juridicamente inútil (sucesso de apenas 8,6%). A IA é ótima em imitar a aparência da linguagem, mas frequentemente falha em entender a lógica por trás dela.

2. Maior nem sempre é Melhor

Geralmente, assumimos que uma IA maior e mais poderosa fará um trabalho melhor. Mas, neste estudo, isso não foi verdade.

• A Surpresa: Um modelo de IA menor (DeepSeek r1:8b) fez um trabalho muito melhor do que seu "irmão mais velho" gigante (DeepSeek r1:70b).
• O Porquê: O modelo menor foi treinado especificamente para "pensar passo a passo" (como um aluno de matemática mostrando seus cálculos), enquanto o modelo maior foi treinado com tantos dados gerais da internet que ficou confuso com as regras estritas do TLA+. É como um chef especializado que sabe exatamente como fazer um suflê, versus um generalista que sabe cozinhar de tudo, mas pode complicar demais uma receita específica.

3. "Especialistas em Código" Falharam

Os pesquisadores testaram IAs que são famosas por escrever código de computador (como Python ou Java). Surpreendentemente, esses "especialistas em código" tiveram um desempenho pior do que as IAs de uso geral.

• A Razão: Esses modelos estão tão acostumados a escrever códigos com ponto e vírgula (;) ou chaves ({}) que continuavam inserindo acidentalmente esses símbolos na receita de TLA+. Como o TLA+ não utiliza esses símbolos, a receita quebrava imediatamente. É como um carpinteiro tentando consertar um relógio, mas acidentalmente tentando usar um martelo porque é isso que ele usa para tudo.

4. O Truque do "Passo a Passo" Funcionou Melhor

Os pesquisadores testaram quatro maneiras diferentes de pedir ajuda à IA. O método de maior sucesso foi chamado de "Prompting Progressivo" (Progressive Prompting).

• Como funcionava: Em vez de pedir à IA para escrever a receita inteira de uma vez, eles pediram para construí-la peça por peça: "Primeiro, escreva o título. Agora, escreva as variáveis. Agora, escreva as regras."
• O Resultado: Este foi o único método que produziu qualquer receita totalmente funcional (a taxa de sucesso de 8,6%). É como construir uma casa: se você tentar construir o telhado, as paredes e a fundação de uma só vez em um grande salto, provavelmente falhará. Mas se você construir um cômodo de cada vez, terá mais chances de sucesso.

5. As "Alucinações" da IA

O artigo descobriu cinco maneiras específicas pelas quais a IA cometia os mesmos erros, o que chamamos de "alucinações":

1. Símbolos Errados: Usar símbolos matemáticos complexos (como ∧) em vez dos símbolos de texto simples que o TLA+ exige (como /\).
2. Mistura de Linguagens: Adicionar acidentalmente ponto e vírgula ou crases de outras linguagens de programação.
3. Pensar em Voz Alta: A IA às vezes colava seu próprio "processo de pensamento" (como ...) diretamente na receita final, o que a quebrava.
4. Tamanho Errado: Às vezes a IA escrevia uma receita 9 vezes maior do que o necessário, ou às vezes não escrevia quase nada.
5. Estrutura Quebrada: Esquecer os marcadores de "fim" da receita, deixando o documento inacabado.

A Conclusão Final

O artigo conclui que as IAs atuais ainda não conseguem escrever especificações de TLA+ confiáveis por conta própria. Embora possam imitar a aparência da linguagem, elas ainda cometem erros lógicos demais para serem confiáveis sem que um especialista humano verifique cada linha.

Os pesquisadores sugerem que, para corrigir isso, precisamos:

• Usar o método de prompting "passo a passo".
• Usar modelos menores focados em raciocínio, em vez de modelos massivos de uso geral.
• Construir ferramentas que corrijam automaticamente os erros comuns (como remover os símbolos errados) antes mesmo da IA tentar rodar a receita.

Até lá, escrever essas receitas críticas de sistemas continua sendo um trabalho de especialistas humanos, com a IA atuando como um assistente útil, porém propenso a erros.