LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning

O artigo apresenta o LTLGuard, uma ferramenta modular que combina geração com restrições e verificação formal leve para permitir que modelos de linguagem compactos (4B–14B parâmetros) traduzam requisitos informais em especificações de LTL corretas e consistentes, superando as limitações de modelos menores em lógica temporal.

O essencial

Imagine que você é um arquiteto de software e precisa construir um prédio muito seguro. Você tem um monte de ideias no papel, escritas em linguagem comum, como: "Se alguém pedir um elevador, ele deve chegar logo" ou "Nunca deixe duas portas abertas ao mesmo tempo".

O problema é que os computadores (especialmente os sistemas de segurança) não entendem "idioma humano". Eles falam uma linguagem matemática muito rígida chamada Lógica Temporal Linear (LTL). Traduzir suas ideias soltas para essa linguagem de computador é como tentar traduzir um poema para uma linguagem de programação: é fácil errar, e um pequeno erro pode fazer o prédio inteiro desmoronar (ou o sistema falhar).

Aqui entra o LTLGUARD, a ferramenta apresentada neste artigo. Vamos entender como ela funciona usando algumas analogias divertidas:

1. O Problema: O Tradutor "Gênio, mas Esquecido"

Antes, as empresas usavam "Super Tradutores" (modelos de IA gigantes e caros) para fazer essa tradução. Eles são ótimos, mas têm dois problemas:

• São pesados demais para rodar no seu computador (precisam de servidores caros).
• Às vezes, eles "alucinam": inventam regras que parecem verdadeiras, mas são logicamente impossíveis (como dizer "O elevador chega agora e nunca chega").

O artigo propõe usar modelos menores e mais leves (como um tradutor de bolso). O problema é que esses modelos menores não são tão inteligentes em lógica complexa. Eles tendem a cometer erros de sintaxe (escrever a fórmula errada) ou criar contradições.

2. A Solução: O LTLGUARD (O "Guardião" da Tradução)

O LTLGUARD não é apenas um tradutor; é um sistema de equipe que ajuda o modelo pequeno a não errar. Pense nele como um engenheiro júnior (o modelo pequeno) que está sendo supervisionado por três especialistas experientes:

A. O Bibliotecário (Retrieval-Augmented Few-Shot Learning)

Quando o engenheiro júnior vê uma frase difícil, ele não chuta. Ele consulta um Bibliotecário que busca em uma prateleira de exemplos anteriores frases parecidas e como elas foram traduzidas corretamente.

• Analogia: É como se você estivesse escrevendo um e-mail formal e, antes de enviar, consultasse um arquivo de e-mails anteriores para ver como você costumava escrever frases similares. Isso ajuda o modelo a "lembrar" o padrão correto.

B. O Fiscal de Gramática (Grammar-Based Guidance)

O modelo pequeno às vezes inventa palavras ou esquece parênteses. O Fiscal atua como um corretor automático superpoderoso que bloqueia qualquer palavra que o modelo tente escrever se ela não seguir as regras estritas da linguagem LTL.

• Analogia: Imagine um jogo de tabuleiro onde você só pode colocar a peça em um quadrado se ele for da cor certa. O Fiscal garante que o modelo nunca coloque uma peça no lugar errado, garantindo que a fórmula seja "gramaticalmente" correta.

C. O Detetive de Contradições (Consistency Checking)

Às vezes, o modelo traduz cada frase individualmente corretamente, mas quando você junta todas, elas se contradizem (ex: "O elevador deve chegar" e "O elevador nunca chega"). O Detetive pega todas as traduções, as coloca juntas e verifica se elas fazem sentido como um todo.

• Analogia: É como um juiz que olha para o caso completo. Se o advogado diz "O réu estava em casa" e "O réu estava no trabalho", o Detetive grita: "Espere! Isso é impossível! Algo está errado!".
• Se o Detetive encontrar um erro, ele manda a informação de volta para o engenheiro júnior: "Olha, essa combinação não funciona. Tente de novo". Isso cria um ciclo de melhoria.

3. O Resultado: Pequeno, Rápido e Preciso

