🤖 AI

Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems

Dieser Artikel schlägt einen auf Mengen basierenden Trainingsansatz für neuronale Barrierenzertifikate vor, der formale Verifikation durch eine spezialisierte Verlustfunktion direkt in den Trainingsprozess integriert und dadurch die iterative Schleife aus Training und Verifikation zu einem einzigen Verfahren zusammenführt, das sich effektiv mit der Systemdimension skaliert und komplexe nichtlineare Dynamiken bewältigt.

Ursprüngliche Autoren: Miriam Kranzlmüller, Lukas Koller, Tobias Ladner, Matthias Althoff

Veröffentlicht 2026-05-06

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Miriam Kranzlmüller, Lukas Koller, Tobias Ladner, Matthias Althoff

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

Das große Ganze: Eine unsichtbare Sicherheitswand bauen

Stellen Sie sich vor, Sie entwerfen ein autonomes Fahrzeug oder einen Roboterarm. Sie müssen zu 100 % sicher sein, dass die Maschine niemals gegen eine Wand fährt oder einen Menschen verletzt. In der Welt des Ingenieurwesens nennt man dies Sicherheitsverifikation.

Um zu beweisen, dass eine Maschine sicher ist, verwenden Mathematiker etwas, das als Barrierenzertifikat bezeichnet wird. Stellen Sie sich dies als eine unsichtbare, magische Wand vor, die in der Luft um die Maschine herum gezeichnet wird.

Auf der einen Seite der Wand befindet sich die „Sicherheitszone" (wo die Maschine startet).
Auf der anderen Seite befindet sich die „Gefahrenzone" (wo die Maschine niemals hinkommen darf).
Die Wand ist so konstruiert, dass, wenn die Maschine sie berührt, sie zurück in Richtung Sicherheit gestoßen wird und niemals die Grenze überschreiten darf.

Wenn Sie mathematisch beweisen können, dass diese Wand existiert und perfekt funktioniert, ist die Maschine als sicher zertifiziert.

Der alte Weg: Das „Raten und Prüfen"-Spiel

Früher versuchten Wissenschaftler, diese unsichtbare Wand mit einem neuronalen Netzwerk (einer Art KI-Gehirn) zu bauen. Der Prozess glich einem frustrierenden Spiel von „Heiß und Kalt":

Raten: Das KI-Gehirn zeichnet eine Wand basierend auf einigen zufälligen Stichproben.
Prüfen: Ein separates, sehr langsames Computerprogramm (ein Verifizierer) überprüft, ob die Wand überall standhält.
Fehlschlag: Wenn der Verifizierer auch nur ein winziges Loch in der Wand findet, muss das KI-Gehirn zurückkehren, die Wand neu zeichnen und es erneut versuchen.
Wiederholen: Dieser Zyklus aus „Zeichnen -> Prüfen -> Fehlschlag -> Neuzeichnen" konnte Stunden oder Tage dauern, insbesondere bei komplexen Maschinen.

Der neue Weg: Die „selbstprüfende" Wand

Die Autoren dieses Papiers schlagen eine neue Methode vor, die Set-basiertes Training genannt wird. Anstatt die Wand nachdem sie gezeichnet wurde zu überprüfen, bauen sie den Prüfmechanismus in den Zeichnungsprozess selbst ein.

So funktioniert ihr neuer Ansatz:

1. Das „Set"-Konzept (Der neblige Kasten)
Anstatt die Wand an einzelnen Punkten zu überprüfen (wie etwa zu prüfen, ob ein bestimmtes Pixel sicher ist), überprüfen sie die Wand gegen ganze „neblige Kästen" (mathematisch als Zonotope bezeichnet). Stellen Sie sich vor, Sie wickeln den gesamten Pfad, den der Roboter möglicherweise nimmt, in einen unscharfen, 3D-Kasten ein. Das KI-Gehirn schaut nicht nur auf einen Punkt, sondern betrachtet den gesamten Kasten auf einmal.

2. Der „Loss"-Wert (Das Sicherheitsmessgerät)
Beim herkömmlichen KI-Training gibt der „Loss"-Wert an, wie falsch das KI-Gehirn liegt. Bei dieser neuen Methode ist der Loss-Wert ein Sicherheitsmessgerät.

