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

Dit paper introduceert LTLGuard, een modulaire toolchain die compacte taalmodellen combineert met lichtgewicht symbolische redeneertools om uit informele eisen correcte en consistentie Linear Temporal Logic (LTL)-specificaties te genereren.

De kern

Stel je voor dat je een architect bent die een heel complex gebouw moet ontwerpen. Je hebt een klant die je vertelt wat hij wil, maar de klant spreekt in vaag, alledaags taalgebruik. Hij zegt bijvoorbeeld: "Elke keer als iemand op de knop drukt, moet er ergens later een lichtje branden."

Het probleem is dat deze zin voor een computer (of een strenge bouwkundige) onduidelijk is. Bedoelt de klant:

1. Het licht gaat direct aan?
2. Het licht gaat een seconde later aan?
3. Of gaat het op een willekeurig moment in de toekomst aan?

Als je dit niet precies vastlegt, kan het gebouw (of de software) falen. In de wereld van computers noemen we deze strikte, onmiskenbare taal LTL (Linear Temporal Logic). Het is als de wiskundige blauwdruk die een computer perfect begrijpt.

Het Probleem: De Vertaler die Verkeert

Vroeger moesten mensen deze vertaling van "vaag Nederlands" naar "streng LTL" zelf doen. Dat is moeilijk, duur en foutgevoelig.

Vervolgens kwamen er enorme, super-intelligente AI-modellen (grote taalmodellen). Die konden goed vertalen, maar ze zijn:

• Te groot: Ze passen niet op je eigen computer; je moet ze via het internet gebruiken (privacy-risico).
• Te duur: Ze verbruiken veel stroom.
• Hallucinerend: Soms verzinnen ze dingen die klinken alsof ze kloppen, maar in de logica totaal onzin zijn.

Daarnaast zijn er kleinere, "compacte" AI-modellen. Die passen wel op je eigen laptop en zijn goedkoop, maar ze zijn vaak niet slim genoeg voor dit soort logische puzzels. Ze maken veel fouten.

De Oplossing: LTLGUARD (De Kwaliteitscontroleur)

De auteurs van dit paper hebben LTLGUARD bedacht. Het is geen nieuwe, supergrote AI, maar een slim gereedschap dat een klein, bescheiden AI-model helpt om perfect te werken.

Je kunt LTLGUARD zien als een drie-delige inspectie-inspectie voor een vertaler:

1. De "Gids" (Retrieval-Augmented Few-Shot Learning)

Stel je voor dat de kleine AI een leerling is die nog nooit een blauwdruk heeft gezien. LTLGUARD pakt een boek met voorbeelden (een database) en zoekt daaruit de drie meest vergelijkbare voorbeelden die hij nodig heeft.

• Voorbeeld: Als de klant zegt "Elke bestelling moet worden verzonden", zoekt de AI in zijn boek naar eerdere zinnen over "bestellingen" en "verzenden" om te zien hoe die in het verleden correct zijn vertaald.
• Dit helpt de kleine AI om zich te concentreren op de juiste logica, zonder dat hij zelf alles uit zijn hoofd hoeft te weten.

2. De "Grammatica-Check" (Syntax-Guided Decoding)

De kleine AI begint nu te schrijven. Maar LTLGUARD houdt een strenge grammatica-regel in de gaten.

• Het is alsof de AI schrijft op een toetsenbord waar bepaalde slechte letters (foutieve symbolen) fysiek geblokkeerd zijn. De AI kan alleen kiezen uit de letters die wiskundig kloppen.
• Zo is het onmogelijk dat de AI een zin produceert die grammaticaal onmogelijk is voor een computer.

3. De "Logica-Detective" (Consistency Checking)

Dit is het slimste deel. Stel, de klant zegt:

1. "Elke vraag krijgt een antwoord."
2. "Geen enkele vraag krijgt een antwoord."

De AI vertaalt dit misschien naar twee formules. LTLGUARD neemt deze formules en laat ze door een logische detective (een rekenmachine) controleren.

