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

Die Studie stellt COOL-MC als Werkzeug vor, das durch die Kombination von Reinforcement Learning mit probabilistischer Modellprüfung und erklärbarer KI eine vertrauenswürdige, verifizierte und transparente Bestellpolitik für das Management von Thrombozytenbeständen in Blutbanken ermöglicht.

Das Wesentliche

🩸 Der große Blutplättchen-Rettungsplan: Wie KI lernt, nicht zu verschwenden und nicht zu verhungern

Stell dir vor, du bist der Chef eines riesigen Supermarkts. Aber du verkaufst keine Äpfel oder Milch, sondern Blutplättchen. Das ist ein ganz besonderer Supermarkt, denn hier gibt es eine extrem strenge Regel: Alles, was du hast, ist nach 5 Tagen abgelaufen und muss weggeschmissen werden.

Das Problem ist ein echtes Glücksspiel:

1. Zu viel bestellen: Wenn du zu viele Blutplättchen kaufst, laufen sie ab, bevor jemand sie braucht. Das ist teuer und eine Verschwendung einer lebenswichtigen Ressource.
2. Zu wenig bestellen: Wenn du zu wenig kaufst und morgen ein Notfallpatient kommt, hast du nichts. Das kann tödlich sein.

Früher haben Menschen versucht, das mit komplizierten Tabellen und Bauchgefühl zu lösen. Heute nutzen Forscher Künstliche Intelligenz (KI), genauer gesagt eine Art KI, die durch "Versuch und Irrtum" lernt (Reinforcement Learning). Diese KI hat gelernt, wann sie bestellen muss, um die Kosten für Verschwendung und das Risiko von Notfällen auszugleichen.

Aber hier liegt das Problem: Die KI ist ein Blackbox. Sie trifft Entscheidungen, aber niemand weiß genau, warum sie heute 10 Einheiten bestellt hat und morgen nur 2. In einem Krankenhaus, wo es um Leben und Tod geht, trauen sich die Ärzte und Blutspendezentren nicht, einer Blackbox blind zu vertrauen.

🕵️‍♂️ Die Lösung: COOL-MC (Der KI-Detektiv)

Hier kommt die Studie ins Spiel. Die Forscher haben ein Werkzeug namens COOL-MC entwickelt. Man kann sich COOL-MC wie einen super-scharfsinnigen Detektiv vorstellen, der die KI nicht nur beobachtet, sondern sie auch versteht und prüft.

Statt die KI einfach nur laufen zu lassen, macht COOL-MC folgendes:

1. Die Landkarte erstellen: Die KI hat gelernt, wie sie sich verhält. COOL-MC zeichnet eine Landkarte aller möglichen Szenarien, die die KI tatsächlich durchläuft. Es ignoriert alles, was die KI nie tun würde (wie einen Weg, den sie nie geht). Das spart enorm viel Rechenleistung.
2. Die Sicherheitsprüfung (Der Test): Der Detektiv fragt die Landkarte: "Wie hoch ist die Wahrscheinlichkeit, dass wir in 200 Tagen komplett ohne Blutplättchen dastehen?" oder "Wie oft landen wir in einer Situation, wo wir so viel haben, dass es abläuft?"
   • Das Ergebnis: Die KI ist ziemlich gut! Die Chance auf einen totalen Mangel liegt bei nur 2,9 %, und die Chance auf eine Verschwendung bei nur 1,1 %.
3. Die Erklärung (Das "Warum"): Jetzt wird es spannend. Der Detektiv fragt: "Was ist dir am wichtigsten?"
   • Er nimmt der KI quasi die Augenbande ab und sagt: "Vergiss mal, welcher Wochentag ist heute." -> Die KI macht fast keinen Fehler.
   • Er sagt: "Vergiss mal, wie alt die Blutplättchen im Lager sind." -> KATASTROPHE! Die KI gerät sofort in Panik und bestellt falsch.
   • Die Erkenntnis: Die KI schaut nicht auf den Kalender (Montag oder Freitag ist ihr egal), sondern sie schaut genau auf das Alter der Vorräte. Sie weiß genau, welche Blutplättchen bald ablaufen und welche noch frisch sind.

🎭 Das "Was-wäre-wenn"-Spiel

Der Detektiv spielt noch ein Spiel: Was wäre, wenn wir die KI zwingen, anders zu handeln?

Stell dir vor, die KI bestellt normalerweise 14 Einheiten. Der Detektiv sagt: "Okay, wir verbieten dir, 14 zu bestellen. Du musst stattdessen immer nur 6 bestellen."

• Erwartung: Das sollte doch gefährlich sein, oder?
• Realität: Nicht wirklich. Die Wahrscheinlichkeit eines Mangels ändert sich kaum.
• Warum? Weil die KI diese großen Bestellungen nur dann tätigt, wenn sie ohnehin schon einen riesigen Sicherheitsvorrat hat. Sie bestellt 14 nur, wenn sie "sicher" ist. Wenn sie 6 bestellt, ist sie immer noch sicher. Das zeigt, dass die KI sehr clever und vorsichtig ist.

