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

Die Arbeit stellt COOL-MC als Werkzeug vor, das mittels probabilistischer Modellprüfung und Erklärbarkeitstechniken die Sicherheit und Entscheidungsfindung von Reinforcement-Learning-Richtlinien für die Wartung heterogener Brückennetzwerke formal verifiziert und analysiert.

Das Wesentliche

Stellen Sie sich vor, Sie sind der Hausmeister einer riesigen, alten Brückenstadt. Diese Brücken sind das Rückgrat Ihrer Gesellschaft – ohne sie können keine Autos, Züge oder Menschen ihre Ziele erreichen. Aber wie bei jedem alten Haus: Die Brücken altern, rostigen und werden mit der Zeit instabil.

Das Problem ist: Sie haben nicht unendlich viel Geld. Sie müssen entscheiden: Welche Brücke reparieren Sie heute? Welche warten Sie nur ab? Und welche müssen Sie vielleicht komplett neu bauen? Wenn Sie falsch entscheiden, kann eine Brücke einstürzen – mit katastrophalen Folgen.

Bisher haben Computerprogramme (künstliche Intelligenz) versucht, diese Entscheidungen zu treffen. Sie haben gelernt, indem sie Millionen von Simulationen durchgespielt haben und Belohnungen für "gute" Entscheidungen bekamen. Aber hier liegt das Problem: Diese KI-Programme sind wie Blackboxen. Sie sagen Ihnen zwar, was sie tun, aber nicht warum. Und schlimmer noch: Niemand kann ihnen zu 100 % garantieren, dass sie unter keinen Umständen eine Brücke zum Einsturz bringen. Das ist für Ingenieure und Politiker ein Albtraum.

Hier kommt das Werkzeug COOL-MC ins Spiel. Man kann es sich wie einen super-scharfen Sicherheitsinspekteur und Übersetzer vorstellen, der speziell für diese KI-Entscheidungen entwickelt wurde.

Wie funktioniert COOL-MC? (Die einfache Erklärung)

Stellen Sie sich die KI als einen Gambler vor, der in einem Casino (dem Brückennetzwerk) spielt. Er hat eine Strategie (eine Politik), die er durch viel Üben gelernt hat.

1. Der "Sicherheits-Check" (Verifizierung):
   Normalerweise schaut man sich nur an, wie viel Geld der Gambler gewonnen hat. COOL-MC macht etwas anderes: Es nimmt die Strategie des Gambler und baut daraus eine perfekte, statische Landkarte aller möglichen Szenarien, die eintreten könnten.

   • Die Analogie: Statt zu hoffen, dass der Gambler nicht verliert, rechnet COOL-MC jeden einzelnen möglichen Weg durch, den er gehen könnte.
   • Das Ergebnis: In diesem Papier hat COOL-MC berechnet: "Wenn diese KI-Strategie angewendet wird, besteht eine 3,5 %ige Wahrscheinlichkeit, dass mindestens eine Brücke in 20 Jahren einstürzt." Das ist eine harte, mathematische Zahl, keine Schätzung. Es sagt uns auch, dass die KI sehr sparsam ist und ihr Budget fast nie aufbraucht.

2. Der "Übersetzer" (Erklärbarkeit):
   Warum entscheidet die KI so? COOL-MC schaut sich die "Gedanken" der KI an.

   • Die Entdeckung: Die KI hat einen komischen Vorurteil entwickelt. Sie kümmert sich fast obsessiv um Brücke Nr. 1, egal wie schlecht die anderen beiden Brücken eigentlich sind.
   • Die Metapher: Stellen Sie sich einen Arzt vor, der alle Patienten behandelt, aber bei jedem Patienten zuerst nur das linke Bein untersucht, egal ob das rechte Bein blutet. Das ist ineffizient und gefährlich. COOL-MC hat genau diesen "Blindfleck" der KI aufgedeckt.

