🤖 AI

Neuro-Symbolic Injection of LTLf Constraints in Autoregressive Reinforcement Learning Policies

Dit artikel stelt een neuro-symbolisch raamwerk voor dat constraints gebaseerd op Linear Temporal Logic over eindige sporen (LTLf) integreert in transformer-gebaseerde autoregressieve reinforcement learning-policies door specificaties te compileren naar differentieerbare deterministische eindige automaten, waardoor de naleving van constraints wordt verbeterd terwijl competitieve rendementen in offline RL-taken behouden blijven.

Oorspronkelijke auteurs: Ashkan Ansarifard (Sapienza University of Rome), Matteo Mancanelli (Sapienza University of Rome), Elena Umili (Sapienza University of Rome), Fabio Patrizi (Sapienza University of Rome)

Gepubliceerd 2026-06-09

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Ashkan Ansarifard (Sapienza University of Rome), Matteo Mancanelli (Sapienza University of Rome), Elena Umili (Sapienza University of Rome), Fabio Patrizi (Sapienza University of Rome)

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Het Grote Plaatje: Robots leren regels te volgen zonder trial-and-error

Stel je voor dat je een robot probeert te leren hoe hij door een doolhof moet navigeren. In de echte wereld leert de robot: "Au, dat moet ik niet doen," als hij tegen een muur botst. Maar in Offline Reinforcement Learning mag de robot de echte wereld niet aanraken. Hij mag alleen een gigantisch fotoalbum bestuderen van eerdere pogingen die door iemand anders zijn gemaakt.

Het probleem? De robot in het fotoalbum heeft misschien fouten gemaakt. Als je de robot simpelweg vertelt om "zoveel mogelijk punten te scoren", kan hij die fouten gaan kopiëren omdat ze in het verleden tot hoge scores leidden, zelfs als ze gevaarlijk waren.

Dit paper introduceert een nieuwe manier om deze robots te onderwijzen: Neuro-Symbolic Injection. Zie het als het geven van een "regelboek" aan de robot, geschreven in een strikte, logische taal (LTLf), en het dwingen om dat regelboek te bestuderen terwijl hij leert van het fotoalbum.

Het Kernprobleem: De "Beloningsval"

Standaard AI-modellen (zoals de modellen die in dit paper worden gebruikt, genaamd Transformers) zijn als briljante studenten die geobsedeerd zijn door het halen van een voldoende (het maximaliseren van de beloning). Ze kijken naar het fotoalbum en zeggen: "Oké, ik zie dat de robot in deze foto op een bom stapte, maar daarna later een enorme beloning kreeg. Dat ga ik ook doen!"