🏆 Warum ist das wichtig?

Früher haben wir KI-Systeme nur daran gemessen, ob sie "günstig" waren. Aber in der Medizin reicht "günstig" nicht. Wir brauchen Sicherheit und Verständlichkeit.

Diese Studie zeigt, dass wir mit COOL-MC:

1. Beweisen können, dass die KI sicher ist (wie ein Sicherheitsgutachten für ein Flugzeug).
2. Verstehen können, worauf die KI achtet (sie achtet auf das Alter der Ware, nicht auf den Wochentag).
3. Vertrauen aufbauen können, damit Blutspendezentren diese KI wirklich einsetzen können, um Leben zu retten.

Zusammengefasst: Die Forscher haben eine KI trainiert, die Blutplättchen bestellt. Aber statt sie einfach loszulassen, haben sie einen Detektiv (COOL-MC) hingeschickt, der die KI durchleuchtet, ihre Sicherheitsgarantien prüft und uns erklärt, dass sie klüger ist, als wir dachten: Sie achtet genau auf das, was zählt – das Verfallsdatum.

Technische Zusammenfassung

1. Problemstellung

Die Verwaltung von Thrombozyten- (Blutplättchen-) Beständen stellt eine kritische Herausforderung für Blutbanken dar. Thrombozyten haben eine sehr kurze Haltbarkeit von nur fünf Tagen. Die täglichen Bedarfe sind stochastisch und schwer vorherzusagen. Blutbanken müssen daher eine Balance finden zwischen:

• Überbeständen: Dies führt zu kostspieligem Verfall (Waste) der knappen Ressource.
• Unterbeständen: Dies führt zu lebensbedrohlichen Engpässen für Patienten.

Dieses sequenzielle Entscheidungsproblem wird als Markov-Entscheidungsprozess (MDP) modelliert. Während Reinforcement Learning (RL) effektive Bestellungenstrategien lernen kann, bleiben die resultierenden neuronalen Politiken oft „Black Boxes". In sicherheitskritischen Bereichen wie dem Gesundheitswesen ist dies problematisch, da:

1. Die Sicherheit nicht formal garantiert werden kann (z. B. Wahrscheinlichkeit eines Engpasses).
2. Die Entscheidungsgründe der KI nicht nachvollziehbar sind (Interpretierbarkeit), was die Akzeptanz bei Praktikern behindert.

2. Methodik: COOL-MC

Das Paper stellt die Anwendung von COOL-MC vor, einem Werkzeug, das RL mit probabilistischer Modellprüfung (Probabilistic Model Checking) und erklärbarer KI (Explainable AI) kombiniert. Der Ansatz umfasst vier Hauptschritte:

A. MDP-Modellierung und Training

• Modell: Basierend auf einem MDP von Haijema et al. für eine regionale Blutbank in den Niederlanden. Der Zustand umfasst den Wochentag, ausstehende Bestellungen und die altersstrukturierte Lagerbestände (5 Altersklassen).
• Aktionen: Bestellungen von 0 bis 30 aggregierten Einheiten.
• Training: Ein Deep RL-Agent wird mit dem PPO-Algorithmus (Proximal Policy Optimization) trainiert, um die kombinierten Kosten aus Engpässen und Verfall zu minimieren (Kostenverhältnis 5:1).

B. Konstruktion des induzierten DTMC

Anstatt den gesamten, oft unüberwindbaren Zustandsraum des MDP zu analysieren, konstruiert COOL-MC einen induzierten diskreten zeitlichen Markov-Kette (DTMC).

• Dies geschieht durch eine Tiefensuche, die nur die erreichbaren Zustände unter der trainierten Policy verfolgt.
• Dies löst das „Curse of Dimensionality"-Problem und reduziert den Speicherbedarf drastisch (im Experiment um >99,6 %).
• Der resultierende DTMC ist deterministisch bezüglich der Aktionen (da die Policy festlegt, was getan wird) und probabilistisch bezüglich der Übergänge (Nachfrage).

C. Formale Verifikation (PCTL)

Auf dem induzierten DTMC werden Eigenschaften in der PCTL (Probabilistic Computation Tree Logic) spezifiziert und mit dem Modellprüfer Storm verifiziert.

• Beispielabfrage: „Ist die Wahrscheinlichkeit, innerhalb von 200 Schritten einen vollständigen Engpass (empty) zu erreichen, kleiner als 5 %?"
• Dies liefert exakte quantitative Werte (Wahrscheinlichkeiten, erwartete Schritte) statt nur Schätzungen durch Simulation.

