The FABRIC Strategy for Verifying Neural Feedback Systems

Die Arbeit stellt die FABRIC-Strategie vor, die durch die Integration neuer Algorithmen für die Rückwärtsreichbarkeitsanalyse mit bestehenden Vorwärtsanalysen die Verifikation von nichtlinearen neuronalen Feedback-Systemen signifikant verbessert.

Das Wesentliche

🧵 FABRIC: Das Sicherheitsnetz für Roboter-Köpfe

Stellen Sie sich vor, Sie bauen einen autonomen Roboter, der ein Flugzeug steuert oder ein selbstfahrendes Auto lenkt. Der „Gehirn" dieses Roboters ist ein künstliches neuronales Netzwerk (eine Art KI). Das Problem: Diese KIs sind wie schwarze Kisten. Wir wissen oft nicht genau, wie sie in jeder denkbaren Situation reagieren werden.

Die Forscher wollen sicherstellen, dass diese Roboter niemals in einen Unfall geraten (z. B. gegen eine Wand fahren oder aus dem Ziel fliegen), egal was passiert. Dafür haben sie eine neue Strategie namens FABRIC entwickelt.

Der Name FABRIC steht für Forward and Backward Reachability Integration for Certification. Klingt kompliziert? Lassen Sie uns das mit ein paar Analogien erklären.

---

1. Das Problem: Nur nach vorne schauen reicht nicht

Stellen Sie sich vor, Sie wollen wissen, ob ein Wanderer von Punkt A (Start) sicher zu Punkt B (Ziel) kommt, ohne in einen Abgrund zu fallen.

• Der alte Weg (Vorwärts-Analyse): Sie schicken den Wanderer los und schauen, wohin er läuft.
  • Das Problem: Wenn der Wanderer 100 verschiedene Wege hat, müssen Sie alle 100 Wege durchgehen. Bei komplexen KI-Systemen gibt es aber unendlich viele Möglichkeiten. Das ist wie der Versuch, jeden einzelnen Sandkorn auf einem Strand zu zählen, um zu sehen, ob einer davon ein Diamant ist. Es dauert ewig und ist oft ungenau.
• Der neue Weg (Rückwärts-Analyse): Sie stehen am Ziel (Punkt B) und fragen: „Von welchen Punkten aus kann ich garantiert hierher kommen?" oder „Von welchen Punkten aus könnte ich vielleicht hierher kommen?"
  • Das Problem: Das ist für Computer extrem schwer, weil man die KI „rückwärts" durchlaufen muss. Bisher war das so schwer, dass es kaum jemand gemacht hat.

2. Die Lösung: FABRIC – Der Zangen-Griff

Die Forscher sagen: „Warum nur eine Seite wählen? Machen wir beides!"