Das KI-Gehirn wird darauf trainiert, diesen Wert zu minimieren.
Der Wert wird berechnet, indem mathematisch bewiesen wird, dass die „nebligen Kästen" der Gefahrenzone und die „nebligen Kästen" der Sicherheitszone niemals berühren.
Die Magie: Wenn das KI-Gehirn den Wert auf Null senkt, bedeutet dies nicht nur „es sieht gut aus". Es bedeutet mathematisch, dass die Wand perfekt ist. Die Sicherheit ist sofort bewiesen.

3. Das Ergebnis: Ein Schritt, nicht zwei
Da das „Prüfen" Teil des „Zeichnens" ist, muss das KI-Gehirn nicht anhalten und ein separates Computerprogramm um Erlaubnis bitten. Es trainiert, und sobald der Wert Null erreicht, ist die Arbeit erledigt. Es gibt keinen zweiten Schritt.

Warum das wichtig ist (laut dem Papier)

Die Autoren testeten diese neue Methode an 13 verschiedenen komplexen Szenarien, darunter:

Einfache Systeme: Wie ein Auto, das sich geradeaus bewegt.
Komplexe Systeme: Roboter mit wackeligen, nichtlinearen Bewegungen (wie ein Pendel oder eine Drohne in einem Sturm).
Hohe Dimensionen: Systeme mit vielen beweglichen Teilen (bis zu 9 Dimensionen).

Die Ergebnisse:

100 % Erfolg: Ihre Methode fand für jeden einzelnen Testfall eine gültige Sicherheitswand.
Geschwindigkeit: Sie war deutlich schneller als die alten „Raten und Prüfen"-Methoden. Zum Beispiel dauerte bei einem komplexen Test die alte Methode 47 Sekunden, während ihre Methode nur 1 Sekunde benötigte.
Vielseitigkeit: Sie bewältigte „seltsame" Mathematik (nicht-polynomiale Dynamiken), die andere Werkzeuge einfach nicht lösen konnten.

Zusammenfassung der Analogie

Alte Methode: Wie ein Bildhauer, der eine Statue meißelt, zurücktritt und einen Richter fragt: „Ist das sicher?" Wenn der Richter „Nein" sagt, meißelt der Bildhauer erneut. Das dauert ewig.
Neue Methode: Wie ein Bildhauer, der einen magischen Meißel besitzt, der nur Stein entfernt, wenn die Statue sicherer wird. Der Bildhauer muss nie anhalten und um Erlaubnis fragen. Wenn der Bildhauer aufhört, ist die Statue garantiert perfekt, weil das Werkzeug selbst dafür gesorgt hat.

Was das Papier nicht behauptet

Es wird nicht behauptet, dass dies selbstfahrende Autos auf den Straßen morgen sofort reparieren wird.
Es wird nicht behauptet, dass dies für jeden möglichen Maschinentyp im Universum funktioniert (nur für die spezifischen mathematischen Modelle, die getestet wurden).
Es wird nicht behauptet, alle anderen Sicherheitsmethoden zu ersetzen, sondern vielmehr eine schnellere, zuverlässigere Möglichkeit anzubieten, diese spezifischen „Barrierenzertifikate" zu synthetisieren.

Kurz gesagt führt das Papier einen intelligenteren Weg ein, um KI zu trainieren, unsichtbare Sicherheitswände zu zeichnen, und verwandelt ein langsames, wiederholendes Ratespiel in einen einzigen, schnellen und mathematisch garantierten Vorgang.

Technische Zusammenfassung: Mengenbasiertes Training neuronaler Barrierenzertifikate zur Sicherheitsverifikation dynamischer Systeme

1. Problemstellung

Die Sicherheitsverifikation kontinuierlicher dynamischer Systeme ist für autonome Agenten in sicherheitskritischen Umgebungen (z. B. autonome Fahrzeuge, UAVs, Roboterarme) von entscheidender Bedeutung. Ein System gilt als sicher, wenn keine Trajektorie, die aus einer Anfangsmenge $X_I$ startet, eine unsichere Menge $X_U$ betritt.

Bestehende Verifikationsmethoden weisen erhebliche Einschränkungen auf:

