COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management

Dit artikel introduceert COOL-MC, een tool die versterkt leren combineert met probabilistische modelchecking en uitlegbare AI om een getraind beleid voor het beheer van bloedplaatjesvoorraden formeel te verifiëren en te verklaren, waardoor transparante en betrouwbare besluitvorming in deze veiligheidskritieke gezondheidszorgtoepassing mogelijk wordt.

De kern

Het Koelkast-Dilemma: Hoe AI en Wiskunde Reden om Bloedplaatjes niet te Verspillen

Stel je voor dat je een enorme koelkast beheert voor een ziekenhuis. Maar dit is geen gewone koelkast met melk en kaas. Hierin liggen bloedplaatjes: levensreddende middelen voor mensen met kanker of ernstige bloedingen.

Het probleem? Deze bloedplaatjes zijn extreem kwetsbaar. Ze gaan slechts vijf dagen mee.

• Als je er te weinig bestelt, kunnen patiënten sterven omdat er niets beschikbaar is.
• Als je er te veel bestelt, verlopen ze voordat ze gebruikt worden. Dat is niet alleen een enorme geldverspilling, maar ook een moreel dilemma: je gooit een schaars levensreddend middel weg.

Vroeger deden mensen dit met complexe spreadsheets en ervaring. Nu proberen wetenschappers Kunstmatige Intelligentie (AI) te gebruiken om dit te regelen. De AI leert door te "proberen en te falen" (een techniek genaamd Reinforcement Learning). Maar hier zit de hak: de AI is een zwarte doos. We weten dat het werkt, maar we weten niet waarom het op dinsdag 10 eenheden bestelt en op woensdag 3. In een ziekenhuis, waar mensenlevens op het spel staan, is "het werkt wel" niet genoeg. We moeten het kunnen controleren en uitleggen.

Hier komt dit onderzoek, genaamd COOL-MC, om de hoek kijken.

De Oplossing: De "Spooktocht" door de AI

Stel je voor dat je een nieuwe, super-snelle auto hebt die zelf kan rijden. Je wilt weten of hij veilig is. Je kunt hem niet zomaar op de snelweg zetten om te zien of hij crasht. In plaats daarvan bouw je een virtuele simulatie van alle mogelijke routes die de auto kan nemen.

COOL-MC doet precies dit met de AI voor bloedplaatjes:

1. De AI maakt een routeplan: De AI heeft een strategie bedacht om te bestellen.
2. De "Bereikbare Wereld": In plaats van alle denkbare situaties in de wereld te bekijken (wat te veel is voor een computer), kijkt COOL-MC alleen naar de situaties die de AI echt tegenkomt. Het is alsof je alleen de wegen op een kaart tekent die de auto daadwerkelijk rijdt, en de rest van de wereld negeert. Dit maakt het berekenen veel sneller en lichter.
3. De Wiskundige Politie: Vervolgens laat de onderzoekers een wiskundige "politieagent" (een tool genaamd probabilistic model checking) deze route controleren. Ze stellen vragen als: "Wat is de kans dat we binnen 200 dagen volledig zonder voorraad zitten?" of "Hoe vaak raken we de voorraad vol?"

Wat hebben ze ontdekt? (De Verhalen)

Het onderzoek liet zien dat de AI een slimme, maar soms verrassende strategie heeft:

• De "Kijk naar de Ouderdom"-Strategie:
  De AI negeert bijna alles wat niet direct met de ouderdom van de bloedplaatjes te maken heeft. Of het nu dinsdag is of vrijdag, of er bestellingen onderweg zijn... de AI kijkt vooral naar: "Hoe oud is mijn oudste voorraad?" en "Hoe vers is mijn nieuwste voorraad?".

  • Analogie: Het is alsof een kok alleen kijkt naar de datum op de melkdoos, en niet naar de dag van de week of de weersvoorspelling.

• De "Onzichtbare" Bestellingen:
  De AI heeft 31 mogelijke bestelhoeveelheden (van 0 tot 30). Maar ze bleek dat de AI zeven van deze opties nooit gebruikt. Het is alsof je een auto hebt met 31 versnellingen, maar je rijdt alleen in versnelling 1, 2, 5 en 8. De andere versnellingen zijn voor deze specifieke situatie gewoon overbodig.