• De detective zegt: "Hé, dit kan niet! Als A waar is, kan B niet waar zijn. Dit is een tegenstrijdigheid."
• Vervolgens geeft LTLGUARD dit signaal terug naar de AI: "Je hebt een fout gemaakt, probeer het nog eens."
• Zo wordt de vertaling stap voor stap verbeterd tot alles klopt.

Waarom is dit geweldig?

• Privacy: Omdat het werkt met kleine modellen, kun je dit op je eigen computer draaien. Je hoeft geen gevoelige bedrijfsgegevens naar een grote cloud-dienst te sturen.
• Betrouwbaarheid: Het combineert de creativiteit van de AI met de strenge logica van wiskundige regels.
• Resultaat: De paper laat zien dat deze combinatie van een klein model + slimme hulpmiddelen net zo goed (of soms beter) werkt als de enorme, dure modellen, maar dan zonder de nadelen.

Samenvattend

LTLGUARD is als het geven van een super-intelligente werkboek, een onfeilbare grammatica-regel en een strenge controleur aan een beginnende vertaler. Hierdoor kan zelfs een "kleine" AI complexe, veilige en foutloze blauwdrukken maken voor software, zonder dat je een dure supercomputer nodig hebt. Het maakt het mogelijk om van vaag menselijk taalgebruik naar perfecte, veilige computerregels te gaan.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "LTLGUARD: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning" in het Nederlands.

Probleemstelling

Het vertalen van informele eisen (in natuurlijke taal) naar formele specificaties (zoals Lineaire Temporele Logica, LTL) is een fundamentele maar uitdagende taak in de verificatie van systemen. De belangrijkste obstakels zijn:

1. Ambiguïteit: Natuurlijke taal is vaak vaag en kan meerdere interpretaties toelaten (bijv. betekent "elk verzoek wordt gevolgd door een toekenning" dat dit in dezelfde stap, de volgende stap, of op een willekeurig moment in de toekomst gebeurt?).
2. Beperkingen van Compacte Modellen: Hoewel Large Language Models (LLMs) goed zijn in deze vertaling, zijn de topmodellen vaak te groot voor lokale implementatie (privacy- en kostenproblemen). Compacte, open-source modellen (4B–14B parameters) missen vaak voldoende kennis van temporele logica, wat leidt tot syntactisch ongeldige output of semantische inconsistenties.
3. Hallucinaties en Inconsistenties: Zelfs geavanceerde modellen kunnen geloofwaardige maar semantisch misleidende resultaten produceren, en het ontbreken van controlemechanismen maakt het moeilijk om fouten op te sporen.

Methodologie: Het LTLGUARD Framework

LTLGUARD is een modulaire toolchain die compacte, open-weight taalmodellen combineert met lichtgewicht symbolische redeneertechnieken om correcte en consistente LTL-specificaties te genereren zonder dat er zware fine-tuning nodig is. Het framework werkt in een iteratieve cyclus met de volgende kerncomponenten:

1. Prompt Specificatie: Een systeemprompt die de rol van het model definieert, syntactische richtlijnen voor LTL geeft en de outputstructuur beperkt.
2. Retrieval-Augmented Few-Shot Learning (RAFSL): In plaats van een vast aantal voorbeelden te gebruiken, selecteert het systeem dynamisch de meest relevante NL-LTL voorbeelden uit een kennisbank op basis van semantische gelijkenis (via embeddings). Dit helpt het compacte model om context te begrijpen en patronen te herkennen.
3. Grammargebaseerde Gids (Grammar-Based Guidance): Om syntactische correctheid te garanderen, wordt SynCode gebruikt. Dit is een tool die een Deterministisch Eindige Automaten (DFA) gebruikt om de token-generatie van het LLM te beperken tot alleen geldige LTL-tokens volgens de grammatica. Dit voorkomt dat het model syntactisch onjuiste formules genereert.
4. Consistentiecontrole en Feedback:
   • Na generatie worden de formules gecontroleerd op syntactische validiteit.
   • Vervolgens wordt een satisfiability checker (BLACK) ingezet om te controleren of de verzameling formules logisch consistent is (d.w.z. of er een uitvoeringstrace bestaat die aan alle eisen voldoet).
   • Als een conflict wordt gedetecteerd (UNSAT), wordt een "unsatisfiable core" gegenereerd. Deze diagnostische informatie wordt teruggevoerd naar het LLM om de fout automatisch te corrigeren of de gebruiker te waarschuwen.

