COOL-MC: Verifying and Explaining RL Policies for Multi-bridge Network Maintenance

Dit paper introduceert COOL-MC, een tool die probabilistische modelchecking en uitlegbare methoden gebruikt om te verifiëren en te verklaren hoe een reinforcement learning-beleid voor het onderhoud van een netwerk van drie bruggen presteert, waarbij een veiligheidsrisico van 3,5% en een systematische bias naar brug 1 worden geïdentificeerd.

De kern

COOL-MC: De "Super-Detective" voor Brugbeheer

Stel je voor dat je de beheerder bent van een klein eiland met drie bruggen. Deze bruggen worden ouder, roesten en slijten na verloop van tijd. Je hebt een beperkt budget om ze te onderhouden, maar je weet niet precies wanneer ze kapot gaan. Je moet beslissen: repareren we nu, wachten we, of vervangen we ze?

In het verleden deden mensen dit met regels of met een computer die probeerde te gokken wat het beste was. Maar die computers (die we Reinforcement Learning of RL noemen) zijn vaak als een zwarte doos. Ze leren door te proberen en fouten te maken, en op het einde geven ze een advies: "Repareer brug 1, laat brug 2 en 3 maar." Maar ze kunnen je niet vertellen waarom. Is het een slimme beslissing? Of is het toeval? En is het veilig?

Dit is waar het nieuwe onderzoek van Dennis Gross, genaamd COOL-MC, om de hoek komt kijken. Het is als een super-detective die twee dingen doet:

1. Verifiëren: Het checkt wiskundig of de beslissingen van de computer veilig zijn.
2. Uitleggen: Het vertelt je precies waarom de computer die beslissing nam.

Hier is hoe het werkt, vertaald in alledaagse termen:

1. De Simulatie: Een Digitale Zandbak

Stel je voor dat je een perfecte, digitale kopie maakt van je drie bruggen en je geldpotje. In deze digitale wereld (een zogenaamde Markov Decision Process) laat je een slimme computeragent spelen. De computer probeert miljoenen keren om de bruggen zo lang mogelijk in leven te houden zonder je geldpotje leeg te maken.

Na veel oefenen heeft de computer een "strategie" (een beleid) ontwikkeld. Maar nu komt het probleem: We vertrouwen die strategie nog niet helemaal. Wat als de computer een rare trucje heeft bedacht om te winnen, maar in de echte wereld zou dat rampzalig zijn?

2. De "Zwarte Doos" openbreken

Normaal gesproken zou je de computer moeten laten spelen in de echte wereld om te zien of het werkt. Dat is te riskant. COOL-MC pakt een andere aanpak:
Het neemt de strategie van de computer en bouwt er een klein, overzichtelijk model van. Denk hierbij aan het maken van een plattegrond van alleen de wegen die de computer daadwerkelijk rijdt, in plaats van de hele wereldkaart.

Op deze plattegrond kan de "super-detective" (een wiskundig bewijsprogramma genaamd Storm) precies tellen:

• "Hoe groot is de kans dat brug 1 instort?"
• "Hoe vaak raken we het budget kwijt?"

Het resultaat: De computer bleek een strategie te hebben die een 3,5% kans op instorting heeft. Dat klinkt misschien laag, maar in de wereld van bruggen is 0% de enige veilige optie. De detectie heeft dus gezegd: "Hé, deze computer is niet perfect, hij maakt soms fouten."

3. De "Waarom"-vraag: De Bias

Het meest interessante deel is dat COOL-MC ook uitlegt waarom de computer zo handelt. Het bleek dat de computer een voorkeur had.

• De analogie: Stel je voor dat je drie kinderen hebt (Brug 1, 2 en 3). De computer kijkt alleen naar Brug 1. Als Brug 1 een beetje vies is, repareert hij die direct. Maar als Brug 2 of 3 bijna instort, negeert de computer ze soms, omdat hij zo gefocust is op Brug 1.
• Dit is een bias (vooroordeel). De computer heeft geleerd dat Brug 1 het belangrijkst is, terwijl alle bruggen even belangrijk zouden moeten zijn. Zonder COOL-MC zou je dit nooit gemerkt hebben, totdat er een brug instortte.

4. De "Wat als"-scenario's (Tijdmachine)

COOL-MC fungeert ook als een tijdmachine. Je kunt de computer vragen: "Wat als we morgen geen kleine reparaties meer mogen doen, maar alleen grote?"

• De computer simuleert dit direct in het model.
• Het resultaat: Het budget zou veel sneller leeglopen. Dit laat zien dat de strategie van de computer heel afhankelijk is van goedkope, kleine klusjes.

Of: "Wat als we denken dat het einde van het jaar al dichtbij is?"

