Technische Samenvatting: Een Survey naar de Verificatie van Reinforcement Learning Policies

1. Probleemstelling

Reinforcement Learning (RL) wordt steeds vaker ingezet in veiligheidskritische domeinen zoals autonoom rijden en energiesystemen. De inzet van RL-agenten in omgevingen met hoge inzet wordt echter belemmerd door een gebrek aan rigoureuze gedragsgaranties. RL-policies worden doorgaans geïmplementeerd als Deep Neural Networks (DNN's) met complexe, niet-lineaire beslissingsgrenzen die onder zeldzame omstandigheden, distributieverschuivingen of interactie-effecten onveilig gedrag kunnen vertonen.

In tegen tegenstelling tot supervised learning, waarbij correctheid wordt gedefinieerd door input-output robuustheid op vaste distributies, hangt de correctheid van RL fundamenteel af van interactie, feedback en distributieverschuiving tijdens de uitvoering. Een RL-policy vormt actief de staat-distributie die het tegenkomt via closed-loop controle. Dit leidt tot foutaccumulatie, falen bij zeldzame gebeurtenissen en veiligheidsschendingen die pas over lange horizonten (bijv. een policy die robuust is bij elke individuele tijdstap, kan toch falen door cumulatieve fouten) zichtbaar worden. Bijgevolg kunnen verificatie-objectieven in RL niet worden teruggebracht tot statische input-output analyse; ze moeten rekening houden met temporele afhankelijkheid, de koppeling tussen policy en omgeving, en onzekerheid tijdens de inzet.

De literatuur over RL-verificatie is momenteel conceptueel gefragmenteerd. Methoden worden ontwikkeld onder variërende aannames, richten zich op verschillende concepties van correctheid en opereren over verschillende temporele scopes, wat het moeilijk maakt om benaderingen te vergelijken of hun fundamentele relaties te begrijpen.

2. Methodologie en Taxonomie

Het artikel introduceert een verenigde taxonomie om bestaande post-training verificatiemethoden voor neurale netwerk-gebaseerde policies te organiseren. De taxonomie classificeert benaderingen langs drie primaire assen:

1. Verificatieparadigma: Maakt onderscheid tussen Formele methoden (het bieden van solide, deterministische garanties via verzadigbaarheid of bereikbaarheid) en Probabilistische methoden (het kwantificeren van risico en het bieden van garanties met een hoge betrouwbaarheid in stochastische omgevingen).
2. Temporele Scope:
   • Stap-gewijs (Step-wise): Analyseert een enkele policy-beslissing bij een gegeven staat, waarbij de toekomstige dynamiek wordt geabstraheerd. Dit is de meest volwassen klasse van tools.
   • Multi-stap: Redeneert over traject-niveau of closed-loop gedrag over eindige of oneindige horizonten, waarbij de interactie tussen de policy en de omgeving wordt gevangen.
3. Garantiekracht: Varieert van Sound & Complete (exacte verificatie) tot Sound (over-approximaties) en Probabilistisch (statistische grenzen).

De taxonomie bevat ook een "RL-gereedheid"-as, die aangeeft of een methode direct kan worden toegepast op getrainde RL-policies zonder substantiële abstractie of herformulering.

Belangrijke Verificatieformules

• Stap-gewijze Verificatie: Geformuleerd als het controleren of een policy een onveilige actie selecteert binnen een lokale inputregio $X$. Dit wordt vaak in kaart gebracht naar Neural Network Verification problemen met behulp van:
  • Verzadigbaarheid (SAT): Het zoeken naar een tegenvoorbeeld-input (NP-hard).
  • Bereikbaarheid (Reachability): Het berekenen van over-approximaties van bereikbare output-sets (bijv. via Abstract Interpretation of Lineaire Relaxatie).
  • Probabilistisch: Het schatten van de waarschijnlijkheid van onveilige acties zonder specifieke ruismodellen aan te nemen (bijv. PT-LiRPA).
• Multi-stap Verificatie: Geformuleerd als het bepalen of een gesloten traject een onveilige staat bereikt. Benaderingen omvatten:
  • Gelabelde MDP's & Temporele Logica: Het gebruik van Linear Temporal Logic (LTL) om traject-eigenschappen te specificeren, geverifieerd over het product van de door de policy geïnduceerde MDP en een automaat.
  • Neuro-symbolische Certificaten: Het combineren van geleerde policies met controle-theoretische certificaten (bijv. Control Barrier Functions, Lyapunov-functies) om veiligheid tijdens runtime af te dwingen.
  • Probabilistische Multi-stap: Het schatten van de waarschijnlijkheid van het voldoen aan temporele eigenschappen over trajecten via sampling of probabilistische grens-propagatie.
• Enumeratie-gebaseerde Verificatie: Een opkomend paradigma dat de set van alle inputs berekent die leiden tot onveilige acties (de preimage). Dit biedt informatie op regionaal niveau voor debugging en risicobeoordeling, hoewel exacte enumeratie #P-hard is.

3. Belangrijkste Bijdragen

1. Verenigde Taxonomie: Het artikel biedt de eerste uitgebreide organisatie van RL-verificatiemethoden langs de assen van paradigma, temporele scope en garantiekracht, waarbij de trade-offs tussen expressiviteit en schaalbaarheid worden verduidelijkt.
2. Formalisering: Het verenigt de theoretische fundamenten van RL-verificatieproblemen met een consistente notatie, waardoor impliciete aannames en beperkingen expliciet worden gemaakt.
3. Kritische Analyse: De survey analyseert de beperkingen van bestaande methoden, met name de schaalbaarheidsbottlenecks in multi-stap verificatie en de uitdagingen bij het toepassen van stap-gewijze tools op recurrente of multi-agent systemen.
4. Tool Benchmarking: Het biedt een empirische vergelijking van verificatietools (inclusclusief VNN-COMP deelnemers en preimage-approximatiemethoden) op RL-benchmarks (ACAS Xu, CartPole, LunarLander, Dubin's Rejoin), waarbij wordt benadrukt dat hoewel bound-propagation methoden goed schalen voor stap-gewijze taken, multi-stap verificatie een significante bottleneck blijft door de staat-ruimte explosie.

4. Resultaten en Observaties

• Schaalbaarheid vs. Precisie: Er is een fundamentele trade-off. Exacte methoden (SAT, exhaustieve enumeratie) zijn vaak onhandelbaar voor grote netwerken of lange horizonten. Over-approximatie en probabilistische methoden bieden betere schaalbaarheid maar kunnen conservatieve of probabilistische garanties bieden in plaats van absolute veiligheid.
• Volwassenheid van Stap-gewijze Verificatie: Stap-gewijze verificatie is het meest volwassen gebied, waarbij tools zoals $\alpha,\beta$-CROWN en NNV 2.0 veelbelovende schaling laten zien. Deze methoden kunnen echter niet redeneren over closed-loop executie of effecten op lange termijn.
• Uitdagingen van Multi-stap: Multi-stap verificatie wordt beperkt door de "vloek van dimensionaliteit" bij het modelleren van dynamiek en temporele specificaties. Neuro-symbolische benaderingen bieden sterke garanties, maar vertrouwen op aanvullende modelleringsaannames (bijv. bekende dynamiek of leerbare certificaten) die de algemeenheid beperken.
• Nut van Enumeratie: Enumeratie-gebaseerde benaderingen, hoewel computationeel duur, bieden unieke waarde voor policy debugging, gerichte dataverzameling en het kwantificeren van de ernst van residu-risico door de onveilige regio's van de staat-ruimte te karakteriseren.

5. Openstaande Uitdagingen en Toekomstige Richtingen

Het artikel identificeert verschillende kritieke hiaten tussen klassieke neurale netwerkverificatie en moderne RL-systemen:

• Recurrente Policies (RNN's): Verificatie van geschiedenis-afhankelijke policies in gedeeltelijk observeerbare omgevingen is uitdagend omdat veiligheid afhangt van haalbare verborgen-toestand trajecten. Huidige methoden slagen er vaak niet in om onderscheid te maken tussen realiseerbare en spurieuze verborgen toestanden, wat leidt tot overly conservatieve garanties of spurieuze tegenvoorbeelden.
• Multi-Agent RL (MARL): Veiligheid in MARL ontstaat uit interacties. Het verifiëren van gedecentraliseerde policies vereist redeneren over gezamenlijke staat-actie ruimtes en impliciete coördinatie, wat exponentiële complexiteit en nieuwe semantische uitdagingen introduceert met betrekking tot agent-specifieke versus team-niveau veiligheid.
• Omgevingsonzekerheid: De meeste methoden gaan uit van bekende of nauwkeurig benaderde dynamiek. Real-world systemen kampen met model-mismatch en non-stationariteit, wat vragen oproept over hoe men hanteerbare garanties kan bieden voor het closed-loop systeem onder onzekerheid.
• Moderne Architecturen: Het verifiëren van Transformers en attention-gebaseerde modellen is moeilijk omdat attention-mechanismen piecewise-lineaire aannames schenden, en deze modellen redeneren over variabel-lengte geschiedenissen, wat temporele abstractie bemoeilijkt.

6. Betekenis

Het artikel betoogt dat RL-verificatie niet louter een schaalbaarheidsprobleem is, maar een conceptueel probleem. Correctheid in RL moet worden gedefinieerd in termen van interacties, temporele afhankelijkheid en gedecentraliseerde beslissingen, in plaats van statische input-output robuustheid. De voorgestelde taxonomie dient als een verenigend perspectief om de gefragmenteerde literatuur te navigeren, waarbij de gebruiker helpt de juiste tools te selecteren op basis van hun specifieke verificatie-objectieven (bijv. lokale robuustheid versus veiligheid op lange termijn) en de structurele beperkingen van hun RL-systemen. De auteurs benadrukken dat toekomstige vooruitgang vereist dat frameworks beter aansluiten bij de RL-executie-semantiek terwijl ze een balans vinden tussen soundness en schaalbaarheid.