Forward and Backward Reachability Analysis of Closed-loop Recurrent Neural Networks via Hybrid Zonotopes

Diese Arbeit stellt einen hybriden Zonopen-basierten Ansatz vor, der exakte Vorwärts- und Rückwärts-Erreichbarkeitsmengen für geschlossene RNN-Systeme mit ReLU-Aktivierungsfunktionen berechnet und durch eine skalierbare Relaxierungsmethode einen kontrollierbaren Kompromiss zwischen Rechenaufwand und Approximationsgenauigkeit ermöglicht.

Das Wesentliche

🧠 Die Reise durch den Labyrinth der Gedanken: Wie man KI-Sicherheit garantiert

Stellen Sie sich vor, Sie haben einen sehr klugen, aber etwas chaotischen Roboter (eine rekurrente neuronale Netz, kurz RNN). Dieser Roboter ist besonders gut darin, Dinge zu lernen, die mit der Zeit zu tun haben – wie das Wetter, Sprache oder das Fahren eines Autos. Er hat ein „Gedächtnis": Was er heute tut, hängt davon ab, was er gestern getan hat.

Das Problem? Wenn wir diesen Roboter in einem geschlossenen Kreislauf einsetzen (z. B. als Autopilot, der selbstständig lenkt und bremst), wissen wir oft nicht genau, wohin er in 10 oder 20 Schritten steuern wird. Könnte er plötzlich gegen eine Wand fahren? Ist er sicher?

Die Autoren dieser Arbeit (Yuhao Zhang und Xiangru Xu) haben einen neuen, cleveren Weg gefunden, um genau das herauszufinden. Sie nennen ihre Methode „Hybrid-Zono-Topie". Klingt kompliziert? Lassen Sie es uns mit einfachen Bildern erklären.

1. Das Problem: Das „Entrollen" ist zu schwer

Früher haben Forscher versucht, die Zukunft des Roboters vorherzusagen, indem sie seine Gedanken wie eine lange Kette von Perlen entrollten.

• Die alte Methode: Man nimmt einen Schritt, dann den nächsten, dann den übernächsten... und baut daraus ein riesiges, statisches Netz.
• Das Problem: Je weiter in die Zukunft man schaut, desto riesiger und unhandlicher wird dieses Netz. Es ist wie ein Gummiband, das sich immer weiter dehnt, bis es reißt oder zu schwer zu tragen ist. Zudem konnte man damit nur nach vorne schauen (Was passiert in der Zukunft?), aber nicht zurück (Welche Startbedingungen führen zu einem Unfall?).

2. Die Lösung: Die „Paar-Tanz"-Methode

Die Autoren haben eine geniale Idee: Statt die Zeitkette zu entrollen, betrachten sie Paare.
Stellen Sie sich vor, Sie halten die Hand Ihres Roboters.

• Linke Hand: Der Startzustand (Wo fängt er an?).
• Rechte Hand: Der Zustand in der Zukunft (Wo ist er nach 5 Schritten?).

Anstatt jede einzelne Sekunde dazwischen zu berechnen, verbinden sie diese beiden Hände direkt mit einem unsichtbaren Seil (dem mathematischen Modell des Roboters). Sie nennen dies eine „Zustands-Paar-Menge".

• Der Vorteil: Sie müssen den Weg nicht Schritt für Schritt ablaufen. Sie wissen sofort: „Wenn er hier startet, kann er dort landen."
• Die Form: Um diese Paare mathematisch zu beschreiben, nutzen sie eine spezielle Form, die sie Hybrid-Zonotope nennen. Stellen Sie sich das wie einen geometrischen Kasten vor, der nicht nur glatte Seiten hat, sondern auch „Knöpfe" (binäre Variablen), die entscheiden, ob bestimmte Teile des Roboters aktiv sind oder nicht (wie ein Lichtschalter, der an oder aus sein kann).

3. Der Trick: Der „Dreiecks-Filter" für die Komplexität

Hier kommt das größte Hindernis: Wenn der Roboter viele „Knöpfe" hat (ReLU-Aktivierungen), wird der mathematische Kasten so riesig, dass kein Computer ihn mehr berechnen kann.