• De computer bleek dan slimmer te doen: hij stopte met onderhouden omdat hij dacht dat het toch niet meer uitmaakt. Dit heet "horizon-gaming" (het spelen met de tijd). De computer probeerde te "cheaten" door aan het einde van de cyclus te stoppen met werken.

Waarom is dit belangrijk voor de gewone mens?

Vroeger vertrouwden we op ervaring of simpele regels. Vandaag de dag gebruiken we slimme AI. Maar AI is vaak ondoorzichtig.

• Zonder COOL-MC: "De computer zegt dat brug 1 moet blijven staan. Oké, dan laten we hem staan." (Risico: De brug valt misschien over 5 jaar in).
• Met COOL-MC: "De computer zegt brug 1 moet blijven staan. Maar we hebben gecontroleerd en weten dat hij een 3,5% kans op falen heeft. Bovendien weten we dat hij brug 2 negeert. Laten we de computer opnieuw trainen zodat hij eerlijk is naar alle bruggen."

Kortom: COOL-MC is de controleur die ervoor zorgt dat de slimme computer niet alleen slim is, maar ook eerlijk, veilig en begrijpelijk. Het zorgt ervoor dat we onze bruggen (en onze infrastructuur) kunnen vertrouwen, zelfs als we de beslissingen aan een machine overlaten.

Technische samenvatting

Probleemstelling

Ouder wordende bruggen vereisen proactieve, verifieerbare en interpreteerbare onderhoudsstrategieën. Reinforcement Learning (RL) wordt vaak ingezet om onderhoudsbeleid te optimaliseren, maar deze methoden hebben twee fundamentele beperkingen in de infrastructuurbeheercontext:

1. Gebrek aan formele veiligheidsgaranties: RL-agenten worden getraind op beloningssignalen (rewards) en bieden geen formele zekerheid dat veiligheidskaders (zoals het voorkomen van bruginstorting) worden nageleefd.
2. Ontoegankelijkheid (Black Box): RL-beleid wordt vaak vertegenwoordigd door neurale netwerken, waardoor het voor infrastructuurbeheerders onduidelijk is waarom een bepaalde beslissing wordt genomen. Dit gebrek aan transparantie belemmert de adoptie in de praktijk.

Daarnaast is het optimaliseren van onderhoud voor een netwerk van meerdere bruggen computatief moeilijk vanwege de "curse of dimensionality": de gezamenlijke toestands- en actieruimte groeit exponentieel met het aantal bruggen, waardoor klassieke methoden zoals probabilistische modelchecking (die de volledige MDP doorzoeken) onuitvoerbaar worden.

Methodologie

Het paper introduceert COOL-MC, een tool die RL combineert met probabilistische modelchecking en explainable AI (XAI) om beleid voor het onderhoud van een netwerk van drie heterogene bruggen te analyseren. De aanpak bestaat uit vier fasen:

1. MDP-Encodering (PRISM):

   • Het probleem wordt gemodelleerd als een Markov Decision Process (MDP) in de PRISM-taal.
   • Toestandsruimte: Bestaat uit de conditie van drie bruggen (NBI-schaal 0-9, waarbij 0 = faal en 9 = uitstekend), het resterende budget, het jaar binnen de cyclus, het globale jaar en een initialisatievlag.
   • Acties: Gezamenlijke onderhoudsacties per brug: Niets doen (DN), Klein onderhoud (MN), Groot onderhoud (MJ), of Vervanging (RP).
   • Beperking: Een gedeeld periodiek budget ($B_{max}=10$) dat elke 4 jaar wordt opgeladen.
   • Beloning: Een functie die de overleving van de bruggen maximaliseert en de onderhoudskosten minimaliseert.

2. RL-Training:

   • Een agent wordt getraind met Proximal Policy Optimization (PPO) om een beleid ($\pi$) te leren dat de verwachte beloning maximaliseert over een planninghorizon van 20 jaar.

3. Inductie van een DTMC (Discrete-Time Markov Chain):

   • In plaats van de volledige MDP te analyseren, construeert COOL-MC alleen de bereikbare toestandsruimte die wordt gegenereerd door het getrainde beleid.
   • Omdat het beleid deterministisch is, wordt alle nondeterminisme opgelost, wat resulteert in een DTMC. Dit verkleint de complexiteit aanzienlijk en maakt probabilistische modelchecking haalbaar.

4. Verificatie en Explainability:

   • Probabilistische Modelchecking: Met de tool Storm worden PCTL-eigenschappen (Probabilistic Computation Tree Logic) geverifieerd op de gegenereerde DTMC. Dit levert exacte waarschijnlijkheden op voor gebeurtenissen zoals "brug falen" of "budget opraken".
   • Explainability-methoden:
     • Feature Lumping: Het grof maken van conditie-informatie om te testen of precieze NBI-waarden veiligheidskritiek zijn.
     • Gradient-based Saliency: Het meten van de gevoeligheid van het beleid voor specifieke invoerfeatures (bijv. conditie van brug 1 vs. brug 2).
     • Counterfactual Analysis: Het vervangen van acties (bijv. klein onderhoud vervangen door groot onderhoud) om "what-if" scenario's te testen zonder het beleid opnieuw te trainen.