Simulationsbasierte Methoden leiden unter einem exponentiellen Anstieg der Laufzeit in Abhängigkeit von der Systemdimension.
Erreichbarkeitsanalysen nutzen mengenbasierte Berechnungen, um exponentielle Laufzeiten zu vermeiden, können jedoch rechenintensiv sein.
Barrierenzertifikate bieten einen formalen Sicherheitsbeweis, indem sie eine skalare Funktion $B$ definieren, die $X_I$ über ihre Niveaulinie (Nullniveau) von $X_U$ trennt. Neuere Ansätze zur Synthese neuronaler Barrierenzertifikate basieren jedoch auf einem iterativen Trainings-Verifikations-Zyklus. In diesem Zyklus wird ein neuronales Netzwerk auf Zustandsraumstichproben trainiert und anschließend mittels eines externen Lösers (z. B. SMT) formal verifiziert. Scheitert die Verifikation (Gegenbeispiele werden gefunden), wird das Netzwerk neu trainiert. Dieser Prozess ist kostspielig, erfordert möglicherweise viele Zyklen und garantiert keine Konvergenz zu einem gültigen Zertifikat innerhalb eines einzigen Verfahrens.

2. Methodik: Mengenbasiertes Training

Die Autoren schlagen einen neuartigen mengenbasierten Trainingsansatz vor, der die formale Verifikation direkt in den Trainingsprozess des neuronalen Netzwerks integriert und somit einen separaten Verifikationsschritt überflüssig macht.

Kernkonzept

Anstatt auf diskreten Stichproben zu trainieren und später zu verifizieren, trainiert die Methode das neuronale Netzwerk $B_\theta$ unter Verwendung einer sounden mengenbasierten Verlustfunktion. Diese Verlustfunktion wird über gesamte Mengen (Einschlüsse) des Zustandsraums berechnet und nicht über einzelne Punkte. Wenn der Verlust Null erreicht, ist die Gültigkeit des Barrierenzertifikats durch Konstruktion formal bewiesen.

Wichtige technische Komponenten

A. Sounde mengenbasierte Verlustfunktion
Die Verlustfunktion kodiert die drei für ein Barrierenzertifikat erforderlichen Eigenschaften (Satz 1):

Eigenschaft P I (Unsichere Zustände): Alle Zustände in $X_U$ müssen positive Werte abbilden. Der Verlust $L_I$ bestraft die untere Schranke des mengenbasierten Bildes von $X_U$ .
Eigenschaft P II (Anfangszustände): Alle Zustände in $X_I$ müssen nicht-positive Werte abbilden. Der Verlust $L_{II}$ bestraft die obere Schranke des mengenbasierten Bildes von $X_I$ .
Eigenschaft P III (Dynamik der Nullniveaulinie): Die Lie-Ableitung $L_f B_\theta$ $L_{f} B_{θ}$ muss auf der Nullniveaulinie $X_Z = \{x \mid B_\theta(x) = 0\}$ $X_{Z} = {x ∣ B_{θ} (x) = 0}$ negativ sein.
- Da $X_Z$ unbekannt und nicht-konvex ist, berechnet die Methode einen engen Einschließungsbereich (tight enclosure) von $X_Z$ unter Verwendung einer Vereinigung von Zonotopen mittels einer rekursiven Branch-and-Bound-Strategie (Aufspaltung des Eingaberaums und Verwerfen von Regionen ohne Nullpunkte).
- Für jedes Zonotop im Einschließungsbereich wird die Lie-Ableitung durch mengenbasierte Vorwärtspropagierung von Gradienten und der Systemdynamik eingeschlossen.
- Der Verlust $L_{III}$ bestraft die oberen Schranken dieser Einschließungen der Lie-Ableitung.

Der Gesamtverlust ist $L = L_I + L_{II} + L_{III}$ . Wenn $L=0$ , ist das System formal als sicher verifiziert.

B. Mengenbasierte Vorwärtspropagierung
Um diese Verluste zu berechnen, propagiert die Methode Zonotope (eine spezifische Art von konvexem Polytop) durch die Schichten des neuronalen Netzwerks:

Lineare Schichten: Exakt berechnet durch affine Abbildungen.
Nichtlineare Schichten: Eingeschlossen durch konservative Überapproximationen (z. B. Bereichsbegrenzung).
Gradienten und Lie-Ableitungen: Die Menge der Gradienten wird rückwärts propagiert, und die Lie-Ableitung wird als inneres Produkt der Gradientenmenge und der Flussmenge berechnet.

C. Algorithmus
Die Trainingsschleife (Algorithmus 1) initialisiert das Netzwerk, berechnet mengenbasierte Verluste für $P_I$ , $P_{II}$ und $P_{III}$ , aktualisiert die Parameter mittels Gradientenabstieg und beendet den Vorgang, sobald der Gesamtverlust Null ist.

3. Wichtige Beiträge