Belangrijkste Bijdragen

• Privacy-bevorderende Architectuur: LTLGUARD maakt het mogelijk om betrouwbare formele specificaties te genereren met lokale, compacte modellen (4B-14B), waardoor gevoelige eisen niet naar externe cloudservices hoeven te worden gestuurd.
• Geen Fine-tuning: Het framework bereikt hoge nauwkeurigheid door het combineren van prompt-engineering, RAFSL en symbolische redenering, in plaats van het kostbare en data-intensieve proces van fine-tuning.
• Iteratieve Verfijning: Door de integratie van automatische consistentiecontrole met feedbackloops, kan het systeem niet alleen syntactische fouten oplossen, maar ook semantische conflicten tussen meerdere eisen detecteren en oplossen.
• Omgaan met Ambiguïteit: Het framework erkent dat er geen "enkele waarheid" is voor informele eisen en biedt mechanismen om verschillende interpretaties te onderscheiden of te verhelderen.

Resultaten en Evaluatie

De auteurs hebben LTLGUARD geëvalueerd op vier compacte modellen (o.a. Qwen2.5-14B, Mistral-7B, Phi-3-mini) tegenover bestaande methoden en benchmarks.

• Vertaalnauwkeurigheid (RQ1):
  • De combinatie van syntactische beperkingen (SynCode) en RAFSL leidt tot aanzienlijke verbeteringen. Voor het Mistral-7B-model steeg de syntactische validiteit van 10% naar 92,8% en de semantische correctheid van 7,1% naar 40%.
  • Op de moeilijke "nl2spec" benchmark (36 instances) bereikte LTLGUARD met Qwen2.5-14B een semantische nauwkeurigheid van 75,0% (bij overlap met trainingsdata) en 50,0% (zonder overlap). Dit presteert beter dan veel niet-interactieve methoden met veel grotere modellen en benadert de prestaties van interactieve methoden met topmodellen zoals Codex.
• Robuustheid (RQ2):
  • Het systeem toont sterke robuustheid tegenover herschrijvingen van eisen (rephrasing) en hernoeming van atomaire proposities. Variant V6 (met SynCode en RAFSL) behaalde perfecte robuustheid bij het hernoemen van variabelen.
• Consistentiecontrole (RQ3):
  • De consistentiechecker slaagde erin om zowel inherente tegenstrijdigheden in de eisen als vertaalfouten te detecteren. Bijvoorbeeld, het detecteerde dat een vertaling van "requests will not be granted" als G(¬ request) in plaats van G(¬ granted) leidde tot een logisch conflict met andere eisen, wat de gebruiker kon helpen de fout te vinden.

Betekenis en Toekomstperspectief

LTLGUARD bewijst dat het niet nodig is om enorme, dure LLM's te gebruiken om formele methoden toegankelijk te maken voor industriële toepassingen. Door slimme integratie van compacte modellen met symbolische redenering, kan men:

1. Privacy en Kosten: Lokale implementaties mogelijk maken zonder in te leveren op kwaliteit.
2. Betrouwbaarheid: Syntactische en semantische fouten systematisch oplossen.
3. Toekomst: De auteurs plannen uitbreidingen naar meer expressieve logica's (zoals LTL met verleden en Signal Temporal Logic) en het integreren van visuele voorbeelden (traces) om de ambiguïteit verder te reduceren.

Kortom, LTLGUARD is een doorbraak in het maken van formele specificatie-tools die zowel toegankelijk als betrouwbaar zijn, zelfs met beperkte rekenkracht.