💻 computer science

Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning

Das Papier stellt RNN-ProVe vor, ein probabilistisches Framework, das die Wahrscheinlichkeit unerwünschter Verhaltensweisen in auf rekurrenten neuronalen Netzen basierenden Richtlinien für Reinforcement Learning mit einem bzw. mehreren Agenten abschätzt, indem es policy-gesteuertes Sampling nutzt, um die Einschränkungen bestehender Verifikationswerkzeuge in teilweise beobachtbaren Umgebungen zu überwinden.

Ursprüngliche Autoren: Luca Marzari, Enrico Marchesini

Veröffentlicht 2026-05-15

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Luca Marzari, Enrico Marchesini

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie trainieren einen Roboter, der ein Labyrinth navigieren soll. Dieser Roboter verfügt über ein spezielles „Gedächtnis" (ein rekurrentes neuronales Netzwerk, kurz RNN), das ihm hilft, sich daran zu erinnern, wo er gewesen ist, damit er nicht nur auf das reagiert, was er gerade jetzt sieht, sondern Entscheidungen auf Grundlage seiner gesamten bisherigen Reise trifft.

Das Problem lautet: Wie können wir wissen, dass dieser Roboter nicht versehentlich gegen eine Wand fährt?

Der alte Weg: Die „Worst-Case"-Vermutung

Traditionelle Sicherheitsprüfer versuchen, die Sicherheit des Roboters zu beweisen, indem sie alles Mögliche betrachten, was jemals passieren könnte. Sie stellen sich jedes mögliche Gedächtnis vor, das der Roboter haben könnte, sogar diejenigen, die im echten Leben unmöglich sind (wie etwa, dass sich der Roboter an eine Wand erinnert, die gar nicht existiert).

Da sie jede einzelne Möglichkeit prüfen müssen, einschließlich der unmöglichen, geraten sie oft ins Stocken. Es ist, als würde man versuchen, eine spezifische Nadel im Heuhaufen zu finden, indem man jedes einzelne Strohhalmbündel überprüft, sogar die, die von Anfang an nicht einmal in der Scheune waren. Dies macht den Prozess unglaublich langsam, und oft geben sie einfach auf und sagen: „Wir können nicht sicher sein", oder sie gehen davon aus, dass der Roboter unsicher ist, nur um auf der sicheren Seite zu sein, was nicht sehr hilfreich ist.