• De "Wat-als"-Test (Het Verwissel-experiment):
  De onderzoekers deden een gekke test: "Wat als we alle grote bestellingen (14 eenheden) vervangen door kleine bestellingen (6 eenheden)?"
  Het resultaat? Niets veranderde. De kans op een tekort of een vol magazijn bleef bijna hetzelfde.

  • Betekenis: Dit betekent dat de AI die grote bestellingen alleen doet op momenten dat het magazijn al zo vol zit dat het geen kwaad kan om een beetje minder te bestellen. De AI heeft een enorme "veiligheidsbuffer" opgebouwd. Het is alsof je een paraplu meeneemt op een dag dat het regent, maar je doet het ook op een dag dat het alleen een beetje bewolkt is, omdat je zeker weet dat het niet gaat stormen.

Waarom is dit belangrijk?

Vroeger was het vertrouwen in AI voor ziekenhuizen moeilijk. Managers dachten: "Ik vertrouw dit niet, ik snap niet hoe het werkt."

Met COOL-MC kunnen ze nu zeggen:
"We hebben de AI niet alleen getraind, we hebben hem ook gecontroleerd. We weten met wiskundige zekerheid dat de kans op een tekort minder dan 3% is. We weten dat hij kijkt naar de ouderdom van de voorraad. En we weten dat hij veilig is, zelfs als we kleine fouten maken in de bestellingen."

Conclusie

Dit onderzoek is als het bouwen van een transparante glazen muur rondom een zwarte doos. Het maakt de beslissingen van de AI zichtbaar, controleerbaar en begrijpelijk. Voor bloedbanken betekent dit dat ze eindelijk met een gerust hart AI kunnen inzetten om ervoor te zorgen dat er altijd genoeg bloedplaatjes zijn voor de patiënten die het nodig hebben, zonder dat er onnodig veel verspild wordt.

Het is een stap van "hopelijk werkt het" naar "we weten zeker dat het werkt, en we weten waarom."

Technische samenvatting

Probleemstelling

Thrombocyten (bloedplaatjes) hebben een zeer korte houdbaarheid van slechts vijf dagen. Bloedbanken staan voor een complexe uitdaging: ze moeten dagelijks bestelbeslissingen nemen onder onzekere vraag om een balans te vinden tussen:

1. Overschotten: Te veel bestellen leidt tot dure verspilling van een schaars middel (veroudering).
2. Tekorten: Te weinig bestellen kan leiden tot levensbedreigende tekorten voor patiënten.

Hoewel Reinforcement Learning (RL) effectieve bestelbeleid kan leren voor dit Markov Decision Process (MDP), blijven de resulterende neurale netwerken "black boxes". Dit gebrek aan interpretatie en het onvermogen om formele veiligheidsgaranties te geven, vormt een grote barrière voor de adoptie in veiligheidskritieke domeinen zoals de gezondheidszorg. Managers moeten begrijpen waarom een beleid een bepaalde bestelling doet en of het rekening houdt met de leeftijdsverdeling van de voorraad.

Methodologie: COOL-MC

De auteurs passen COOL-MC toe, een tool die RL combineert met probabilistische modelchecking en explainable AI (XAI). De aanpak verloopt in vier fasen:

1. MDP Encodering:

   • Het probleem wordt gemodelleerd als een MDP (geïnspireerd door Haijema et al.) met een toestand die bestaat uit: dag van de week, hangende bestellingen, en de voorraad opgesplitst in 5 leeftijdsklassen (1 tot 5 dagen houdbaarheid).
   • Acties zijn bestelhoeveelheden (0 tot 30 geaggregeerde eenheden).
   • De beloning (penalty) straalt tekorten en verspilling af met een kostenverhouding van 5:1 (tekort is 5x zo duur als verspilling).
   • Het model is geïmplementeerd in het PRISM-taalformaat voor probabilistische verificatie.

2. RL Training:

   • Een agent wordt getraind met Proximal Policy Optimization (PPO) om een beleid te leren dat de totale penalty minimaliseert.
   • Het beleid wordt vertegenwoordigd door een feedforward neurale netwerk (3 verborgen lagen van 256 neuronen).

3. Constructie van de Geïnduceerde DTMC:

   • In plaats van de volledige MDP-ruimte te analyseren (wat ondoenlijk is door de "curse of dimensionality"), construeert COOL-MC een Discrete-Time Markov Chain (DTMC) die alleen de toestanden bevat die bereikbaar zijn onder het getrainde beleid.
   • Dit reduceert de staatruimte aanzienlijk (van ~1,68 miljoen toestanden naar ~5.200 bereikbare toestanden) en maakt formele verificatie mogelijk.

