Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs

Resumo Técnico: Ponte entre Linguagem Natural e Especificação Formal via Decomposição Semântica Hierárquica

Declaração do Problema
A tradução precisa e automatizada de requisitos de software em linguagem natural (NL) para especificações formais, especificamente Lógica Temporal Linear (LTL), é um gargalo crítico para a escalabilidade da verificação formal em domínios industriais de missão crítica, como o aeroespacial. As práticas industriais atuais dependem fortemente da tradução manual por especialistas humanos, um processo demorado e propenso a erros. Embora as abordagens automatizadas existentes — variando de sistemas baseados em regras a métodos baseados em aprendizado — ofereçam algum nível de automação, elas enfrentam limitações significativas. Métodos baseados em regras carecem de flexibilidade e lutam com a variabilidade da linguagem natural, enquanto abordagens baseadas em aprendizado frequentemente falham em generalizar além de seus dados de treinamento. Além disso, os Modelos de Linguagem de Grande Escala (LLMs) recentes, apesar de sua proficiência na extração semântica, lutam com a semântica temporal implícita, estruturas lógicas profundamente aninhadas e restrições específicas de contexto inerentes aos requisitos industriais do mundo real. A aplicação direta de LLMs frequentemente leva a "falhas silenciosas", onde as fórmulas geradas são sintaticamente válidas, mas semanticamente incorretas devido ao acúmulo de erros e à falta de validação estrutural.

Metodologia: O Framework REQ2LTL
Para enfrentar esses desafios, os autores propõem o REQ2LTL, um framework modular que faz a ponte entre NL e LTL através de uma nova representação intermediária hierárquica chamada OnionL. O framework opera via um pipeline de dois estágios que combina as capacidades de extração semântica dos LLMs com as garantias estruturais da síntese determinística baseada em regras.

1. Representação Intermediária (OnionL):
   O OnionL é uma linguagem intermediária estruturada em árvore projetada para codificar explicitamente a semântica temporal, escopos e relações lógicas. Ele decompõe os requisitos em três elementos composicionais:

   • Proposições Atômicas (APs): Fatos de nível de predicado anotados com subcampos semânticos (Componente, Variável, Relação, Fórmula).
   • Escopos (Scopes): Limites contextuais correspondentes a operadores unários (ex: Globalmente, Eventualmente, Próximo) ou antecedentes baseados em modo.
   • Relações: Dependências lógicas ou temporais (ex: E, Ou, Implica, Até) que conectam subfórmulas.
     Esta estrutura espelha a sintaxe composicional da LTL, servindo como uma ponte semântica que permite aos LLMs focar na análise semântica local enquanto delegam a composição lógica global para mecanismos baseados em regras.

2. Estágio 1: REQ2ONIONL (Decomposição Semântica):
   Este módulo utiliza um LLM guiado por prompts para transformar requisitos de linguagem natural livre em árvores OnionL estruturadas. Ele emprega um algoritmo específico de Cadeia de Pensamento (Chain-of-Thought) chamado BUILDING-ONIONL, que opera em dois estágios:

   • Extração de Macroestrutura: Identifica escopos temporais globais ou baseados em modo para construir o nó de nível superior.
   • Decomposição Recursiva de Cláusulas: Decompõe recursivamente as cláusulas em escopos aninhados, relações e proposições atômicas normalizadas.
     O processo é guiado por um repositório de conhecimento que define a gramática recursiva do OnionL e é reforçado por exemplos de poucos disparos (few-shot) de padrões industriais.

3. Estágio 2: ONIONL2LTL (Síntese Baseada em Regras):
   Este módulo realiza uma tradução determinística e baseada em regras da árvore OnionL validada para uma fórmula LTL padronizada.

   • Validação: Antes da tradução, o sistema realiza uma travessia em profundidade para verificar a integridade estrutural (ex: aridade correta de operadores, aninhamento de escopo válido). Para aplicações de segurança crítica, o framework suporta um mecanismo de "humano no circuito" (human-in-the-loop), onde a estrutura OnionL é visualizada (via diagramas Mermaid) para inspeção e correção por engenheiros.
   • Tradução: Uma travessia pós-ordem converte cada nó em sua sintaxe LTL correspondente (ex: mapeando Globalmente para $G$, Implica para $\rightarrow$). Este processo garante que cada saída seja sintaticamente válida por construção.

Principais Contribuições

• Representação Intermediária OnionL: Uma linguagem hierárquica que codifica explicitamente a semântica temporal e as relações lógicas, atuando como uma ponte semântica robusta entre NL e LTL.
• Decomposição Semântica Hierárquica: Um algoritmo de dois estágios, impulsionado por prompts (BUILDING-ONIONL), que decompõe sistematicamente os requisitos, melhorando significativamente a integridade estrutural e a precisão semântica.
• Framework REQ2LTL: Um pipeline automatizado que combina a decomposição baseada em LLM com a tradução e validação determinística baseada em regras. Ele alcança precisão semântica superior e correção sintática perfeita em comparação com métodos existentes.

Resultados Experimentais
Os autores avaliaram o REQ2LTL tanto em benchmarks acadêmicos (Circuit, Navigation, Office Email) quanto em um conjunto de dados industrial do mundo real de 112 requisitos aeroespaciais.

• Desempenho Industrial: No conjunto de dados aeroespacial, o REQ2LTL alcançou 88,4% de precisão semântica (Correspondência Exata) e 100% de correção sintática. Isso superou significativamente os baselines de última geração (ex: NL2SPEC, NL2LTL, NL2TL), que tiveram dificuldades com lógica aninhada e pistas temporais implícitas, alcançando taxas de correspondência exata entre 55% e 65%.
• Desempenho Acadêmico: Nos benchmarks acadêmicos, o REQ2LTL demonstrou alto desempenho consistente (Acurácia Binária >94%, BLEU >0,97), generalizando efetivamente mesmo em cenários menos ambíguos.
• Estudos de Ablação: Experimentos confirmaram que a combinação de modelagem estruturada (OnionL), prompting em estágios e feedback de verificação é essencial. Remover a representação intermediária estruturada causou uma queda na precisão semântica para 65,2%, enquanto remover o prompting em estágios reduziu-a para 58,9%.
• Análise de Erros: O framework eliminou efetivamente erros relacionados à interpretação temporal errônea, confusão condicional e perda de aninhamento, que eram prevalentes em métodos zero-shot e outros baselines. Os erros restantes foram primariamente atribuídos à ambiguidade linguística inerente aos requisitos de entrada.

Significância e Alegações
O artigo afirma que o REQ2LTL efetivamente preenche a lacuna entre requisitos informais de linguagem natural e especificações formais, fornecendo uma base prática para a adoção escalável em sistemas industriais de missão crítica. Ao introduzir uma representação intermediária estruturada e uma arquitetura híbrida de LLM e regras, o framework mitiga as limitações da tradução direta de LLM, abordando especificamente os desafios da semântica temporal implícita e do profundo aninhamento lógico. Os autores enfatizam que a capacidade do framework de garantir 100% de correção sintática através de síntese baseada em regras, combinada com alta fidelidade semântica, torna-o uma ferramenta viável para fluxos de trabalho de verificação industrial. Adicionalmente, a inclusão de uma etapa de validação visualizada com humano no circuito aborda a questão da ambiguidade linguística, permitindo que engenheiros corrijam eficientemente erros semânticos sem quebrar o pipeline de automação. Os autores observam que, embora o trabalho atual se concentre em LTL, extensões futuras poderiam visar lógicas temporais mais expressivas como Signal Temporal Logic (STL) e Metric Temporal Logic (MTL).