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

Sintesi Tecnica: Colmare il divario tra Linguaggio Naturale e Specifica Formale tramite la Decomposizione Semantica Gerarchica

Definizione del Problema
La traduzione accurata e automatizzata dei requisiti software in linguaggio naturale (NL) in specifiche formali, nello specifico la Logica Temporale Lineare (LTL), rappresenta un collo di bottiglia critico per la scalabilità della verifica formale in domini industriali critici per la sicurezza, come l'aerospazio. Le attuali pratiche industriali si affidano pesantemente alla traduzione manuale da parte di esperti umani, un processo che è dispendioso in termini di tempo ed è soggetto a errori. Sebbene gli approcci automatizzati esistenti — che spaziano dai sistemi basati su regole a quelli basati sull'apprendimento — offrano un certo grado di automazione, essi affrontano limitazioni significative. I metodi basati su regole mancano di flessibilità e faticano con la variabilità del linguaggio naturale, mentre gli approcci basati sull'apprendimento spesso non riescono a generalizzare oltre i loro dati di addestramento. Inoltre, i recenti Modelli di Linguaggio di Grandi Dimensioni (LLM), nonostante la loro competenza nell'estrazione semantica, faticano con la semantica temporale implicita, le strutture logiche profondamente annidate e i vincoli specifici del contesto inerenti ai requisiti industriali reali. L'applicazione diretta degli LLM porta spesso a "fallimenti silenziosi", in cui le formule generate sono sintatticamente valide ma semanticamente errate a causa dell'accumulo di errori e della mancanza di validazione strutturale.

Metodologia: Il Framework REQ2LTL
Per affrontare queste sfide, gli autori propongono REQ2LTL, un framework modulare che colma il divario tra NL e LTL attraverso una nuova rappresentazione intermedia gerarchica chiamata OnionL. Il framework opera tramite una pipeline a due stadi che combina le capacità di estrazione semantica degli LLM con le garanzie strutturali della sintesi deterministica basata su regole.

1. Rappresentazione Intermedia (OnionL):
   OnionL è un linguaggio intermedio a struttura ad albero progettato per codificare esplicitamente la semantica temporale, gli scope e le relazioni logiche. Decompone i requisiti in tre elementi composizionali:

   • Proposizioni Atomiche (AP): Fatti a livello di predicato annotati con sottocampi semantici (Componente, Variabile, Relazione, Formula).
   • Scope: Confini contestuali corrispondenti a operatori unari (ad es. Globalmente, Eventualmente, Successivamente) o antecedenti basati su modalità.
   • Relazioni: Dipendenze logiche o temporali (ad es. And, Or, Implica, Finché [Until]) che collegano le sottoformule.
     Questa struttura rispecchia la sintassi compositiva della LTL, fungendo da ponte semantico che permette agli LLM di concentrarsi sulla parsing semantico locale delegando la composizione logica globale a meccanismi basati su regole.

2. Stadio 1: REQ2ONIONL (Decomposizione Semantica):
   Questo modulo utilizza un LLM guidato da prompt per trasformare i requisiti in linguaggio naturale libero in alberi OnionL strutturati. Impiega un algoritmo di Chain-of-Thought specifico chiamato BUILDING-ONIONL, che opera in due fasi:

   • Estrazione della Macro-Struttura: Identifica gli scope temporali o basati su modalità globali per costruire il nodo di alto livello.
   • Decomposizione Ricorsiva delle Clausole: Scompone ricorsivamente le clausole in scope annidati, relazioni e proposizioni atomiche normalizzate.
     Il processo è guidato da un repository di conoscenza che definisce la grammatica ricorsiva di OnionL ed è rinforzato da esempi di pattern industriali tramite few-shot learning.

