Technische Samenvatting: PlatoLTL

Probleemstelling

Een centrale uitdaging in multi-task reinforcement learning (RL) is het trainen van generalistische beleidsregels die in staat zijn taken uit te voeren die niet tijdens het trainen zijn gezien. Hoewel Lineaire Temporele Logica (LTL) is opgekomen als een krachtige formalisatie voor het specificeren van gestructureerde, tijdelijk uitgebreide taken, staan bestaande door LTL geleide RL-approaches voor een kritieke beperking: ze kunnen niet generaliseren naar ongezette vocabulaires van proposities (of "symbolen"). Huidige methoden vereisen dat alle geldige LTL-specificaties worden samengesteld uit een vaste, discrete vocabulaire van atomaire proposities die a priori bekend zijn. Dit beperkt hun toepasbaarheid tot taken waarbij proposities worden geparametriseerd door continue variabelen (bijvoorbeeld een object oppakken op een specifieke coördinaat $(x, y)$ of een klep draaien met een hoek $\theta$). Bestaande oplossingen ofwel discretiseren de parameterruimte, wat slecht schaalt met de resolutie, ofwel voegen ze parameters toe aan observaties, wat slecht schaalt in multi-task settings en faalt in het leren van gedeelde structuur over gerelateerde proposities heen.

Methodologie: PlatoLTL

De auteurs stellen PlatoLTL (Parameterized logic architecture for temporal objectives in LTL) voor, een nieuwe aanpak die beleidsregels in staat stelt om zowel compositieseel over LTL-structuren als parametrisch over proposities zero-shot te generaliseren.

Kernconcept: Geparametriseerde Predicaten

In plaats van atomaire proposities te behandelen als distincte, discrete tokens, modelleert PlatoLTL ze als instanties van atomaire predicaten met specifieke parameterwaarden. Een propositie $p$ wordt gedefinieerd als $p = f(x_f)$, waarbij $f$ een atomair predicaat is (een Booleaanse functie die een waarheidsuitspraak over de omgeving vertegenwoordigt) en $x_f$ vaste parameters zijn. Dit stelt de beleidsregel in staat om gedeelde structuur over gerelateerde proposities heen te leren door te conditioneren op het predicaattype en zijn parameters.

Architectuur

De aanpak maakt gebruik van een doel-geconditioneerd RL-kader waarbij de beleidsregel $\pi(a | s, \phi)$ wordt geconditioneerd op de LTL-specificatie $\phi$. De architectuur bestaat uit drie hoofdcomponenten:

1. Embedding van Predicaat-instanties:

   • Een atomaire propositie $p = f(x_f)$ wordt ontleed in zijn predicaattoken $f$ en parameters $x_f$.
   • Het predicaat $f$ wordt gemapt naar een leerbare embedding $\phi_{prd}(f)$.
   • De parameters $x_f$ worden doorgegeven aan een predicaatspecifiek parameter-embeddingsnetwerk $\rho_f(\cdot)$.
   • Deze embeddings worden samengevoegd en gefuseerd via een predicaatspecifiek netwerk $f_f(\cdot)$ om de propositie-embedding $\phi(p)$ te produceren. Dit fungeert als een geleerde transformatie van de basispredicaat-embedding, gemoduleerd door de parameters.

