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

Resumen Técnico: Puente entre el Lenguaje Natural y la Especificación Formal mediante la Descomposición Semántica Jerárquica

Planteamiento del Problema
La traducción precisa y automatizada de requisitos de software en lenguaje natural (NL) a especificaciones formales, específicamente la Lógica Temporal Lineal (LTL), es un cuello de botella crítico para escalar la verificación formal en dominios industriales de seguridad crítica, como el aeroespacial. Las prácticas industriales actuales dependen en gran medida de la traducción manual por parte de expertos humanos, un proceso que consume mucho tiempo y es propenso a errores. Aunque los enfoques automatizados existentes —que van desde sistemas basados en reglas hasta métodos basados en aprendizaje— ofrecen cierto grado de automatización, enfrentan limitaciones significativas. Los métodos basados en reglas carecen de flexibilidad y luchan contra la variabilidad del lenguaje natural, mientras que los enfoques basados en aprendizaje suelen fallar al generalizar más allá de sus datos de entrenamiento. Además, los Modelos de Lenguaje de Gran Escala (LLMs) recientes, a pesar de su competencia en la extracción semántica, tienen dificultades con la semántica temporal implícita, las estructuras lógicas profundamente anidadas y las restricciones específicas de contexto inherentes a los requisitos industriales del mundo real. La aplicación directa de los LLMs suele conducir a "fallos silenciosos", donde las fórmulas generadas son sintácticamente válidas pero semánticamente incorrectas debido a la acumulación de errores y a la falta de validación estructural.

Metodología: El Marco REQ2LTL
Para abordar estos desafíos, los autores proponen REQ2LTL, un marco modular que tiende un puente entre el NL y el LTL a través de una novedosa representación intermedia jerárquica llamada OnionL. El marco opera mediante un pipeline de dos etapas que combina las capacidades de extracción semántica de los LLMs con las garantías estructurales de la síntesis determinista basada en reglas.

1. Representación Intermedia (OnionL):
   OnionL es un lenguaje intermedio con estructura de árbol diseñado para codificar explícitamente la semántica temporal, los alcances (scopes) y las relaciones lógicas. Descompone los requisitos en tres elementos composicionales:

   • Proposiciones Atómicas (APs): Hechos a nivel de predicado anotados con subcampos semánticos (Componente, Variable, Relación, Fórmula).
   • Alcances (Scopes): Límites contextuales que corresponden a operadores unarios (por ejemplo, Globalmente, Eventualmente, Siguiente) o antecedentes basados en modos.
   • Relaciones: Dependencias lógicas o temporales (por ejemplo, Y, O, Implica, Hasta) que conectan las subfórmulas.
     Esta estructura refleja la sintaxis composicional de LTL, sirviendo como un puente semántico que permite a los LLMs enfocarse en el parseo semántico local mientras delegan la composición lógica global a mecanismos basados en reglas.

2. Etapa 1: REQ2ONIONL (Descomposición Semántica):
   Este módulo utiliza un LLM guiado por prompts para transformar requisitos de lenguaje natural libre en árboles estructurados de OnionL. Emplea un algoritmo de Cadena de Pensamiento (Chain-of-Thought) específico llamado BUILDING-ONIONL, que opera en dos etapas:

   • Extracción de Macroestructura: Identifica alcances globales temporales o basados en modos para construir el nodo de nivel superior.
   • Descomposición Recursiva de Cláusulas: Descompone recursivamente las cláusulas en alcances anidados, relaciones y proposiciones atómicas normalizadas.
     El proceso es guiado por un repositorio de conocimiento que define la gramática recursiva de OnionL y se refuerza con ejemplos de pocos disparos (few-shot) de patrones industriales.

