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

Technische Samenvatting: Het overbruggen van Natuurlijke Taal en Formele Specificatie via Hiërarchische Semantische Decompositie

Probleemstelling
De nauwkeurige en geautomatiseerde vertaling van natuurlijke taal (NL) software-eisen naar formele specificaties, specifelijk Linear Temporal Logic (LTL), is een kritieke flessenhals voor het opschalen van formele verificatie in veiligheidskritische industriële domeinen zoals de luchtvaart. De huidige industriële praktijken leunen zwaar op handmatige vertaling door menselijke experts, een proces dat tijdrovend en foutgevoelig is. Hoewel bestaande geautomatiseerde benaderingen — variërend van regelgebaseerde systemen tot lerende methoden — enige automatisering bieden, kampen zij met significante beperkingen. Regelgebaseerde methoden missen flexibiliteit en hebben moeite met de variabiliteit van natuurlijke taal, terwijl lerende benaderingen vaak niet generaliseren buiten hun trainingsdata. Bovendien hebben recente Large Language Models (LLM's), ondanks hun bekwaamheid in semantische extractie, moeite met de impliciete temporele semantiek, diep geneste logische structuren en contextspecifieke beperkingen die inherent zijn aan echte industriële eisen. Directe toepassing van LLM's leidt vaak tot "stille fouten", waarbij gegenereerde formules syntactisch geldig zijn maar semantisch incorrect vanwege foutstapeling en een gebrek aan structurele validatie.

Methodologie: Het REQ2LTL-framework
Om deze uitdagingen aan te pakken, stellen de auteurs REQ2LTL voor, een modulair framework dat NL en LTL overbrugt via een nieuwe hiërarchische intermediaire representatie genaamd OnionL. Het framework werkt via een tweefasige pipeline die de semantische extractiecapaciteiten van LLM's combineert met de structurele garanties van deterministische, regelgebaseerde synthese.

1. Intermediaire Representatie (OnionL):
   OnionL is een boomstructuur-intermediaire taal die is ontworpen om temporele semantiek, scopes en logische relaties expliciet te coderen. Het deelt eisen op in drie compositionele elementen:

   • Atomic Propositions (APs): Predicaatniveau feiten geannoteerd met semantische subvelden (Component, Variabele, Relatie, Formule).
   • Scopes: Contextuele grenzen die overeenkomen met unaire operatoren (bijv. Globally, Eventually, Next) of modus-gebaseerde antecedenten.
   • Relations: Logische of temporele afhankelijkheden (bijv. And, Or, Implies, Until) die subformules verbinden.
     Deze structuur weerspiegelt de compositionele syntaxis van LTL, wat dient als een semantische brug waardoor LLM's zich kunnen concentreren op lokale semantische parsing terwijl ze de globale logische compositie delegeren aan regelgebaseerde mechanismen.

2. Fase 1: REQ2ONIONL (Semantische Decompositie):
   Deze module maakt gebruik van een prompt-gestuurde LLM om vrije natuurlijke taal-eisen te transformeren naar gestructureerde OnionL-bomen. Het hanteert een specifiek Chain-of-Thought algoritme genaamd BUILDING-ONIONL, dat opereert in twee stadia:

   • Macro-structuur Extractie: Identificeert globale temporele of modus-gebaseerde scopes om de top-level node te construeren.
   • Recursieve Clausedecompositie: Breekt clausules recursief af in geneste scopes, relaties en genormaliseerde atomische proposities.
     Het proces wordt gestuurd door een kennisrepository die de recursieve grammatica van OnionL definieert en wordt versterkt door few-shot voorbeelden van industriële patronen.

3. Fase 2: ONIONL2LTL (Regelgebaseerde Synthese):
   Deze module voert een deterministische, regelgebaseerde vertaling uit van de gevalideerde OnionL-boom naar een gestandaardiseerde LTL-formule.

   • Validatie: Voor de vertaling voert het systeem een depth-first traversal uit om de structurele welgevormdheid te verifiëren (bijv. correcte ariteit van operatoren, geldige scope-nesting). Voor veiligheidskritische toepassingen ondersteunt het framework een "human-in-the-loop" mechanisme waarbij de OnionL-structuur wordt gevisualiseerd (via Mermaid-diagrammen) voor inspectie en correctie door ingenieurs.
   • Vertaling: Een post-order traversal zet elke node om in de bijbehorende LTL-syntaxis (bijv. het mappen van Globally naar $G$, Implies naar $\rightarrow$). Dit proces zorgt ervoor dat elke output bij constructie syntactisch geldig is.

Belangrijkste Bijdragen

• OnionL Intermediaire Representatie: Een hiërarchische taal die temporele semantiek en logische relaties expliciet codeert, dienend als een robuuste semantische brug tussen NL en LTL.
• Hiërarchische Semantische Decompositie: Een tweefasig, prompt-gestuurd algoritme (BUILDING-ONIONL) dat eisen systematisch deelt, wat de structurele integriteit en semantische nauwkeurigheid aanzienlijk verbetert.
• REQ2LTL Framework: Een geautomatiseerde pipeline die LLM-gebaseerde decompositie combineert met deterministische regelgebaseerde vertaling en validatie. Het bereikt superieure nauwkeurigheid en perfecte syntactische correctheid vergeleken met bestaande methoden.

Experimentele Resultaten
De auteurs evalueerden REQ2LTL op zowel academische benchmarks (Circuit, Navigation, Office Email) als een echte industriële dataset van 112 luchtvaart-eisen.

• Industriële Prestaties: Op de luchtvaartdataset behaalde REQ2LTL 88,4% semantische nauwkeurigheid (Exact Match) en 100% syntactische correctheid. Dit presteerde aanzienlijk beter dan state-of-the-art baselines (bijv. NL2SPEC, NL2LTL, NL2TL), die moeite hadden met geneste logica en impliciete temporele cues, met exact match-percentages tussen de 55% en 65%.
• Academische Prestaties: Op academische benchmarks demonstreerde REQ2LTL consistente hoge prestaties (Binary Accuracy >94%, BLEU >0.97), waarbij het effectief generaliseert, zelfs in minder ambigue settings.
• Ablatie-studies: Experimenten bevestigden dat de combinatie van gestructureerde modellering (OnionL), staged prompting en verificatie-feedback essentieel is. Het verwijderen van de gestructureerde intermediaire representatie zorgde voor een daling van de semantische nauwkeurigheid naar 65,2%, terwijl het verwijderen van staged prompting de nauwkeurigheid terugbracht naar 58,9%.
• Foutanalyse: Het framework elimineerde effectief fouten gerelateerd aan temporele misinterpretatie, conditionele verwarring en het verlies van nesting, die prevalent waren in zero-shot en andere baseline-methoden. Resterende fouten werden voornamelijk toegeschreven aan de inherente linguïstische ambiguïteit in de invoereisen.

Betekenis en Claims
Het artikel claimt dat REQ2LTL effectief de kloof overbrugt tussen informele natuurlijke taal-eisen en formele specificaties, en een praktische basis biedt voor de schaalbare adoptie in veiligheidskritische industriële systemen. Door een gestructureerde intermediaire representatie en een hybride LLM-regelgebaseerde architectuur te introduceren, verzacht het framework de beperkingen van directe LLM-vertaling, waarbij het specifiek de uitdagingen van impliciete temporele semantiek en diepe logische nesting aanpakt. De auteurs benadrukken dat het vermogen van het framework om 100% syntactische correctheid te garanderen via regelgebaseerde synthese, gecombineerd met een hoge semantische getrouwheid, het een levensvatbaar hulpmiddel maakt voor industriële verificatiewerkstromen. Daarnaast adresseert de inclusie van een gevisualiseerde, human-in-the-loop validatiestap het probleem van linguïstische ambiguïteit, waardoor ingenieurs semantische fouten efficiënt kunnen corrigeren zonder de automatisering te breken. De auteurs merken op dat hoewel het huidige werk zich richt op LTL, toekomstige extensies zich kunnen richten op expressievere temporele logica's zoals Signal Temporal Logic (STL) en Metric Temporal Logic (MTL).