4. Verificatie en Uitleg (PCTL & XAI):

   • Verificatie: Eigenschappen worden gespecificeerd in PCTL (Probabilistic Computation Tree Logic). De tool Storm wordt gebruikt om exacte kansen te berekenen (bijv. "Wat is de kans op een volledig leeg magazijn binnen 200 stappen?").
   • Uitleg (Explainability):
     • Feature Pruning: Het verwijderen van invoerfeatures (bijv. leeftijd van voorraad) om te zien hoe de veiligheidskansen veranderen.
     • Feature Permutation Importance: Het randomiseren van feature-waarden per toestand om lokale belangrijkheid te meten.
     • Action Labeling: Het annoteren van toestanden met de gekozen actie om gedragspatronen te analyseren.
     • Counterfactual Analysis: Het vervangen van specifieke acties (bijv. grote bestellingen door kleinere) om "what-if" scenario's te testen zonder het beleid opnieuw te trainen.

Belangrijkste Resultaten

• Veiligheidskansen: Het getrainde PPO-beleid bereikt binnen een horizon van 200 stappen:

  • Een 2,9% kans op volledige uitputting (stockout).
  • Een 1,1% kans op een volle voorraad (potentiële verspilling).
  • Dit is aanzienlijk beter dan willekeurige strategieën, maar nog steeds hoger dan een theoretisch optimaal beleid (dat echter niet schaalbaar is voor complexe omgevingen).

• Feature Belangrijkheid:

  • De analyse toont aan dat het beleid primair reageert op de leeftijdsverdeling van de voorraad (vooral de jongste voorraad $x_4$ en $x_5$ voor het voorkomen van tekorten, en de oudste voorraad $x_1$ voor het voorkomen van overschot).
  • Features zoals de dag van de week en hangende bestellingen hebben een verwaarloosbare invloed op de beslissingen. Het negeren van de dag van de week leidt slechts tot een minimale toename in tekortkans.

• Gedragsanalyse:

  • Actiebereikbaarheid: Het beleid gebruikt een divers vervangingsstrategie; de meeste bestelhoeveelheden worden snel bereikt, maar 7 specifieke hoeveelheden worden nooit gekozen.
  • Counterfactualen: Het vervangen van middelgrote/grote bestellingen (14 eenheden) door kleinere bestellingen (6 eenheden) in 11,8% van de toestanden had geen significant effect op de veiligheidskansen. Dit suggereert dat deze bestellingen plaatsvinden in toestanden met een voldoende veiligheidsbuffer.

• Efficiëntie: De constructie van de geïnduceerde DTMC reduceerde de staatruimte met >99,6%, wat formele verificatie mogelijk maakt op hardware die een volledige MDP-analyse niet zou aankunnen.

Bijdragen en Significantie

1. Eerste Formele Analyse: Dit is het eerste werk dat een RL-beleid voor bloedplaatjesbeheer formeel verifieert en verklaart. Het vult de kloof tussen de prestaties van RL en de noodzaak aan transparantie in de gezondheidszorg.
2. Tooling (COOL-MC): Het demonstreert de kracht van COOL-MC om complexe, neurale RL-beleiden om te zetten in verifieerbare Markov-ketens, waardoor exacte probabilistische garanties kunnen worden gegeven.
3. Inzicht in "Black Box" Beleid: Door feature pruning en counterfactuals te gebruiken, krijgen bloedbankmanagers inzicht in waarom het beleid bepaalde beslissingen neemt (bijv. focus op veroudering vs. dag van de week) en onder welke omstandigheden het beleid robuust is.
4. Praktische Toepasbaarheid: De methode biedt een workflow voor pre-deployment verificatie. Managers kunnen nieuwe beleidsregels testen op veiligheidskansen en robuustheid tegen variaties in vraag of meetfouten zonder het beleid opnieuw te hoeven trainen.

Conclusie:
Het paper bewijst dat het combineren van RL met probabilistische modelchecking en explainability-methoden essentieel is voor de veilige implementatie van geautomatiseerde beslissingssystemen in de gezondheidszorg. COOL-MC biedt een transparant, auditabel raamwerk dat vertrouwen kan wekken in RL-gestuurde supply chain management systemen.