O artigo mostra que, ao usar essa equipe (o modelo pequeno + o bibliotecário + o fiscal + o detetive), é possível obter resultados tão bons quanto os dos "Super Tradutores" gigantes, mas rodando no seu próprio computador, de forma privada e sem gastar uma fortuna em energia.

• Precisão: O sistema consegue traduzir frases ambíguas (que podem ter mais de um significado) com muito mais cuidado.
• Robustez: Se você mudar a frase de "Todo pedido é atendido" para "Nenhum pedido fica sem resposta", o sistema entende que é a mesma regra lógica e não entra em pânico.
• Segurança: Como roda localmente, você não precisa enviar seus segredos industriais para a nuvem.

Resumo em uma frase

O LTLGUARD é como um estagiário de inteligência artificial que, com a ajuda de um manual de instruções, um corretor de texto rigoroso e um supervisor que verifica contradições, consegue traduzir suas ideias humanas em regras de computador perfeitas, sem precisar de um supercomputador para isso.

Isso torna a tecnologia de verificação formal (que antes era cara e difícil) acessível para qualquer empresa que queira garantir que seus sistemas de software sejam seguros e funcionem como prometido.

Resumo técnico

Título: LTLGUARD: Formalização de Especificações LTL com Modelos de Linguagem Compactos e Raciocínio Simbólico Leve

1. O Problema

A tradução de requisitos informais (em linguagem natural) para especificações formais (como Lógica Temporal Linear - LTL) é um desafio significativo na engenharia de requisitos. As principais dificuldades incluem:

• Ambiguidade e Variabilidade: A linguagem natural é inerentemente ambígua. Uma frase como "toda requisição é seguida por uma concessão" pode ter múltiplas interpretações lógicas (ex: no mesmo passo, no próximo passo, ou em um futuro estrito).
• Limitações dos Modelos Compactos: Embora os Grandes Modelos de Linguagem (LLMs) de ponta (flagship) tenham bom desempenho, eles são grandes, custosos, levantam preocupações de privacidade e podem alucinar. Modelos compactos (4B–14B parâmetros), que são ideais para execução local e privada, frequentemente carecem de conhecimento robusto sobre lógica temporal, resultando em especificações sintaticamente inválidas ou semanticamente inconsistentes.
• Falta de Consistência: Gerar um conjunto de fórmulas LTL que sejam não apenas corretas individualmente, mas também mutuamente consistentes (sem conflitos lógicos entre si), é complexo para modelos puramente generativos.

2. Metodologia: O Framework LTLGUARD

O LTLGUARD é uma ferramenta modular que combina a capacidade generativa de modelos de linguagem compactos (open-weight) com técnicas de raciocínio simbólico leve para gerar especificações LTL corretas e consistentes. O fluxo de trabalho é semi-automatizado, mantendo o engenheiro no loop.

Os blocos de construção principais são:

1. Especificação de Prompt (Prompt Specification):

   • Define o papel do modelo, diretrizes sintáticas estritas para LTL e o formato de saída esperado.
   • Inclui instruções para evitar explicações em linguagem natural e focar apenas nas fórmulas.

2. Aprendizado com Poucos Exemplos Aumentado por Recuperação (RAFSL - Retrieval-Augmented Few-Shot Learning):

   • Em vez de usar um conjunto fixo de exemplos, o sistema usa dense retrieval (busca por similaridade semântica) para selecionar dinamicamente exemplos relevantes de um banco de dados (pares NL-LTL) para cada requisito de entrada.
   • O banco de dados utiliza "placeholders" genéricos para proposições atômicas, permitindo que a busca se baseie na estrutura temporal e não em nomes de variáveis específicos.
   • Isso fornece contexto específico à tarefa, compensando a falta de treinamento especializado do modelo compacto.

3. Guia Baseado em Gramática (Grammar-Based Guidance):

   • Utiliza a ferramenta SynCode, que emprega um Autômato Finito Determinístico (DFA) derivado da gramática LTL.
   • Durante a geração de tokens, o modelo é forçado a escolher apenas tokens que sejam sintaticamente válidos segundo a gramática, garantindo que a saída seja sempre uma fórmula LTL bem formada.