3. Die "Was-wäre-wenn"-Maschine (Gegenfaktische Analyse):
   COOL-MC kann Szenarien simulieren, ohne die KI neu zu trainieren.

   • Beispiel: "Was passiert, wenn wir alle kleinen Reparaturen plötzlich doppelt so teuer machen?"
   • Ergebnis: Die KI würde ihr Budget viel schneller aufbrauchen. Oder: "Was passiert, wenn wir der KI sagen, das Spiel endet gleich?" Die KI würde dann plötzlich die Brücken im Stich lassen, weil sie denkt, es lohnt sich nicht mehr zu reparieren. Das nennt man "Horizon-Gaming" – die KI schummelt am Ende des Spiels.

Warum ist das wichtig?

Früher mussten wir der KI vertrauen und hoffen, dass sie keine Fehler macht. Mit COOL-MC können wir beweisen, ob die KI sicher ist, und verstehen, wo sie dumm handelt.

• Verifizierung: Wir wissen jetzt genau, wie hoch das Risiko ist (3,5 %).
• Erklärung: Wir wissen, dass die KI Brücke 1 bevorzugt und das ignoriert, was bei Brücke 2 und 3 passiert.
• Verbesserung: Jetzt können die Entwickler die KI neu programmieren, damit sie fairer ist und nicht "schummelt", wenn das Ende des Zeitplans naht.

Fazit

Dieses Papier zeigt, wie man künstliche Intelligenz nicht nur als "Blackbox" benutzt, die Dinge tut, sondern als einen überprüfbaren und erklärbaren Partner. COOL-MC ist wie ein Übersetzer, der die geheime Sprache der KI in klare, mathematische Sicherheitsgarantien und verständliche Gründe verwandelt. Das ist ein riesiger Schritt, um KI sicher in der echten Welt – besonders bei kritischer Infrastruktur wie Brücken – einzusetzen.

Technische Zusammenfassung

1. Problemstellung

Die Instandhaltung alternder Brückennetzwerke erfordert proaktive, verifizierbare und interpretierbare Strategien. Traditionelle Reinforcement-Learning-(RL)-Ansätze, die ausschließlich auf Belohnungssignalen (Rewards) basieren, leiden unter zwei wesentlichen Mängeln im Kontext kritischer Infrastruktur:

1. Fehlende formale Sicherheitsgarantien: RL-Policies können unsicheres Verhalten zeigen (z. B. das Ignorieren von Sicherheitsgrenzen), da die Belohnungsfunktion komplexe Sicherheitsanforderungen oft nicht vollständig abbildet.
2. Mangelnde Interpretierbarkeit: Da moderne RL-Policies oft auf neuronalen Netzen basieren, sind sie „Black Boxes". Infrastrukturmanager können nicht nachvollziehen, warum eine bestimmte Wartungsentscheidung getroffen wurde, was die praktische Adoption behindert.

Zudem führt die Skalierung von Wartungsproblemen auf mehrere Brücken zu einem „Fluch der Dimensionalität" (Curse of Dimensionality). Die Zustands- und Aktionsräume wachsen exponentiell, was eine vollständige Analyse mittels klassischer probabilistischer Modellprüfung (Model Checking) auf dem gesamten Markov-Entscheidungsprozess (MDP) rechnerisch unmöglich macht.

2. Methodik

Das Paper stellt COOL-MC als Werkzeug vor, das RL mit probabilistischer Modellprüfung und Explainable AI (XAI) kombiniert, um diese Lücken zu schließen. Der Ansatz folgt einem vierstufigen Prozess:

A. Modellierung (MDP in PRISM)

Das Problem wird als MDP modelliert, das ein Netzwerk aus drei heterogenen Brücken beschreibt.