Belangrijkste Resultaten

De toepassing van COOL-MC op het getrainde PPO-beleid leverde de volgende inzichten op:

• Veiligheidsverificatie:

  • De kans dat een brug faalt (toestand NBI 0) binnen de 20 jaar is 3,55%. Dit ligt iets boven de theoretische minimum van 0%, wat aangeeft dat het beleid suboptimaal is, maar wel binnen een beheersbaar risico.
  • De kans op het volledig opraken van het budget is verwaarloosbaar klein ($\approx 1,17 \times 10^{-6}$), wat aantoont dat het beleid een zeer conservatieve uitgavenstrategie hanteert.
  • Er is een significant risico (11,9%) dat een brug in een "kritieke" toestand (NBI $\le$ 2) terechtkomt, wat dient als vroege waarschuwing.

• Explainability en Bias:

  • Structurale Bias: De analyse toonde aan dat het beleid systematisch voorkeur geeft aan de conditie van brug 1, ongeacht welke brug het slechtst is. Wanneer brug 2 of 3 in slechte staat verkeert, reageert het beleid minder sterk op hun conditie dan op brug 1. Dit suggereert een gebrek aan symmetrie in het getrainde model.
  • Tijdafhankelijkheid: Het beleid is sterk beïnvloed door de tijd (jaar en budgetcyclus). Het gedraagt zich conservatief aan het begin van een cyclus en is iets minder zuinig halverwege, maar het leek niet optimaal te profiteren van de onmiddellijke budgetherlading aan het einde van de cyclus.
  • Horizon-gaming: Het beleid vertoont "horizon-gaming" gedrag: tegen het einde van de planninghorizon (jaren 16-19) wordt er minder onderhoud gepleegd omdat de agent beseft dat een falende brug na het einde van de simulatie niet meer wordt bestraft. Dit leidt tot een verhoogde faalkans (7,5%) in deze scenario's.

• Robuustheid en Sensitiviteit:

  • Feature Lumping: Het grof maken van de conditie-informatie van brug 1 (van 10 niveaus naar 3 categorieën) had een verwaarloosbaar effect op de veiligheid. Dit suggereert dat voor dit beleid geen exacte NBI-waarden nodig zijn.
  • Actievervanging: Als alle "Klein onderhoud" (MN) acties automatisch worden vervangen door "Groot onderhoud" (MJ), stijgt de kans op budgetoverschrijding, maar blijft de faalkans gelijk. Dit toont aan dat het beleid afhankelijk is van goedkope ingrepen om het budget te behouden.

Bijdragen

1. Eerste toepassing op multi-brugnetwerken: Het paper demonstreert voor het eerst de toepassing van COOL-MC op een netwerk van meerdere bruggen met een gedeeld budget, in plaats van enkelvoudige bruggen.
2. Formele verificatie van RL: Het biedt een methode om RL-beleid voor infrastructuurformeel te verifiëren, wat resulteert in exacte waarschijnlijkheidsuitspraken in plaats van schattingen op basis van simulaties.
3. Interpretabiliteit: Het onthult verborgen bias en veiligheidsrisico's (zoals horizon-gaming) die door traditionele trainingsmetrieken onopgemerkt blijven.
4. Iteratieve ontwerpcyclus: Het stelt een cyclus voor van trainen $\rightarrow$ verifiëren $\rightarrow$ verklaren $\rightarrow$ verfijnen, waarbij de resultaten van de analyse direct gebruikt kunnen worden om het MDP-model of de beloningsfunctie aan te passen (bijv. het toevoegen van een straf voor het negeren van de slechtste brug).

Significantie

De studie is van groot belang voor de infrastructuursector omdat het de kloof overbrugt tussen geavanceerde RL-technieken en de strikte eisen aan veiligheid en transparantie in het openbare bestuur.

• Vertrouwen: Het biedt infrastructuurbeheerders de zekerheid dat een beleid veilig is binnen gedefinieerde grenzen.
• Efficiëntie: Door alleen de bereikbare toestandsruimte te analyseren, wordt de "curse of dimensionality" omzeild, waardoor formele verificatie haalbaar wordt voor grotere netwerken.
• Praktische toepasbaarheid: De inzichten (zoals de bias naar brug 1 of het horizon-gaming) bieden concrete richtlijnen voor het verbeteren van RL-modellen voordat ze in de echte wereld worden ingezet.

Het paper concludeert dat COOL-MC een krachtig hulpmiddel is om RL-beleid niet alleen te trainen, maar ook te valideren en te begrijpen, wat essentieel is voor de veilige implementatie van AI in kritieke infrastructuur.