3. Stadio 2: ONIONL2LTL (Sintesi Basata su Regole):
   Questo modulo esegue una traduzione deterministica e basata su regole dell'albero OnionL validato in una formula LTL standardizzata.

   • Validazione: Prima della traduzione, il sistema esegue una traversata depth-first per verificare la correttezza strutturale (ad es. arità corretta degli operatori, annidamento valido degli scope). Per le applicazioni critiche per la sicurezza, il framework supporta un meccanismo "human-in-the-loop" dove la struttura OnionL viene visualizzata (tramite diagrammi Mermaid) per l'ispezione e la correzione da parte dell'ingegnere.
   • Traduzione: Una traversata post-order converte ogni nodo nella sua corrispondente sintassi LTL (ad es. mappando Globalmente a $G$, Implica a $\rightarrow$). Questo processo assicura che ogni output sia sintatticamente valido per costruzione.

Contributi Chiave

• Rappresentazione Intermedia OnionL: Un linguaggio gerarchico che codifica esplicitamente la semantica temporale e le relazioni logiche, agendo come un robusto ponte semantico tra NL e LTL.
• Decomposizione Semantica Gerarchica: Un algoritmo a due stadi guidato da prompt (BUILDING-ONIONL) che decompone sistematicamente i requisiti, migliorando significativamente l'integrità strutturale e l'accuratezza semantica.
• Framework REQ2LTL: Una pipeline automatizzata che combina la decomposizione basata su LLM con la traduzione e la validazione deterministica basata su regole. Raggiunge una precisione superiore e una correttezza sintattica perfetta rispetto ai metodi esistenti.

Risultati Sperimentali
Gli autori hanno valutato REQ2LTL sia su benchmark accademici (Circuit, Navigation, Office Email) sia su un dataset industriale reale di 112 requisiti aerospaziali.

• Performance Industriale: Sul dataset aerospaziale, REQ2LTL ha raggiunto l'88,4% di accuratezza semantica (Exact Match) e il 100% di correttezza sintattica. Ha superato significativamente i baseline allo stato dell'arte (ad es. NL2SPEC, NL2LTL, NL2TL), che faticavano con la logica annidata e i segnali temporali impliciti, ottenendo tassi di exact match compresi tra il 55% e il 65%.
• Performance Accademica: Sui benchmark accademici, REQ2LTL ha dimostrato prestazioni costantemente elevate (Binary Accuracy >94%, BLEU >0,97), generalizzando efficacemente anche in contesti meno ambigui.
• Studi di Ablazione: Gli esperimenti hanno confermato che la combinazione di modellazione strutturata (OnionL), prompting a stadi e feedback di verifica è essenziale. Rimuovendo la rappresentazione intermedia strutturata, l'accuratezza semantica è scesa al 65,2%, mentre rimuovendo il prompting a stadi è scesa al 58,9%.
• Analisi degli Errori: Il framework ha eliminato efficacemente gli errori relativi alla misinterpretazione temporale, alla confusione condizionale e alla perdita di annidamento, che erano prevalenti negli approcci zero-shot e in altri metodi baseline. Gli errori rimanenti sono stati principalmente attribuiti all'ambiguità linguistica intrinseca nei requisiti di input.

Significato e Rivendicazioni
L'articolo sostiene che REQ2LTL colmi efficacemente il divario tra i requisiti informali in linguaggio naturale e le specifiche formali, fornendo una base pratica per l'adozione scalabile in sistemi industriali critici per la sicurezza. Introducendo una rappresentazione intermedia strutturata e un'architettura ibrida LLM-regole, il framework mitiga i limiti della traduzione diretta tramite LLM, affrontando specificamente le sfide della semantica temporale implicita e del profondo annidamento logico. Gli autori sottolineano che la capacità del framework di garantire il 100% di correttezza sintattica attraverso la sintesi basata su regole, combinata con un'alta fedeltà semantica, lo rende uno strumento valido per i flussi di lavoro di verifica industriale. Inoltre, l'inclusione di un passaggio di validazione visualizzato "human-in-the-loop" affronta il problema dell'ambiguità linguistica, consentendo agli ingegneri di correggere efficientemente gli errori semantici senza interrompere la pipeline di automazione. Gli autori osservano che, sebbene il presente lavoro si concentri sulla LTL, estensioni future potrebbero mirare a logiche temporali più espressive come la Signal Temporal Logic (STL) e la Metric Temporal Logic (MTL).