2. Sequentie-samenvoeging:

   • LTL-specificaties worden omgezet in Limit-Deterministische Büchi-automata (LDBA's).
   • Uit de LDBA wordt een reach-avoid-sequentie van Booleaanse formules geëxtraheerd, die een pad naar een accepterende cyclus vertegenwoordigt.
   • Elke Booleaanse formule in de sequentie wordt weergegeven als een Abstract Syntax Tree (AST).
   • Een Graph Convolutional Network (GCN) verwerkt deze AST's, waarbij het gebruik maakt van de propositie-embeddings voor bladerknopen en leerbare embeddings voor logische operatoren, om formule-embeddings te produceren.
   • Een Gated Recurrent Unit (GRU) verwerkt de sequentie van formule-embeddings (achter naar voren) om een enkele taak-embedding te genereren.

3. Uitvoering van het Beleid:

   • Het beleidsnetwerk (Actor-Critic) neemt de samengevoegde toestandsembedding (vanomgevingobservaties) en de taak-embedding.
   • Om LDBA $\epsilon$-transities (ongezette sprongen) te verwerken, wordt de actieruimte uitgebreid met een speciale $\epsilon$-actie. Het beleid leert te voorspellen wanneer deze transities moeten worden geactiveerd.
   • Tijdens evaluatie, als de LDBA-toestand verandert, wordt een nieuwe reach-avoid-sequentie geëxtraheerd en wordt het beleid opnieuw geconditioneerd op deze nieuwe sequentie.

Training

PlatoLTL wordt end-to-end getraind met Proximal Policy Optimization (PPO) met een curriculum van steeds uitdagendere reach-avoid-sequenties. Cruciaal is dat de trainingssequenties worden bemonsterd uit een verdeling van willekeurige sequenties in plaats van vast te zitten aan specifieke LTL-specificaties, waardoor het beleid de onderliggende structuur van predicaatinstanties kan leren en kan generaliseren naar ongezette specificaties.

Belangrijkste Bijdragen

1. Parametrische Modellering: Het voorstel om LTL-proposities te modelleren als geparametriseerde instanties van atomaire predicaten, waardoor generalisatie over continue parameterruimtes mogelijk wordt.
2. Nieuwe Architectuur: Een neurale netwerkarchitectuur die predicaatparameters zinvol mapt naar embeddings en deze samenvoegt om LTL-formules weer te geven via AST's en sequentiemodeling.
3. Zero-Shot Generalisatie: Het aantonen dat PlatoLTL zero-shot generalisatie bereikt, zowel compositieseel (over LTL-structuren) als parametrisch (over ongezette proposities).
4. Nieuwe Benchmarks: De introductie van vier nieuwe op predicaten gebaseerde benchmark-omgevingen (RGBZoneEnv, XYZEnv, XYXYEnv, FalloutWorld) die complexe, geparametriseerde LTL-specificaties ondersteunen, waardoor de bestaande literatuur wordt uitgebreid.
5. Empirische Validatie: Uitgebreide experimenten die de superieure prestaties en convergentiesnelheid van PlatoLTL tonen ten opzichte van state-of-the-art baselines (DeepLTL, LTL-GNN) en op parametrisatie gebaseerde methoden (Naïve, SIAMS).

Resultaten

Experimenten werden uitgevoerd op zowel discrete sets van proposities (trainings- en ongezette evaluatiesets) als continue sets van proposities.

• Discrete Generalisatie: Op ongezette evaluatieproposities behield PlatoLTL prestatie-pariteit met trainingsproposities (bijvoorbeeld ~99% slagingspercentage in RGBZoneEnv), terwijl baselines (DeepLTL, LTL-GNN) faalden in generalisatie en aanzienlijk lagere slagingspercentages vertoonden.
• Continue Generalisatie: In omgevingen met continue proposities (XYZEnv, XYXYEnv) bereikten baselines bijna nul slagingspercentages, ondanks toegang tot parameters. PlatoLTL bereikte hoge slagingspercentages (bijvoorbeeld >95% in XYZEnv) en lage episode-lengtes.
• Convergentie: PlatoLTL convergeerde aanzienlijk sneller dan baselines. Naarmate het aantal trainingsproposities toenam, nam de convergentiesnelheid van baselines gestaag af (wat onpraktische trainingstijden vereiste voor grote vocabulaires), terwijl PlatoLTL robuust en onaangetast bleef.
• Embedding-structuur: Principal Component Analysis (PCA) onthulde dat PlatoLTL een laag-dimensionale, gestructureerde embeddruimte leerde waarin gerelateerde proposities (bijvoorbeeld verschillende RGB-kleuren) coherente geometrieën vormden (bijvoorbeeld een kubus), terwijl baselines verspreide, hoog-dimensionale embeddings produceerden die op ruis leken.

Betekenis en Claims

Het artikel beweert dat PlatoLTL een fundamentele beperking in neuro-symbolisch RL aanpakt: het onvermogen om te generaliseren naar ongezette vocabulaires van proposities. Door proposities te behandelen als geparametriseerde instanties van predicaten, leert de aanpak onderbouwde associaties tussen taakparameters en de omgeving.

De auteurs positioneren PlatoLTL als een stap in de richting van het creëren van agenten die in staat zijn willekeurige complexe, lang-horizontale taken uit te voeren zonder een vaste, discrete vocabulaire te vereisen. Zij merken op dat, hoewel de aanpak ervan afhankelijk is dat predicaten a priori bekend zijn (een beperking die wordt gedeeld met eerdere werken, hoewel strikt genomen generalerend), het de schaalbaarheid en generalisatie in geparametriseerde settings aanzienlijk verbetert. Het werk suggereert dat het combineren van deze ruggengraat met methoden voor efficiëntie in exploratie en robuustheid zou kunnen leiden tot schaalbaarheid naar hoog-dimensionale, real-world robotische taken. De auteurs stellen bescheiden dat toekomstig werk deze combinaties en de automatische ontdekking van onderbouwde predicaten moet onderzoeken.