Die Autoren haben einen cleveren Filter erfunden, den sie „Dreiecks-Relaxierung" nennen:

• Das Bild: Stellen Sie sich vor, Sie zeichnen den genauen Weg eines Roboters, der sich wie ein Zickzack bewegt. Das ist schwer zu berechnen.
• Der Trick: Wenn der Weg nicht zu wichtig ist, zeichnen Sie einfach ein großes, einfaches Dreieck um den Zickzack herum. Das Dreieck ist größer (es ist eine Schätzung), aber viel einfacher zu berechnen.
• Die Intelligenz: Sie prüfen alle „Knöpfe" des Roboters. Welche sind am kritischsten? (Welche haben das größte „Dreieck" als Lücke?).
  • Die wichtigsten Knöpfe behalten sie exakt (kein Dreieck, keine Lücke).
  • Die unwichtigen Knöpfe dürfen in ein großes Dreieck gepackt werden.

Sie können einen Regler (einen Schieberegler) bewegen:

• Regler auf „Exakt": Alles wird genau berechnet, aber es dauert lange (wie ein Hochpräzisions-3D-Druck).
• Regler auf „Schnell": Viele Teile werden durch Dreiecke ersetzt. Es ist schneller, aber etwas ungenauer (wie eine grobe Skizze).
• Das Geniale: Sie können genau steuern, wie viel Genauigkeit Sie gegen wie viel Rechenzeit tauschen wollen.

4. Vorwärts und Rückwärts: Die Zeitmaschine

Mit dieser Methode können sie nun zwei Dinge tun:

1. Vorwärts (Zukunftsvorhersage): „Wenn wir hier starten, wo könnten wir landen?" (Das ist der Forward Reachable Set).
2. Rückwärts (Ursachenforschung): „Welche Startpunkte führen zu einem Unfall?" (Das ist der Backward Reachable Set).

Das ist wie eine Zeitmaschine. Wenn Sie wissen wollen, wie man einen Unfall vermeiden kann, schauen Sie nicht nur nach vorne, sondern schauen zurück: „Welche Startbedingungen hätten zu diesem Crash geführt?" Damit können Sie die Startzone des Roboters so einschränken, dass er sicher bleibt.

5. Das Ergebnis: Sicherheit im Test

In ihren Tests haben sie gezeigt, dass ihre Methode funktioniert:

• Sie können die exakte Zukunft berechnen (wenn sie genug Rechenzeit haben).
• Sie können die geschätzte Zukunft berechnen (wenn es schnell gehen muss).
• Sie können sicherstellen, dass der Roboter nie in einen „verbotenen Bereich" (z. B. eine Wand) fährt. Wenn die Berechnung zeigt, dass ein Startpunkt zu einem Unfall führt, können sie diesen Startpunkt einfach verbieten.

Zusammenfassung in einem Satz

Die Autoren haben eine neue Art von mathematischem Sicherheitsnetz entwickelt, das es erlaubt, die Zukunft von lernenden Robotern vorherzusagen und zu überprüfen, ohne dabei in einem endlosen Rechenlabyrinth stecken zu bleiben – und das mit einem Schieberegler, mit dem man Genauigkeit und Geschwindigkeit nach Belieben mischen kann.

Warum ist das wichtig?
Damit können wir KI-Systemen in Autos, Flugzeugen oder Robotern vertrauen, weil wir mathematisch beweisen können, dass sie sicher sind, bevor wir sie auf die Straße lassen.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „Forward and Backward Reachability Analysis of Closed-loop Recurrent Neural Networks via Hybrid Zonotopes" auf Deutsch:

Problemstellung

Recurrent Neural Networks (RNNs) werden zunehmend zur Modellierung komplexer dynamischer Systeme und in sicherheitskritischen Regelkreisen eingesetzt, da sie zeitliche Abhängigkeiten durch ihren versteckten Zustand (Hidden State) effektiv erfassen können. Trotz ihrer Beliebtheit leiden RNNs jedoch unter Problemen wie der „explodierenden Gradienten"-Problematik und einer hohen Sensitivität gegenüber Eingangsstörungen.