Synthese in einem einzigen Verfahren: Ein neuartiger Ansatz zur Synthese neuronaler Barrierenzertifikate in einem einzigen mengenbasierten Trainingsverfahren, der den iterativen Trainings-Verifikations-Zyklus eliminiert.
Sounde Verlustfunktion: Eine mengenbasierte Verlustfunktion, die alle Eigenschaften von Barrierenzertifikaten sound kodiert. Ein Verlustwert von Null stellt einen formalen Sicherheitsbeweis dar.
Iterative Verfeinerung: Ein iteratives Verfahren zur dynamischen Einschließung der Nullniveaulinie und der für Eigenschaft P III erforderlichen Lie-Ableitung.
Umfassende Evaluierung: Evaluierung an 13 Benchmarks, die lineare, polynomiale und nicht-polynomiale Dynamiken abdecken, einschließlich hochdimensionaler Systeme (bis zu 9D) und komplexer Mengenkonfigurationen.

4. Experimentelle Ergebnisse

Der Ansatz wurde mit dem CORA-Toolbox implementiert und mit State-of-the-Art-Tools verglichen: SynNBC und FOSSIL (iteratives Trainings-Verifikations-Verfahren) sowie PRoTECT (Optimierung auf Summen von Quadraten).

Erfolgsrate: Die vorgeschlagene Methode erreichte bei allen 13 Benchmarks eine Erfolgsrate von 100 %.
- Im Gegensatz dazu scheiterten SynNBC und PRoTECT bei nicht-polynomiellen Dynamiken und Benchmarks mit mehreren Anfangs-/unsicheren Mengen.
- FOSSIL erzielte hohe Erfolgsraten, verschlechterte sich jedoch bei höherdimensionalen Systemen (z. B. 70 % bei Peruffo 6D, 80 % bei Peruffo 8D).
Laufzeit: Der mengenbasierte Trainingsansatz war signifikant schneller als FOSSIL. Beispielsweise benötigte die vorgeschlagene Methode im Durchschnitt 1,0 s für den Peruffo-Benchmark (8D), verglichen mit 47,7 s für FOSSIL.
Trainings-Effizienz: Die Methode konvergierte typischerweise innerhalb weniger Trainingsepochen. Im Gegensatz dazu benötigte FOSSIL oft mehrere Trainings-Verifikations-Zyklen, wobei jeder Zyklus bis zu 1.000 Epochen umfassen konnte.
Ablationsstudien:
- Netzwerkarchitektur: Flache Netzwerke (einzelne lineare Schicht) genügten für lineare Systeme, versagten jedoch bei nicht-polynomiellen Systemen. Für komplexe Dynamiken waren tiefere Netzwerke erforderlich.
- Einschließung der Nullniveaulinie: Komplexere Dynamiken erforderten ausgefeiltere Einschließungen der Nullniveaulinie (mehr Aufspaltungen/Iterationen), um Eigenschaft P III zu erfüllen.

5. Bedeutung und Behauptungen

Die Autoren behaupten, dass dieser Ansatz einen Paradigmenwechsel in der Sicherheitsverifikation darstellt, indem er die Trainings- und Verifikationsphasen zusammenführt.

Formale Garantien: Im Gegensatz zum standardmäßigen Training neuronaler Netzwerke, das keine formalen Sicherheitsgarantien bietet, stellt diese Methode sicher, dass ein Verlust von Null ein gültiges Barrierenzertifikat impliziert.
Skalierbarkeit: Die Operationen reduzieren sich auf effiziente Matrixmultiplikationen, was zu einer polynomialen Komplexität führt, die sich gut mit der Systemdimension skaliert.
Vielseitigkeit: Der Ansatz ist weitgehend unabhängig von der Systemdynamik und bewältigt natürlich komplexe nichtlineare (nicht-polynomiale) Dynamiken sowie komplexe Mengendarstellungen (z. B. Vereinigungen von Mengen, nicht-konvexe Regionen), mit denen intervallbasierte Methoden Schwierigkeiten haben.
Effizienz: Durch die Eliminierung des kostspieligen iterativen Zyklus bietet die Methode einen effizienteren Weg zur formalen Verifikation für hochdimensionale und nichtlineare Systeme.

Die Autoren schließen, dass ihre mengenbasierte Synthese Barrierenzertifikate effizient generieren kann, ohne dass eine nachfolgende Verifikation erforderlich ist, und übertrifft frühere Arbeiten insbesondere bei hochdimensionalen und nicht-polynomiellen Systemen.