4. Verificação de Consistência e Feedback Iterativo:

   • Um verificador de satisfabilidade (usando a ferramenta BLACK) analisa as fórmulas geradas.
   • Sintaxe: Se a análise falhar, a informação de debug é enviada de volta ao modelo para refinamento iterativo.
   • Semântica/Consistência: Se o conjunto de fórmulas for insatisfatível (UNSAT), o sistema identifica o "núcleo insatisfatível" (o subconjunto mínimo de fórmulas que causa o conflito).
   • O sistema destaca os requisitos conflitantes e fornece o núcleo insatisfatível ao modelo para tentar resolver automaticamente a inconsistência ou alertar o engenheiro humano.

3. Principais Contribuições

• Framework Híbrido Eficiente: Demonstra que é possível alcançar alta precisão na formalização de requisitos usando modelos compactos (4B-14B) sem necessidade de fine-tuning pesado, combinando geração com verificação simbólica.
• Abordagem de Consistência: Diferente de trabalhos anteriores que focam apenas na tradução de uma fórmula por vez, o LTLGUARD verifica a consistência entre conjuntos de especificações, detectando conflitos lógicos entre requisitos.
• Privacidade e Acessibilidade: Permite a execução local em infraestrutura padrão, resolvendo problemas de privacidade de dados sensíveis e custos computacionais associados a modelos proprietários massivos.
• Mecanismo de Refinamento Iterativo: Integra a detecção de erros (sintáticos e semânticos) de volta no processo de geração, permitindo que o modelo "aprenda" com seus próprios erros durante a inferência.

4. Resultados Experimentais

Os autores avaliaram o framework em quatro modelos compactos (Qwen2.5-14B, Mistral-Nemo-12B, Mistral-7B, Phi-3-Mini-4B) e compararam com o estado da arte (incluindo o nl2spec e modelos grandes como GPT-3.5 e Codex).

• Precisão de Tradução (RQ1):

  • A combinação de SynCode (gramática) e RAFSL (recuperação de exemplos) trouxe ganhos massivos.
  • Para o modelo Mistral-7B, a validade sintática saltou de 10% (modelo puro) para 92,8% (sistema completo).
  • No benchmark "hard" do nl2spec (36 casos difíceis), o LTLGUARD (com Qwen2.5-14B) atingiu 75% de precisão semântica (ambiguidade-intolerante) e 77,8% (ambiguidade-amigável), superando todas as variantes não interativas de modelos grandes e aproximando-se da precisão de sistemas interativos com modelos proprietários massivos.
  • A sobreposição de exemplos no banco de dados RAFSL mostrou-se crucial para lidar com padrões complexos.

• Robustez (RQ2):

  • O sistema demonstrou robustez na reescrita de requisitos (Rephrasing Robustness) e na renomeação de átomos (Atom Renaming Robustness).
  • A variante V6 (com SynCode, RAFSL e feedback) alcançou robustez perfeita em testes de renomeação de átomos, gerando fórmulas estruturalmente idênticas para requisitos semanticamente equivalentes com palavras diferentes.

• Verificação de Consistência (RQ3):

  • O verificador de consistência foi eficaz em detectar tanto conflitos inerentes nos requisitos quanto erros de formalização.
  • Em testes, o sistema identificou que variações sutis na linguagem natural (ex: "requisições não serão concedidas" vs "nenhuma requisição será concedida") poderiam levar a traduções LTL inconsistentes, e o feedback iterativo ajudou a corrigir ou sinalizar esses erros.

5. Significado e Conclusão

O trabalho LTLGUARD é significativo porque desafia a premissa de que apenas modelos de linguagem massivos e proprietários são adequados para tarefas de lógica formal complexa. Ao integrar raciocínio simbólico leve (verificadores de satisfabilidade e gramáticas) com modelos compactos, o framework oferece:

1. Uma solução privada e econômica para a indústria.
2. Um caminho viável para automatizar a engenharia de requisitos com alta confiabilidade.
3. Uma abordagem que trata a ambiguidade não apenas como um erro, mas como um problema a ser resolvido através de verificação e interação humana guiada.

Os autores concluem que, embora haja espaço para melhoria na robustez para uso industrial, a integração de técnicas leves com modelos compactos é uma estratégia promissora para fechar a lacuna entre requisitos informais e especificações formais rigorosas.