Maar in kritieke veiligheidssituaties (zo\nals zelfrijdende auto's of medische robots) is stappen op een bom een "Game Over". Je kunt niet simpelweg zeggen: "Nou, ik kreeg later een beloning." Je moet ervoor zorgen dat de robot nooit op de bom stapt, zelfs als dat betekent dat hij een langere route moet nemen.

De Oplossing: De "Verkeersregelaar" en de "Logica-motor"

De auteurs hebben een systeem gebouwd dat werkt als een Verkeersregelaar die naast de student-robot staat terwijl deze studeert.

Het Regelboek (LTLf): In plaats van vage instructies zoals "wees veilig", gebruiken de onderzoekers Linear Temporal Logic. Dit is als een nauwkeurig juridisch contract.
- Slechte instructie: "Probeer bommen te vermijden."
- LTLf-instructie: "Je moet altijd bommen vermijden, en je moet uiteindelijk het doel bereiken."
- Dit dekt de hele reis, niet alleen de volgende stap.
De Verkeersregelaar (De DFA): De computer vertaalt dat juridische contract naar een Deterministic Finite Automaton (DFA). Stel je een flowchart voor of een bordspel-kaart.
- Elke keer dat de robot een stap zet in zijn training, controleert de Verkeersregelaar de flowchart.
- "Ben je op een bom gestapt? Nee? Goed, ga naar het volgende vakje op de kaart."
- "Ben je op een bom gestapt? Ja? STOP. Je bent nu in de 'Fail'-zone."
De "Zachte" Duw (Differentiable Loss): Hier zit de magische truc. Normaal gesproken is een flowchart rigide: je bent ofwel veilig, ofwel dood. Maar een robot leert door minuscule aanpassingen aan zijn brein te maken (wiskundig gezien). Je kunt geen "dode" staat aanpassen.
- De auteurs hebben de Verkeersregelaar differentieerbaar gemaakt. Dit betekent dat de Regelaar niet alleen zegt "Fail"; de Regelaar zegt: "Je bent voor 90% veilig, maar je komt dichter bij de gevarenzone. Pas je brein een klein beetje aan om weg te bewegen van het gevaar."
- Dit creëert een Logic Loss. Het is als een docent die een student een cijfer geeft, niet alleen voor de eindtoets, maar voor elke stap van hun huiswerk, waarbij de student zachtjes wordt gecorrigeerd voordat hij een fatale fout maakt.

Hoe ze het hebben getest: Het "ColourBomb" Spel

Ze hebben dit getest in een grid-world spel genaamd ColourBomb.

Het Doel: Een gekleurde uitgang bereiken.
Het Gevaar: Rode "Bomb"-cellen die het spel direct beëindigen.
De Uitdaging: De robot moest leren het doel te bereiken zonder ooit op een bom te stappen.

Ze vergeleken twee soorten AI-modellen:

Decision Transformer (DT): Een model dat de volgende zet bepaalt op basis van de historie.
Trajectory Transformer (TT): Een model dat het hele pad in één keer voorspelt.

De Resultaten: Van "Chaos" naar "Kampioen"

Zonder de Logica-regelaar (De Baseline):
De robots waren rampzalig. Ze bleven op bommen stappen omdat ze alleen probeerden punten te maximaliseren op basis van de rommelige data die ze kregen. Ze faalden bijna 100% van de tijd om het doel veilig te bereiken.

Met de Logica-regelaar (De Nieuwe Methode):
Door de "Logic Loss" (de zachte duwtjes van de Verkeersregelaar) toe te voegen, veranderden de resultaten drastisch:

Veiligheid: De robots stopten met het raken van bommen. Ze behaalden 100% veiligheid in de beste instellingen.
Succes: Ze bereikten het doel succesvol.
Prestatie: Ze werden niet alleen veilig; ze scoorden ook daadwerkelijk hogere scores dan de onveilige robots, omdat ze geen tijd verspillen met doodgaan en opnieuw beginnen.

De Afweging: Het vinden van de "Sweet Spot"

De onderzoekers ontdekten een "Goldilocks"-zone.

Als de Logica-regelaar te zwak was (te weinig "duw"), negeerde de robot de regels en raakte hij bommen.
Als de Logica-regelaar te sterk was, werd de robot zo bang voor de regels dat hij bevroor en nooit bewoog (hij was veilig, maar bereikte het doel nooit).
Door de "sterkte" van de regelaar af te stemmen (een parameter genaamd $\alpha$ ), vonden ze de perfecte balans waarbij de robot zowel veilig als succesvol was.

Samenvatting

Dit paper laat zien dat je een AI kunt leren om strikte, complexe veiligheidsregels te volgen (zoals "vermijd altijd X, maar bereik uiteindelijk Y") zelfs wanneer je niet in de echte wereld kunt oefenen. Door die regels te vertalen naar een wiskundige "flowchart" en deze te gebruiken om het leerproces van de AI zachtjes te corrigeren, creëerden ze robots die veel veiliger en betrouwbaarder zijn dan robots die alleen op basis van beloning worden getraind.

Belangrijkste les: Je hoeft niet het hele brein van de robot of de data die hij bestudeert te herschrijven. Je hoeft alleen een "logica-laag" toe te voegen die fungeert als een constante, zachte gids, die ervoor zorgt dat de robot vanaf het begin de juiste gewoontes aanleert.

Technische Samenvatting: Neuro-symbolische Injectie van LTLf-constraints in Autoregressieve Reinforcement Learning Policies

Probleemstelling
In offline Reinforcement Learning (RL) leren agenten beleid (policies) uitsluitend uit vooraf verzamelde datasets zonder online interactie. Recente sequentie-modellerende benaderingen, zoals Trajectory Transformers (TT) en Decision Transformers (DT), hebben RL succesvol geformuleerd als een sequentie-generatieprobleem, maar zij optimaliseren doorgaans enkel voor cumulatieve beloning. Dit creëert een kritieke kloof in veiligheidskritische domeinen (bijv. robotica, autonome navigatie) waar beleid moet voldoen aan hoogwaardige, temporeel uitgebreide constraints. Standaard beloningsgebaseerde optimalisatie kan niet garanderen dat een beleid complexe temporele logische vereisten voldoet, zoals "uiteindelijk het doel bereiken terwijl altijd gevaren worden vermeden", vooral wanneer schendingen niet gecorrigeerd kunnen worden via trial-and-error exploratie in een offline setting.

Methodologie
De auteurs stellen een neuro-symbolisch framework voor dat LTL $_f$ -constraints (Linear Temporal Logic over finite traces) direct injecteert in het trainingsproces van autoregressieve transformer-gebaseerde beleidsmodellen. De kernmethodologie bestaat uit drie hoofdonderdelen:

LTL $_f$ naar DFA Compilatie: Hoogwaardige temporele specificaties worden gecompileerd naar Deterministische Eindige Automata (DFA's). Deze vertaling maakt het mogelijk om logische constraints te representeren als staat-transitie-systemen die sequenties van tokens kunnen verwerken.
Differentiabele Logica Loss: Om deze discrete automata te integreren in de continue optimalisatie van neurale netwerken, gebruiken de auteurs een differentiabele representatie.
- Soft Satisfaction Signals: In plaats van harde sampling, gebruikt het framework Gumbel-Softmax sampling om tijdens de training differentiabele, bijna one-hot token vectoren te genereren.
- DeepDFA Integratie: Deze soft tokens worden gevoed aan een "DeepDFA", een neurale relaxatie van de standaard DFA. Deze module berekent een probabilisch bevredigingssignaal dat de waarschijnlijkheid aangeeft dat de gegenereerde trajectorie de LTL $_f$ formule voldoet.
- Regularisatie: Een logica loss functie ( $L_\phi$ ) wordt afgeleid van de negatieve log-waarschijnlijkheid van bevrediging. Deze wordt gecombineerd met de standaard supervised sequentie-modelleringsverlies ( $L_{\mathcal{D}}$ ) via een gewogen som: $L = \alpha L_\phi + (1 - \alpha) L_{\mathcal{D}}$ , waarbij $\alpha$ een trade-off parameter is.
Architectuur-agnosticisme: Het framework is ontworpen om model-agnostisch te zijn binnen de klasse van autoregressieve sequentiemodellen. Het maakt gebruik van een gedeelde "logic adapter" om token-naar-symbool mapping en DFA rollouts af te handelen, waardoor het toepasbaar is op zowel TT als DT architecturen zonder hun onderliggende structuren te wijzigen.

Belangrijkste Bijdragen
Het artikel beschrijft drie primaire bijdragen:

Verenigd Neuro-Symbolisch Framework: Een methode om LTL $_f$ -constraints in transformer-gebaseerde offline RL-beleidsmodellen te injecteren met behulp van automata-gebaseerde modules die architectuur-agnostisch zijn.
Canonieke Evaluatie Stack: Een consistente end-of-episode evaluatiepipeline die dataset serialisatie, token-naar-symbool mapping en logische evaluatie afstemt, wat semantische mismatches tussen training en temporele logica-beoordeling voorkomt.
Empirische Analyse: Een systematische evaluatie in navigatiedomeinen die de trade-offs demonstreert tussen taakprestaties (return) en constraint-voldoening onder variërende niveaus van logische sturing.

Experimentele Resultaten
Het framework werd geëvalueerd in de ColourBomb navigatieomgeving, waarbij twee typen specificaties werden getest: Invariant Safety ( $G(\neg \text{bomb})$ ) en Reach-while-Safe ( $G(\neg \text{bomb}) \land F(\text{goal})$ ).

Decision Transformers (DT):
- Vanilla DT's (zonder logica-regularisatie) faalden volledig, waarbij ze bomcellen raakten en het doel niet bereikten.
- Het introduceren van logica-regularisatie met een hoge trade-off parameter ( $\alpha = 0.8$ ) bereikte 100% voldoening voor zowel de safety als de reach-while-safe specificaties.
- Cruciaal is dat deze hoge-constraint setting ook de gemiddelde return verbeterde (van -1.460 naar -0.780) door catastrofale fouten (bom-hits) te elimineren, wat aantoont dat constraint-voldoening in offline settings kan samenvallen met prestaties.
Trajectory Transformers (TT):
- Vanilla TT's vertoonden gedeeltelijke veiligheid-compliance maar een lage doelbereikking.
- Logica-regularisatie verbeterde de voldoeningspercentages en verminderde de bomb-hit rates. Voor de invariant safety taak leverde $\alpha = 0.8$ de beste resultaten op. Voor de complexere reach-while-safe taak bood een lagere weging ( $\alpha = 0.1$ ) de optimale balans, wat zowel de voldoening als de return verbeterde ten opzichte van de baseline.
- De auteurs merken op dat hoewel er verbeteringen werden waargenomen, deze in TT's minder uitgesproken waren dan in DT's, een discrepantie die openstaat voor toekomstig onderzoek.

Significantie en Claims
Het artikel claimt dat het integreren van symbolische achtergrondkennis direct in de leerdoelstelling — in plaats van het modificeren van de datarepresentatie of het vertrouwen op reward shaping — een veelbelovende richting is voor het verbeteren van de betrouwbaarheid van beleid in veiligheidskritische offline RL.

Belangrijke claims met betrekking tot de significantie van de methode zijn:

Directe Constraint Injectie: In tegenstelling tot benaderingen die vertrouwen op shielding (die een expliciet omgevingsmodel vereisen) of reward shaping (die moeilijk te ontwerpen is), injecteert deze methode temporele logica-kennis direct in de trainingsverliesfunctie.
Generaliteit: Het framework ondersteunt willekeurige LTL $_f$ formules, reikend voorbij de "safety fragment" naar liveness en complexe temporele combinaties.
Prestatiebehoud: De resultaten suggeren dat het afdwingen van strikte logische constraints niet noodzakelijkerwijs de taakprestaties verslechtert; in de geteste scenario's verbeterde het zelfs de returns door de catastrofale uitkomsten te voorkomen die vanilla modellen vaak tegenkwamen.

De auteurs hanteren een bescheiden toon en erkennen dat de aanpak momenteel beperkt is tot offline settings en dat de waargenomen verbeteringen in TT's minder uitgesproken waren dan in DT's. Zij identificeren toekomstig werk als het uitbreiden van de evaluatie naar aanvullende benchmarks, modelarchitecturen en het uitvoeren van uitgebreide end-to-end vergelijkingen met gevestigde Safe RL frameworks.