Der neue Weg: RNN-ProVe (Der „Realitäts"-Detektiv)

Die Autoren dieses Papers, Luca Marzari und Enrico Marchesini, haben ein neues Werkzeug namens RNN-ProVe entwickelt. Anstatt jede unmögliche Fantasie zu prüfen, stellen sie eine intelligentere Frage: „Welche tatsächlichen Erinnerungen hat dieser Roboter während seines Lernprozesses aufgebaut?"

So funktioniert es, anhand einer einfachen Analogie:

1. Der „Feasibility Oracle" (Der Gedächtnis-Filter)

Stellen Sie sich vor, der Roboter hat Tausende von Trainingsläufen durchlaufen. Während dieser Zeit hat er einen spezifischen Satz „realer" Erinnerungen aufgebaut.

Alte Tools betrachten die gesamte Bibliothek aller möglichen Erinnerungen (einschließlich gefälschter).
RNN-ProVe trainiert einen speziellen „Gedächtnis-Filter" (einen Klassifikator). Dieser Filter lernt, zwischen einer realen Erinnerung (einer, die der Roboter tatsächlich erlebt hat) und einer gefälschten Erinnerung (einer, die niemals passieren könnte) zu unterscheiden.

Stellen Sie sich dies wie einen Türsteher in einem Club vor. Der Türsteher (der Filter) prüft Ihren Ausweis. Wenn Ihr Ausweis besagt, dass Sie tatsächlich auf der Party waren (eine machbare Vergangenheit), lassen Sie ihn herein. Wenn Ihr Ausweis gefälscht ist (eine unmögliche Vergangenheit), wird Sie abgewiesen. RNN-ProVe prüft nur die Sicherheit der Personen, die tatsächlich am Türsteher vorbeigekommen sind.

2. Der „Wahrscheinlichkeits"-Check (Das Risikomessgerät)

Sobald der Filter die realen Erinnerungen von den gefälschten getrennt hat, versucht RNN-ProVe nicht, jede einzelne reale Erinnerung zu prüfen (was immer noch zu schwierig wäre). Stattdessen nimmt es eine zufällige Stichprobe der realen Erinnerungen.

Es fragt: „Von 1.000 realen Erinnerungen, die wir ausgewählt haben, wie viele haben zu einem Crash geführt?"

Wenn 10 von 1.000 zu einem Crash geführt haben, sagt es nicht: „Der Roboter ist unsicher."
Es sagt: „Es besteht eine 1-prozentige Wahrscheinlichkeit, dass der Roboter in dieser spezifischen Situation einen Crash erleidet, und wir sind zu 99 Prozent sicher, dass diese Zahl korrekt ist."

Das ist wie ein Wettervorhersager. Anstatt zu sagen „Es wird definitiv regnen" oder „Es wird definitiv nicht regnen", sagt er: „Es besteht eine 30-prozentige Wahrscheinlichkeit für Regen, basierend auf den Daten, die wir haben." Dies liefert eine viel nützlichere, quantitative Antwort.

Warum das wichtig ist

Das Paper hat dies an zwei Arten von Spielen getestet:

Einzelner Agent: Ein Roboter, der ein Raster navigiert.
Multi-Agent: Zwei Roboter, die zusammenarbeiten, um eine Kiste zu schieben.

Die Ergebnisse:

Geschwindigkeit: Die alten Tools brauchten Minuten oder Stunden, um kleine Raster zu prüfen, und gaben bei größeren auf. RNN-ProVe führte dieselben Prüfungen in Millisekunden durch.
Genauigkeit: Die alten Tools fanden oft „gefälschte" Probleme (Fehlalarme), weil sie unmögliche Erinnerungen prüften. RNN-ProVe ignorierte die unmöglichen und fand die echten Risiken.
Teamarbeit: Die alten Tools konnten mit Roboterteams, die zusammenarbeiten, nicht umgehen. RNN-ProVe bewältigte das Multi-Agent-Team perfekt und prüfte, ob jedes Teammitglied einen Fehler machen könnte.

Das Fazit

RNN-ProVe ist eine neue Methode zur Verifikation der KI-Sicherheit, die aufhört, jede unmögliche Szene zu prüfen. Stattdessen konzentriert sie sich auf das, was tatsächlich während des Trainings passiert. Indem sie die Unmöglichen herausfiltert und die Realen stichprobenartig prüft, liefert sie uns eine schnelle, zuverlässige und mathematische „Risikoprozentsatz"-Angabe dafür, wie oft ein intelligenter Roboter einen Fehler machen könnte.

Sie verwandelt ein beängstigendes, unlösbares mathematisches Problem in eine handhabbare, statistische Schätzung, die uns genau sagt, wie sicher unsere historienabhängige KI wirklich ist.

Technische Zusammenfassung: RNN-Probabilistische Verifikation (RNN-ProVe)

Problemstellung

Recurrente Neuronale Netze (RNNs) werden im Reinforcement Learning (RL) häufig eingesetzt, um partielle Beobachtbarkeit und Multi-Agenten-Koordination zu bewältigen, indem sie latente verborgene Zustände unterhalten, die die Interaktionsgeschichte kodieren. Die Verifikation dieser Strategien ist grundlegend herausfordernd, da der Entscheidungsprozess von der gesamten Historie der Beobachtungen und Aktionen abhängt und nicht nur von der aktuellen Eingabe.

Bestehende Verifikationswerkzeuge für RNNs konzentrieren sich primär auf die Robustheitsanalyse gegenüber begrenzten Eingabestörungen über einen festen Horizont. Diese Methoden stützen sich typischerweise auf grobe geometrische Überapproximationen (z. B. Intervalle oder Hyperrechtecke) des verborgenen Zustandsraums. Im Kontext von RL führt dieser Ansatz zu spurious hidden states (fiktiven verborgenen Zuständen) – Kombinationen von Neuronenwerten, die innerhalb der Netzwerkgrenzen mathematisch möglich sind, aber angesichts der spezifischen Strategie und der Umgebungs dynamik nicht realisierbar sind. Folglich liefern diese Werkzeuge oft übermäßig konservative Ergebnisse oder falsch-positive Befunde.

Darüber hinaus erfordert die exakte Verifikation von RNN-basierten Strategien die Enumeration aller erreichbaren Konfigurationen verborgener Zustände, um unerwünschtes Verhalten zu prüfen. Dieses Problem ist äquivalent zur Berechnung von Vorwärtsbildmaßen neuronaler Netze und ist aufgrund der Nichtlinearität und Nichtkonvexität neuronaler Netze #P-schwer. Eine exakte Charakterisierung ist für nicht-triviale Strategien rechnerisch nicht durchführbar, und bestehende Methoden skalieren nicht auf Multi-Agenten-Szenarien oder hochdimensionale Räume.

Methodik: RNN-ProVe

Die Autoren schlagen RNN Probabilistic Verification (RNN-ProVe) vor, ein Framework, das von der exakten Worst-Case-Verifikation zur probabilistischen Verifikation über realisierbare Historien übergeht. Anstatt alle möglichen verborgenen Zustände zu enumerieren, schätzt RNN-ProVe die Wahrscheinlichkeit unerwünschten Verhaltens, indem es das Volumen des realisierbaren verborgenen Zustandsraums quantifiziert, das zu Verstößen führt.

Das Framework arbeitet in drei Hauptphasen:

Lernen eines Realisierbarkeits-Orakels:
- Während der RL-Trainingsphase erkundet der Agent die Umgebung und generiert einen Datensatz von Zustands-verborgener-Zustand-Paaren $(s, h)$ .
- RNN-ProVe trainiert einen Realisierbarkeits-Klassifikator $C: S \times H \to \{0, 1\}$ auf diesem Datensatz. Dieser Klassifikator lernt, zwischen verborgenen Zuständen zu unterscheiden, die unter der trainierten Strategie tatsächlich erreichbar sind (realisierbar), und solchen, die es nicht sind (nicht realisierbar).
- Dieser Schritt nutzt den Satz der universellen Approximation, um die komplexe, niedrigdimensionale Mannigfaltigkeit realisierbarer Historien innerhalb des hochdimensionalen verborgenen Zustandsraums zu approximieren.
Strategie-gesteuerte Stichprobenziehung und Verifikation:
- Für einen bestimmten Zustand von Interesse werden Kandidaten-Historienvektoren aus dem verborgenen Zustandsbereich gesampelt.
- Der trainierte Klassifikator $C$ fungiert als Orakel, filtert nicht realisierbare Stichproben heraus und behält nur jene verborgenen Zustände $h^*$ bei, die gültigen Interaktionshistorien entsprechen, die zum aktuellen Zustand führen.
- Die Strategie wird dann auf diesen validierten Historien evaluiert, um festzustellen, ob sie zu einem Verstoß führen (z. B. die Auswahl einer unsicheren Aktion).
Statistische Schätzung mit Fehlerschranken:
- Das Framework berechnet das Verhältnis der verstoßenden validierten Historien zur Gesamtzahl der validierten Historien, um das Verstoßvolumen zu schätzen.
- Entscheidend leitet RNN-ProVe statistische Konfidenzschranken unter Verwendung der Hoeffding-Ungleichung ab. Es zerlegt die gesamte Fehlerschranke $\epsilon$ $ϵ$ und den Konfidenzparameter $\delta$ $δ$ in zwei Komponenten:
  - Klassifikatorfehler: Die Genauigkeit des Realisierbarkeits-Orakels.
  - Stichprobenvarianz: Der statistische Fehler aus der Monte-Carlo-Schätzung.
- Dies ermöglicht dem Framework, fehlerbegrenzte, hochkonfidente Zertifikate bezüglich der Wahrscheinlichkeit von Verhaltensverstößen zu produzieren.

Hauptbeiträge

Die Arbeit leistet folgende spezifische Beiträge:

Problemformulierung: Sie definiert formal das Problem der probabilistischen Verifikation für rekurrente RL-Strategien unter partieller Beobachtbarkeit und berücksichtigt explizit die Menge der realisierbaren verborgenen Zustände, die durch eine trainierte Strategie induziert werden.
RNN-ProVe-Framework: Sie stellt ein neuartiges Framework vor, das Realisierbarkeitslernen mit Monte-Carlo-Schätzung kombiniert, um Verhaltensverstöße in RNN-basierten Strategien quantitativ zu bewerten.
Erweiterung auf Multi-Agenten: Sie erweitert das Verifikationsproblem auf vollständig kooperative Multi-Agenten-RL (MARL). Sie leitet fehlerbegrenzte, hochkonfidente Garantien für die Identifikation realisierbarer Historien und die Schätzung von Verstößen in dezentralen Umgebungen ab und bietet damit eine handhabbare Approximation für ein ansonsten #P-schweres Problem.
Theoretische Garantien: Sie liefert einen theoretischen Beweis (Satz 2), dass das geschätzte Verstoßvolumen spezifische Fehler- und Konfidenzschranken erfüllt, abhängig von den Stichprobengrößen der Klassifikatorvalidierung und der Verifikationsstichprobenziehung.

Experimentelle Ergebnisse

Die Autoren evaluierten RNN-ProVe an Einzelagenten-Navigationsaufgaben und kooperativen Multi-Agenten-"BoxPushing" (BP)-Aufgaben unter Verwendung von DRQN-Strategien.

Skalierbarkeit: RNN-ProVe zeigte erhebliche Skalierbarkeitsvorteile. Bei Navigationsaufgaben benötigten lineare Basismethoden Minuten bis Stunden für kleine Umgebungen (4x4, 8x8) und liefen bei größeren Umgebungen (16x16) aus. Im Gegensatz dazu lieferte RNN-ProVe quantitative Ergebnisse in Millisekunden über alle getesteten Gittergrößen hinweg.
Genauigkeit im Vergleich zu Baselines:
- Im Vergleich zu naiver Monte-Carlo-Schätzung (uniforme Stichprobenziehung ohne Realisierbarkeitsfilterung) lieferte RNN-ProVe genaue Schätzungen. Die naive Stichprobenziehung ergab signifikant aufgeblähte Verstoßraten (z. B. ~23 % vs. ~1,6 % bei 4x4), da sie nicht realisierbare verborgene Zustände testete, die in der Praxis nicht auftreten.
- Im Vergleich zu exakten Linearisierungsbaselines (wo möglich) produzierte RNN-ProVe vergleichbare Verstoßschätzungen (z. B. ~1,42 % vs. ~1,44 % bei 4x4), jedoch mit probabilistischen Garantien und einer um Größenordnungen geringeren Rechenzeit.
Multi-Agenten-Leistung: Das Framework verifizierte erfolgreich kooperative Strategien im BP-Bereich (10x10 und 20x20 Gitter) und identifizierte mittlere Verstoßraten von etwa 1,18 % bzw. 1,7 %. Bestehende Werkzeuge konnten nicht direkt auf diese kooperativen Szenarien angewendet werden.
Erkenntnis: Die Experimente zeigten, dass selbst Strategien mit hohen durchschnittlichen Erträgen eine nicht-uniforme Generalisierung über realisierbare verborgene Zustände aufweisen, mit spezifischen Sensitivitäten in der Nähe von Hindernissen, die von standardmäßigen empirischen Evaluierungen übersehen werden.

Bedeutung und Behauptungen

Die Arbeit argumentiert, dass die exakte Worst-Case-Verifikation für rekurrente RL-Strategien nicht nur rechnerisch prohibitiv, sondern auch nicht mit der Struktur historienabhängiger Entscheidungsfindung vereinbar ist. Die Autoren behaupten, dass die probabilistische Verifikation über realisierbare Historien nicht lediglich eine heuristische Relaxierung ist, sondern eine prinzipielle Antwort auf fundamentale rechnerische Barrieren.

Indem RNN-ProVe sich auf die Menge der unter einer Strategie tatsächlich erreichbaren verborgenen Zustände konzentriert, liefert es quantitative, realisierbarkeitsbewusste probabilistische Garantien. Dieser Ansatz erzeugt informativere Zertifikate als binäre "sicher/unsicher"-Ergebnisse oder übermäßig konservative Robustheitsprüfungen und ermöglicht ein besseres Verständnis der Zuverlässigkeit und Generalisierung von Strategien in komplexen, partiell beobachtbaren und Multi-Agenten-Umgebungen. Die Arbeit plädiert für diese probabilistische Perspektive als grundlegenden Ansatz für die Sicherheitsbetrachtung in historienabhängigen Systemen.