D. Erklärbarkeit (Explainability)

Um zu verstehen, warum die Policy so entscheidet, werden vier Methoden angewendet, die mit der DTMC-Verifikation gekoppelt sind:

1. Feature-Pruning: Eingangsmerkmale (z. B. Wochentag, Lagerbestand) werden aus dem neuronalen Netz entfernt (Gewichte auf 0 gesetzt). Die Änderung der Sicherheitswahrscheinlichkeit zeigt die globale Wichtigkeit des Merkmals.
2. Feature-Permutation Importance: Werte eines Merkmals werden lokal in den Zuständen vertauscht, um die lokale Sensitivität der Policy zu messen.
3. Action Labeling: Zustände werden mit den gewählten Aktionen markiert, um PCTL-Abfragen über das Verhalten der Policy zu ermöglichen (z. B. „Wie oft wird maximal bestellt?").
4. Counterfactual Analysis: Spezifische Aktionen werden durch andere ersetzt (z. B. große Bestellungen durch kleine), und das Modell wird erneut verifiziert, um „Was-wäre-wenn"-Szenarien ohne Neutraining zu testen.

3. Wichtige Ergebnisse

Sicherheitsgarantien

• Die trainierte PPO-Policy erreicht eine Engpasswahrscheinlichkeit von 2,9 % und eine Vollbestands-Wahrscheinlichkeit (potenzieller Verfall) von 1,1 % innerhalb eines Horizonts von 200 Schritten.
• Im Vergleich zur optimalen Policy (berechnet durch vollständige MDP-Verifikation, die bei diesem Maßstab oft unmöglich ist) ist die Performance gut, aber die formale Verifikation liefert die notwendigen Sicherheitsgarantien.
• Die Analyse zeigt, dass etwa die Hälfte der Engpässe durch einen schrittweisen Abfall des Bestands vorhergesagt werden kann (Warnzone), während die andere Hälfte durch plötzliche Nachfragespitzen ohne Vorwarnung eintritt.

Verhaltensanalyse und Treiber

• Haupttreiber: Die Policy konzentriert sich fast ausschließlich auf die Altersverteilung des Lagerbestands (insbesondere die frischen Einheiten $x_4, x_5$ für Vermeidung von Engpässen und die ältesten Einheiten $x_1$ für Vermeidung von Überbeständen).
• Irrelevante Merkmale: Der Wochentag und ausstehende Bestellungen haben einen vernachlässigbaren Einfluss auf die Sicherheitswahrscheinlichkeiten.
• Diversität der Strategie: Die Policy nutzt eine breite Palette von Bestellmengen. Die meisten werden schnell erreicht, während 7 der 31 möglichen Bestellmengen nie gewählt werden.
• Counterfactual-Ergebnis: Der Ersatz von mittelgroßen Bestellungen (14 Einheiten) durch kleinere (6 Einheiten) in 11,8 % der Zustände ändert die Sicherheitswahrscheinlichkeiten kaum. Dies zeigt, dass diese Bestellungen in gut gepufferten Zuständen getätigt werden und nicht kritisch für die Sicherheit sind.

4. Hauptbeiträge

1. Erste formale Analyse: Dies ist die erste Anwendung formaler Verifikation und Erklärung auf eine RL-Policy für das Thrombozyten-Bestandsmanagement.
2. Skalierbarkeit: Demonstration, dass COOL-MC durch die Konstruktion induzierter DTMCs die Verifikation auch in komplexen Umgebungen ermöglicht, wo eine vollständige MDP-Analyse unmöglich wäre.
3. Strukturelles Verständnis: Transformation von reinen Kostenmetriken in ein strukturiertes Verständnis der Policy-Logik (welche Merkmale sind wichtig, wann werden sie genutzt, welche Aktionen sind redundant).
4. Praktische Anwendbarkeit: Bereitstellung eines Workflows für Blutbanken, um neue Bestellungenstrategien vor dem Einsatz auf Sicherheitskriterien zu prüfen und deren Robustheit zu bewerten.

5. Bedeutung und Ausblick

Das Paper zeigt, dass COOL-MC eine Brücke zwischen der Leistungsfähigkeit von Deep RL und den strengen Anforderungen an Sicherheit und Nachvollziehbarkeit im Gesundheitswesen schlägt. Es ermöglicht:

• Auditierbare Entscheidungen: Blutbankmanager können nachvollziehen, warum eine Bestellung getätigt wird.
• Risikominimierung: Formale Garantien für die Wahrscheinlichkeit von Engpässen.
• Robustheitsprüfung: Analyse, wie sich Änderungen in der Nachfrage oder Messungenauigkeiten auf die Policy auswirken.

Die Arbeit legt den Grundstein für den Einsatz von verifizierbaren und erklärbaren KI-Systemen in sicherheitskritischen Lieferketten des Gesundheitswesens.