3. Etapa 2: ONIONL2LTL (Síntesis Basada en Reglas):
   Este módulo realiza una traducción determinista y basada en reglas del árbol OnionL validado a una fórmula LTL estandarizada.

   • Validación: Antes de la traducción, el sistema realiza un recorrido de profundidad (depth-first traversal) para verificar la integridad estructural (por ejemplo, la aridad correcta de los operadores, el anidamiento válido de los alcances). Para aplicaciones de seguridad crítica, el marco soporta un mecanismo de "humano en el bucle" (human-in-the-loop) donde la estructura de OnionL se visualiza (mediante diagramas Mermaid) para la inspección y corrección de los ingenieros.
   • Traducción: Un recorrido post-orden convierte cada nodo en su sintaxis LTL correspondiente (por ejemplo, mapeando Globalmente a $G$, Implica a $\rightarrow$). Este proceso asegura que cada salida sea sintácticamente válida por construcción.

Contribuciones Clave

• Representación Intermedia OnionL: Un lenguaje jerárquico que codifica explícitamente la semántica temporal y las relaciones lógicas, actuando como un puente semántico robusto entre el NL y el LTL.
• Descomposición Semántica Jerárquica: Un algoritmo de dos etapas impulsado por prompts (BUILDING-ONIONL) que descompone sistemáticamente los requisitos, mejorando significativamente la integridad estructural y la precisión semántica.
• Marco REQ2LTL: Un pipeline automatizado que combina la descomposición basada en LLM con la traducción y validación determinista basada en reglas. Logra una precisión superior y una corrección sintáctica perfecta en comparación con los métodos existentes.

Resultados Experimentales
Los autores evaluaron REQ2LTL tanto en benchmarks académicos (Circuit, Navigation, Office Email) como en un conjunto de datos industrial del mundo real de 112 requisitos aeroespaciales.

• Rendimiento Industrial: En el conjunto de datos aeroespacial, REQ2LTL alcanzó un 88.4% de precisión semántica (Exact Match) y un 100% de corrección sintáctica. Esto superó significativamente a los baselines de última generación (por ejemplo, NL2SPEC, NL2LTL, NL2TL), que tuvieron dificultades con la lógica anidada y las pistas temporales implícitas, logrando tasas de coincencia exacta de entre el 55% y el 65%.
• Rendimiento Académico: En los benchmarks académicos, REQ2LTL demostró un alto rendimiento constante (Precisión Binaria >94%, BLEU >0.97), generalizando eficazmente incluso en entornos menos ambiguos.
• Estudios de Ablación: Los experimentos confirmaron que la combinación de modelado estructurado (OnionL), prompting por etapas y retroalimentación de verificación es esencial. Eliminar la representación intermedia estructurada causó que la precisión semántica cayera al 65.2%, mientras que eliminar el prompting por etapas la redujo al 58.9%.
• Análisis de Errores: El marco eliminó eficazmente los errores relacionados con la mala interpretación temporal, la confusión condicional y la pérdida de anidamiento, que eran prevalentes en los métodos de cero disparos (zero-shot) y otros baselines. Los errores restantes se atribuyeron principalmente a la ambigüedad lingüística inherente en los requisitos de entrada.

Significancia y Reivindicaciones
El artículo afirma que REQ2LTL cierra eficazmente la brecha entre los requisitos informales de lenguaje natural y las especificaciones formales, proporcionando una base práctica para la adopción escalable en sistemas industriales de seguridad crítica. Al introducir una representación intermedia estructurada y una arquitectura híbrida de LLM y reglas, el marco mitiga las limitaciones de la traducción directa de LLM, abordando específicamente los desafíos de la semántica temporal implícita y el profundo anidamiento lógico. Los autores enfatizan que la capacidad del marco para asegurar una corrección sintáctica del 100% mediante la síntesis basada en reglas, combinada con una alta fidelidad semántica, lo convierte en una herramienta viable para los flujos de trabajo de verificación industrial. Además, la inclusión de un paso de validación visualizado con humano en el bucle aborda el problema de la ambigüedad lingüística, permitiendo a los ingenieros corregir eficientemente los errores semánticos sin romper el pipeline de automatización. Los autores señalan que, si bien el trabajo actual se centra en LTL, futuras extensiones podrían dirigirse a lógicas temporales más expresivas como la Lógica Temporal de Señales (STL) y la Lógica Temporal Métrica (MTL).