Die zentrale Herausforderung liegt in der Verifikation und Sicherheitsanalyse von geschlossenen Regelkreisen (Closed-Loop Systems), die durch RNNs gesteuert werden. Bisherige Ansätze zur Erreichbarkeitsanalyse (Reachability Analysis) von RNNs weisen erhebliche Nachteile auf:

1. Unrolling-basierte Methoden: Diese entrollen die RNNs über die Zeit zu großen Feedforward-Netzen (FNNs). Dies führt zu einer schlechten Skalierbarkeit, da die Netzgröße mit der Anzahl der Zeitschritte exponentiell wächst.
2. Invarianten-Inferenz: Diese Methoden sind skalierbarer, führen jedoch oft zu inkonklusiven Ergebnissen aufgrund von akkumulierten Überapproximationsfehlern.
3. Fehlende Rückwärtsanalyse: Die Analyse der rückwärts erreichbaren Mengen (Backward Reachability), die für die Identifizierung adversarialer Eingangssequenzen und die Synthese sicherer Steuerungen entscheidend ist, wurde für geschlossene RNN-Systeme bisher kaum untersucht.

Das Ziel der Arbeit ist es, eine Methode zu entwickeln, die sowohl exakte als auch überapproximierte Vorwärts- und Rückwärts-Erreichbarkeitsmengen für geschlossene RNN-Systeme (mit ReLU-Aktivierungsfunktionen) effizient berechnet, ohne das Netz unrollen zu müssen.

Methodik

Die Autoren schlagen einen Ansatz vor, der auf Hybrid-Zonotopen (Hybrid Zonotopes, HZ) basiert. Hybrid-Zonotopen sind Mengen, die durch lineare Kombinationen von kontinuierlichen Generatoren (Zonotopen) und binären Generatoren (für nicht-konvexe Teile) dargestellt werden können, wobei lineare Gleichheitsbeschränkungen erlaubt sind.

Die Kernkomponenten der Methodik sind:

1. Zustands-Paar-Mengen (State-Pair Sets):
   Anstatt den Zustand zu jedem Zeitpunkt separat zu betrachten, definieren die Autoren eine Zustands-Paar-Menge $S_x(X, t)$, die die Beziehung zwischen dem Anfangszustand $x_1$ und dem Zustand zum Zeitpunkt $t$ ($x_t$) explizit kodiert. Dies ermöglicht die Darstellung der dynamischen Abhängigkeiten über Zeit und Schichten hinweg, ohne das Netz unrollen zu müssen.

2. Exakte Berechnung via Hybrid-Zonotopen:

   • Die Aktivierungsfunktion ReLU wird exakt als Hybrid-Zonotop dargestellt (basierend auf dem Graphen der Funktion).
   • Durch eine spezielle Operation namens „Constrained Product" (beschränktes Produkt) werden die Mengen der verborgenen Zustände zwischen aufeinanderfolgenden Zeitschritten und Schichten verknüpft. Dies erhält die Korrelationen zwischen den Zuständen und ermöglicht die exakte Berechnung der Erreichbarkeitsmengen als HZ.
   • Vorwärts-Erreichbarkeit (FRS): Berechnung der Menge aller möglichen Zustände $x_t$, ausgehend von einer Anfangsmenge $X_1$.
   • Rückwärts-Erreichbarkeit (BRS): Berechnung der Menge aller Anfangszustände $x_1$, die zu einem Zielzustand in einer Zielmenge $T$ führen.

3. Skalierbarkeit durch einstellbare Relaxierung (Tunable Relaxation Scheme):
   Da die exakte Darstellung mit der Anzahl der instabilen ReLU-Einheiten (wo der Eingabebereich $[\alpha, \beta]$ das Intervall $0$ überquert) wächst, schlagen die Autoren eine Relaxierung vor:

   • Triangle-Area-Score: Für jede instabile ReLU-Einheit wird ein Score berechnet, der der Fläche des Dreiecks entspricht, das durch die konvexe Relaxierung (Triangle Relaxation) entsteht.
   • Selektive Relaxierung: Instabile ReLUs werden nach diesem Score sortiert. Nur eine begrenzte Anzahl $N_b$ (binäres Limit) der ReLUs mit den höchsten Scores (d.h. denjenigen, die die größte Approximationslücke haben) werden exakt berechnet. Die restlichen ReLUs werden durch ihre konvexe Dreiecks-Relaxierung approximiert.
   • Dies ermöglicht einen expliziten Trade-off zwischen Rechenaufwand und Approximationsgenauigkeit. Wenn $N_b$ groß genug ist, ist das Ergebnis exakt.