• Zustände: Jeder Brücke wird ein Zustand auf der 10-stufigen NBI-Skala (National Bridge Inventory, 0 = Versagt bis 9 = Exzellent) zugewiesen. Zusätzlich gibt es Zustandsvariablen für das verbleibende Budget, den Zyklus-Jahr (4-Jahres-Zyklus), das globale Jahr und einen Initialisierungs-Flag.
• Aktionen: Für jede Brücke stehen vier Aktionen zur Verfügung: Nichts tun (DN), Minor Maintenance (MN), Major Maintenance (MJ) und Ersatz (RP). Die gemeinsamen Aktionen bilden einen Vektor aus drei Einzelaktionen.
• Ressourcenbeschränkung: Ein geteiltes periodisches Budget ($B_{max} = 10$) wird alle vier Jahre neu aufgeladen. Aktionen sind nur zulässig, wenn die Summe der Kosten das verbleibende Budget nicht überschreitet.
• Übergänge: Die Verschlechterung der Brücken wird durch stochastische Übergangswahrscheinlichkeiten modelliert (basierend auf Literaturdaten, hier synthetisch).

B. RL-Training

Ein Deep-RL-Agent (Proximal Policy Optimization, PPO) wird trainiert, um eine Policy $\pi$ zu lernen, die die strukturelle Überlebensdauer maximiert und gleichzeitig die Wartungskosten minimiert. Die Policy wird als neuronales Netz (4 Schichten à 512 Neuronen) implementiert.

C. Induzierter DTMC und Verifikation

Anstatt den gesamten MDP zu prüfen, konstruiert COOL-MC einen induzierten diskreten Zeit-Markov-Kette (DTMC), $D_\pi$.

• Prinzip: Da die Policy $\pi$ deterministisch ist, wird jeder Nicht-Determinismus im MDP aufgelöst. Das System durchläuft nur die vom Agenten tatsächlich erreichbaren Zustände.
• Vorteil: Dies reduziert den Zustandsraum erheblich (im Vergleich zum vollen MDP) und macht die probabilistische Modellprüfung mit dem Tool Storm (unter Verwendung von PCTL-Eigenschaften) durchführbar.
• Verifikation: Es werden formale Eigenschaften geprüft, z. B. die Wahrscheinlichkeit, dass eine Brücke den Zustand „Versagt" (NBI 0) erreicht ($P=?(\diamond \text{"failed"})$).

D. Erklärbarkeit (Explainability)

Um die Entscheidungsfindung zu analysieren, werden vier Methoden auf dem induzierten DTMC angewendet:

1. Feature Lumping: Grobe Kategorisierung von Zustandsmerkmalen (z. B. NBI-Werte in Bins), um zu testen, ob präzise Werte für die Sicherheit kritisch sind.
2. Gradient-basierte Saliency: Berechnung der Sensitivität der Policy-Ausgabe gegenüber Eingabe-Features, um zu identifizieren, welche Brücken oder Merkmale die Entscheidungen am stärksten beeinflussen.
3. Action Labeling: Annotation von Zuständen mit den gewählten Aktionen, um Verhaltensmuster formal zu prüfen.
4. Counterfactual Action Replacement: Ersetzen von Aktionen (z. B. Minor durch Major Maintenance) in der Policy, um „Was-wäre-wenn"-Analysen durchzuführen, ohne die Policy neu zu trainieren.

3. Wichtige Ergebnisse

Sicherheitsverifikation

• Die trainierte Policy hat eine Versagenswahrscheinlichkeit von 3,55 % über einen 20-Jahres-Horizont. Dies liegt knapp über dem theoretischen Minimum von 0 %, zeigt aber, dass die Policy nicht perfekt ist.
• Die Wahrscheinlichkeit, dass das Budget erschöpft wird, ist extrem gering ($\approx 1,17 \times 10^{-6}$), was auf eine konservative Ausgabenstrategie hindeutet.
• Die Wahrscheinlichkeit, dass eine Brücke in einen kritischen Zustand (NBI $\le$ 2) gerät, liegt bei ca. 11,9 %.

Erklärbarkeit und Verhaltensanalyse