Stellen Sie sich vor, Sie wollen einen großen, unsicheren Raum (den „Wald") absichern.

• Vorwärts-Analyse: Sie gehen vom Start aus und markieren alles, was der Wanderer erreichen könnte. Das ist wie ein riesiges, unscharfes Netz, das sich vorwärts ausbreitet.
• Rückwärts-Analyse: Sie gehen vom Ziel aus und markieren alles, was sicher zum Ziel führt. Das ist wie ein zweites Netz, das sich rückwärts ausbreitet.

FABRIC ist die Strategie, diese beiden Netze in der Mitte zusammenzuführen.

• Wenn sich das „Vorwärts-Netz" und das „Rückwärts-Netz" überlappen, haben wir einen sicheren Korridor. Wir wissen dann zu 100 %, dass der Roboter das Ziel erreicht, ohne in Gefahr zu kommen.
• Das Geniale daran: Man muss nicht den ganzen Wald durchsuchen. Man sucht nur dort, wo sich die beiden Netze treffen. Das spart enorme Rechenzeit.

3. Die Werkzeuge: Wie man das „Rückwärts-Netz" baut

Das Schwierigste an FABRIC war, das Rückwärts-Netz für nicht-lineare Systeme (also Systeme, die sich nicht einfach wie eine gerade Linie verhalten) zu bauen. Die Forscher haben dafür drei neue Werkzeuge entwickelt:

1. DRIPy (Der Verfeinerer):
   • Analogie: Stellen Sie sich vor, Sie versuchen, einen riesigen, unscharfen Schatten zu zeichnen, der einen kleinen Gegenstand umgibt. Anfangs ist der Schatten riesig und ungenau. DRIPy ist wie ein Künstler, der den Schatten immer wieder neu zeichnet, aber jedes Mal den Bereich etwas einschränkt, bis er perfekt passt. Es „schneidet" den überflüssigen Raum weg, ohne die Sicherheit zu verlieren.
2. SHARP, CRISP und CLEAN (Die Sucher):
   • Diese Werkzeuge versuchen, das kleinste sichere Gebiet zu finden, das garantiert funktioniert.
   • SHARP ist wie ein Ballon, den man langsam aufpustet, bis er fast platzt, aber noch sicher ist.
   • CRISP ist wie ein Fotograf, der tausende Fotos macht, um zu sehen, wo die sicheren Stellen sind, und dann die beste Form daraus schneidet.
   • CLEAN ist wie ein Gärtner, der alle „schlechten" (unsicheren) Stellen aus einem Beet entfernt, bis nur noch das Beste übrig bleibt.

4. Das Ergebnis: Schnell und sicher

Die Forscher haben ihre Methode an verschiedenen Testfällen getestet (wie ein fahrender Wagen oder ein fliegendes Flugzeug).

• Das Ergebnis: FABRIC ist deutlich schneller als die alten Methoden. Bei manchen Tests war es bis zu 7-mal schneller.
• Warum? Weil es nicht blind durch den Wald läuft, sondern intelligent von beiden Seiten her anrückt. Es nutzt die Stärken der Vorwärts-Analyse (einfach zu berechnen) und der Rückwärts-Analyse (sehr präzise), um die Schwächen der jeweils anderen auszugleichen.

Zusammenfassung

FABRIC ist wie ein Sicherheits-Check für KI-gesteuerte Roboter. Anstatt nur zu hoffen, dass der Roboter nicht in den Abgrund fällt, oder stundenlang alle möglichen Wege durchzurechnen, nutzt FABRIC einen cleveren Trick: Es schaut gleichzeitig vom Start und vom Ziel aus. Wo sich die beiden Sichtfelder treffen, ist der Weg sicher.

Dank neuer mathematischer Tricks (die „Schere" und das „Schneidwerkzeug") funktioniert das jetzt auch für komplexe, nicht-lineare Systeme. Das bedeutet: Wir können autonome Autos und Drohnen viel schneller und sicherer verifizieren, bevor sie auf die Straße oder in den Himmel geschickt werden.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „The FABRIC Strategy for Verifying Neural Feedback Systems" auf Deutsch:

1. Problemstellung

Neuronale Feedback-Systeme (NFS), bei denen dynamische Systeme durch neuronale Netzwerke gesteuert werden, werden zunehmend in sicherheitskritischen Anwendungen wie Robotik und autonomen Systemen eingesetzt. Die formale Verifikation dieser Systeme, insbesondere die Sicherstellung von „Reach-Avoid"-Spezifikationen (Erreichen eines Zielzustands unter Vermeidung unsicherer Zustände), ist jedoch herausfordernd.

Bisherige Ansätze konzentrieren sich fast ausschließlich auf die Vorwärts-Reichbarkeitsanalyse (Forward Reachability), die den Satz aller möglichen zukünftigen Zustände berechnet. Die Rückwärts-Reichbarkeitsanalyse (Backward Reachability), die den Satz aller Zustände identifiziert, von denen aus ein Ziel erreicht werden kann, wurde bisher kaum untersucht. Der Hauptgrund dafür ist die begrenzte Skalierbarkeit bekannter Techniken, insbesondere bei nichtlinearen Systemdynamiken und der Notwendigkeit, Mengen durch neuronale Netzwerke rückwärts zu propagieren.

2. Methodik und Kernbeiträge

Die Autoren stellen FABRIC (Forward and Backward Reachability Integration for Certification) vor, eine Strategie, die Vorwärts- und Rückwärtsanalysen kombiniert, um die Skalierbarkeitsgrenzen zu überwinden. Die Arbeit umfasst folgende methodische Neuerungen:

A. Rückwärts-Reichbarkeitsanalyse (Backward Reachability)

Das Paper definiert zwei Arten von rückwärts erreichbaren Mengen für nichtlineare NFS:

1. Must-BRS (Backward Must-Reachable Set): Zustände, die unbedingt das Ziel erreichen (unter allen möglichen Störungen).
2. May-BRS (Backward May-Reachable Set): Zustände, die das Ziel potenziell erreichen können.

Um diese Mengen zu berechnen, werden neue Algorithmen entwickelt:

• Für Overapproximationen (Äußere Mengen/May-BRS):
  • Nutzung von polyedrischen Einschließungen (Polyhedral Enclosures) zur Approximation nichtlinearer Dynamiken.
  • Erweiterung des Domain Refinement-Verfahrens (DRIP) auf nichtlineare Systeme (Algorithmus DRiPy). Dieser Algorithmus iterativ verfeinert den Suchraum, indem er die zuvor berechnete overapproximierte Menge als neue Domäne verwendet, um die Konservativität der Schranken zu reduzieren.
• Für Underapproximationen (Innere Mengen/Must-BRS):
  • Entwicklung von drei Algorithmen zur Berechnung innerer Schranken, die einen Kompromiss zwischen Skalierbarkeit und Präzision finden:
    1. SHARP: Skalierung einer äußeren Menge nach innen basierend auf einer Optimierung der Volumenmaximierung unter der Bedingung, dass die Vorwärts-Reichbarkeit im Ziel enthalten ist.
    2. CRISP: Eine sampling-basierte Methode, die positive Stichproben (die das Ziel erreichen) nutzt, um die konvexe Hülle zu bestimmen und darin ein maximales Hyperrechteck zu finden. Dies reduziert die Anzahl der teuren Vorwärts-Abfragen.
    3. CLEAN: Eine Erweiterung von CRISP, die auch negative Stichproben (die das Ziel nicht erreichen) explizit ausschließt, um mit nicht-konvexen oder löchrigen Mengen umzugehen. Dies führt zu einem gemischt-ganzzahligen linearen Programm (MILP).

B. Die FABRIC-Strategie

FABRIC teilt den Planungshorizont $T$ in $F$ Vorwärts-Schritte und $B$ Rückwärts-Schritte auf ($T = F + B$).

• Für Reach-Eigenschaften: Wenn die overapproximierte Vorwärts-Menge zum Zeitpunkt $F$ in der underapproximierten Rückwärts-Menge (Must-BRS) enthalten ist, ist der Zielzustand garantiert erreichbar.
• Für Avoid-Eigenschaften: Wenn die Vorwärts-Mengen zu jedem Zeitpunkt $t \in [0, F]$ disjunkt von den unsicheren Zuständen sind und die Vorwärts-Menge zum Zeitpunkt $F$ disjunkt von der overapproximierten Rückwärts-Menge der unsicheren Zustände ist, ist das System sicher.

3. Ergebnisse

Die Autoren evaluieren ihre Algorithmen an Benchmarks aus dem ARCH-Wettbewerb (TORA, Unicycle-Modell, Attitude-Control-Modell) mit neuronalen Politik-Netzwerken unterschiedlicher Größe.

• Vergleich mit dem State-of-the-Art (SOTA):
  • Äußere Mengen (Overapproximation): Der Algorithmus DRiPy (mit Domain Refinement) übertrifft den SOTA-Tool HyBReach-MILP signifikant. Während HyBReach-MILP bei komplexeren Benchmarks (Unicycle, Attitude) oft Zeitüberschreitungen erleidet und große Mengen berechnet, liefert DRiPy in deutlich kürzerer Zeit (bis zu 47-fach schneller) viel präzisere (kleinere) Mengen (bis zu 2900-fach kleinere Volumina).
  • Innere Mengen (Underapproximation): Der SOTA-Tool BURNS scheitert bei den komplexeren Benchmarks oft daran, eine gültige innere Menge zu finden (Volumen = 0) oder benötigt extrem lange Rechenzeiten. Die neuen Methoden (SHARP, CRISP, CLEAN) liefern erfolgreich zertifizierte innere Mengen. CRISP erwies sich als der beste Allrounder.
• FABRIC vs. reine Vorwärtsanalyse:
  • Bei einfachen Benchmarks (TORA) ist die reine Vorwärtsanalyse effizienter, da der Overhead der Rückwärtsanalyse dominiert.
  • Bei komplexeren Benchmarks (Unicycle) führt FABRIC zu Speedups von bis zu 7-fach im Vergleich zur reinen Vorwärtsanalyse. Selbst bei Berücksichtigung der zusätzlichen Berechnungsschritte ist FABRIC bei schwierigen Problemen um den Faktor 2–3 schneller.
  • Beim Attitude-Benchmark sind die Ergebnisse gemischt, wobei FABRIC bei „Avoid"-Spezifikationen Vorteile zeigt, bei „Reach"-Spezifikationen jedoch manchmal langsamer ist.

4. Bedeutung und Ausblick

Die Arbeit schließt eine wichtige Lücke in der Verifikation neuronaler Feedback-Systeme, indem sie skalierbare Algorithmen für die Rückwärtsanalyse nichtlinearer Systeme bereitstellt.

• Theoretischer Beitrag: Die Erweiterung von Domain-Refinement-Techniken auf nichtlineare Dynamiken und die Entwicklung von sampling-basierten Methoden zur Berechnung innerer Schranken.
• Praktische Relevanz: Die FABRIC-Strategie bietet einen neuen, effizienteren Weg, um Sicherheitsgarantien für autonome Systeme zu geben, die neuronale Netze als Controller nutzen. Sie ermöglicht die Verifikation von Systemen, die mit reinen Vorwärtsmethoden nicht oder nur sehr ineffizient lösbar wären.

Zukünftige Arbeiten sollen sich auf die weitere Optimierung der inneren Mengen-Schätzung (zur Bewältigung des „Fluchs der Dimensionalität") und die Automatisierung der Aufteilung des Horizonts in Vorwärts- und Rückwärtsanteile ($F$ und $B$) konzentrieren.