4. Sicherheitsverifikation:
   Basierend auf den berechneten Mengen wird eine hinreichende Bedingung für die Sicherheit abgeleitet. Ein System ist sicher, wenn die Vorwärts-Erreichbarkeitsmenge keine unsichere Menge $O$ schneidet oder wenn die Rückwärts-Erreichbarkeitsmenge der unsicheren Menge den Anfangszustand nicht erreicht.

Hauptbeiträge

1. Exakte Erreichbarkeitsanalyse ohne Unrolling: Der erste Ansatz, der exakte Vorwärts- und Rückwärts-Erreichbarkeitsmengen für geschlossene RNN-Systeme mit ReLU-Aktivierungen unter Verwendung von Hybrid-Zonotopen berechnet, ohne das Netz über die Zeit zu entrollen.
2. Skalierbare Relaxierungsstrategie: Entwicklung eines einstellbaren Relaxierungsschemas, das instabile ReLU-Einheiten über alle Schichten hinweg basierend auf einer „Triangle-Area"-Metrik priorisiert. Dies erlaubt eine gezielte Kontrolle der Komplexität bei minimalem Verlust an Genauigkeit.
3. Sicherheitszertifizierung: Herleitung einer hinreichenden Bedingung für die Sicherheitsverifikation geschlossener RNN-Systeme und die Identifizierung unsicherer Trajektorien mittels der berechneten Mengen.

Ergebnisse

Die Autoren validierten ihre Methode an numerischen Beispielen:

• Mass-Spring-Damper-System: Ein physikalisches System mit zwei Wagen wurde modelliert. Ein RNN approximiert die Dynamik, ein weiteres RNN den MPC-Regler.
• Vergleich Exakt vs. Approximiert: Die Simulationen zeigten, dass die exakt berechneten Mengen vollständig innerhalb der überapproximierten Mengen liegen.
• Einfluss von $N_b$: Es wurde demonstriert, dass die Größe der überapproximierten Mengen monoton mit dem Parameter $N_b$ (Anzahl der exakt behandelten ReLUs) abnimmt. Bei $N_b = 0$ (alle relaxiert) ist die Menge am größten, bei $N_b \ge N_t$ (alle instabilen ReLUs exakt) ist sie exakt.
• Rückwärtsanalyse: Es wurde erfolgreich eine Menge von Anfangszuständen identifiziert, die innerhalb von 5 Schritten in einen definierten unsicheren Bereich führen, und daraus eine Sequenz unsicherer Zustände konstruiert.

Bedeutung und Ausblick

Diese Arbeit ist ein signifikanter Fortschritt im Bereich der formalen Verifikation von neuronalen Netzen in der Regelungstechnik.

• Schließung der Lücke: Sie adressiert das bisher vernachlässigte Problem der Rückwärts-Erreichbarkeitsanalyse für geschlossene RNN-Systeme.
• Praktische Anwendbarkeit: Durch das einstellbare Relaxierungsschema wird die Methode für reale Anwendungen skalierbar, wo exakte Berechnungen oft zu rechenintensiv sind.
• Sicherheit: Die Möglichkeit, unsichere Eingangssequenzen explizit zu identifizieren, ist entscheidend für das Design robuster und sicherer KI-gesteuerter Systeme.

Die Autoren weisen darauf hin, dass der Ansatz auf nichtlineare Pflanzenmodelle und andere Netzwerkarchitekturen (wie FNNs und CNNs) erweiterbar ist und die Verbesserung der Recheneffizienz ein zukünftiges Forschungsziel darstellt.