• Verzerrung (Bias): Die Saliency-Analyse zeigt eine systematische Verzerrung zugunsten von Brücke 1. Selbst wenn Brücke 2 oder 3 in einem schlechteren Zustand sind, priorisiert die Policy oft den Zustand von Brücke 1. Dies deutet auf eine Lücke in der Lernarchitektur hin (fehlende Permutationsinvarianz).
• Zeithorizont-Abhängigkeit (Horizon Gaming): Die Policy zeigt ein „Horizon-Gaming"-Verhalten. Wenn sie glaubt, dass das Ende des Planungshorizonts nahe ist (Jahre 16–19), reduziert sie die Wartungsbemühungen, da Ausfälle nach dem Ende des Episoden nicht mehr bestraft werden. Dies führt zu einer erhöhten Versagenswahrscheinlichkeit (auf 7,5 %), wenn dieser Effekt simuliert wird.
• Budget-Zyklus-Bewusstsein: Die Policy reagiert sensibel auf den Budget-Zyklus. Sie gibt am Anfang eines Zyklus (Jahr 0) konservativ aus und gibt im Zyklus-Mitte (Jahr 2) mehr aus. Interessanterweise nutzt sie das bevorstehende Budget-Reset am Ende des Zyklus (Jahr 3) nicht aus, um den Rest des Budgets zu verbrauchen, sondern bleibt konservativ.
• Feature-Lumping-Ergebnis: Eine grobe Kategorisierung der NBI-Werte für Brücke 1 (in drei Stufen) hatte keinen signifikanten Einfluss auf die Sicherheitsleistung. Dies deutet darauf hin, dass eine feine Auflösung der Inspektionsdaten für diese spezifische Policy nicht zwingend erforderlich ist.

4. Hauptbeiträge

1. Erweiterung von COOL-MC: Erste Anwendung des Tools auf ein Multi-Brücken-Netzwerk mit geteiltem Budget, über das bisher nur Ein-Brücken-Szenarien untersucht wurden.
2. Formale Verifikation von RL-Policies: Demonstration, wie probabilistische Modellprüfung (via PRISM/Storm) genutzt werden kann, um exakte Sicherheitsgarantien für RL-basierte Wartungsstrategien zu liefern, anstatt sich auf empirische Rollouts zu verlassen.
3. Interpretierbarkeit und Fehlererkennung: Aufdeckung von suboptimalen Verhaltensmustern (Bias zu Brücke 1, Horizon-Gaming), die durch reine Trainingsmetriken (wie kumulierte Belohnung) unsichtbar bleiben.
4. Skalierbarkeit: Beweis, dass die Konstruktion des induzierten DTMC den Zustandsraum drastisch reduziert und somit formale Verifikation auch für komplexere Netzwerke praktikabel macht.

5. Bedeutung und Ausblick

Das Paper zeigt, dass COOL-MC ein entscheidendes Werkzeug für den Einsatz von KI in der kritischen Infrastruktur ist. Es ermöglicht Infrastrukturmanagern nicht nur zu wissen, dass eine Policy sicher ist, sondern auch warum sie bestimmte Entscheidungen trifft und wo ihre Schwachstellen liegen.

Die Ergebnisse unterstreichen die Notwendigkeit, RL-Policies nicht nur zu trainieren, sondern sie auch formal zu verifizieren und zu erklären, bevor sie in der Praxis eingesetzt werden. Die identifizierten Mängel (wie der Bias zu einer spezifischen Brücke oder das Horizon-Gaming) bieten konkrete Ansatzpunkte für die Verbesserung der Modelle, z. B. durch permutation-invariante Architekturen oder angepasste Belohnungsfunktionen.

Einschränkung: Die Studie basiert auf synthetischen Übergangswahrscheinlichkeiten und Verschlechterungsraten. Für den realen Einsatz müssten die Modelle mit echten Inspektionsdaten und Domänenwissen von Brückenbauingenieuren kalibriert werden. Dennoch demonstriert die Arbeit die Machbarkeit und den Mehrwert des kombinierten Ansatzes aus RL, Verifikation und Erklärbarkeit.