⚡ electrical engineering

Certified Neural Approximations of Nonlinear Dynamics

Dieses Paper führt eine neuartige, adaptive und parallelisierbare Verifizierungsmethode ein, die formale Fehlergrenzen für neuronale Netzwerkapproximationen nichtlinearer dynamischer Systeme bereitstellt, deren sichere Bereitstellung in sicherheitskritischen Kontexten ermöglicht und bestehende State-of-the-Art-Ansätze in verschiedenen Benchmarks, einschließlich der Kompression neuronaler Netze und der Trajektorienvorhersage auf Basis des Koopman-Operators, übertrifft.

Ursprüngliche Autoren: Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano, Luca Laurenti, Alessandro Abate

Veröffentlicht 2026-06-04

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano, Luca Laurenti, Alessandro Abate

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 haben eine sehr komplexe, unvorhersehbare Maschine – wie etwa einen Jetmotor oder ein Wettersystem. Um diese zu verstehen, ihre Zukunft vorherzusagen oder sie sicher zu halten, benötigen Ingenieure in der Regel ein mathematisches Modell. Aber diese realen Modelle sind oft so chaotisch und nichtlinear (wellig, verdreht, schwer zu berechnen), dass Computer Schwierigkeiten haben, zu verifizieren, ob sie sicher sind.

Um dies zu lösen, nutzen Wissenschaftler oft ein „vereinfachtes Modell“, wie zum Beispiel ein neuronales Netz (eine Art KI), um die echte Maschine nachzuahmen. Betrachten Sie das neuronale Netz als eine Cartoon-Version des echten Jetmotors. Es ist viel einfacher für einen Computer, den Cartoon zu lesen als den komplexen Bauplan.

Das Problem:
Die Gefahr besteht darin, dass der Cartoon zwar die meiste Zeit richtig aussieht, aber an einer winzigen, kritischen Stelle versagt. Wenn Sie den Cartoon zur Steuerung des echten Jetmotors verwenden, könnte dieser winzige Fehler einen Absturz verursachen. In der Vergangenheit erforderte die Prüfung, ob der Cartoon „gut genug“ dem Original entspricht, einen superstarken, langsamen Computer (einen SMT-Solver), der versuchte, jede einzelne Möglichkeit zu prüfen. Das war so, als würde man versuchen, jedes Sandkorn an einem Strand einzeln zu zählen, um zu sehen, ob der Strand sicher ist. Es dauerte zu lange und konnte keine großen, komplexen Systeme bewältigen.

Die Lösung: „Zertifizierte neuronale Approximationen“
Dieses Paper stellt eine neue, schnellere Methode vor, um zu prüfen, ob der KI-Cartoon sicher genug ist, um verwendet zu werden. So sind sie dabei vorgegangen, unter Verwendung einfacher Analogien:

1. Die „Lokale Karte“-Strategie (First-Order-Modelle)

Anstatt zu versuchen, das gesamte wendige, komplexe System auf einmal zu verstehen, zerlegen die Autoren das Verhalten der Maschine in kleine, handhabbare Stücke.

Die Analogie: Stellen Sie sich vor, Sie wandern einen sehr steilen, kurvigen Berg hinauf. Es ist schwer, den gesamten Pfad auf einmal vorherzusagen. Aber wenn Sie den Fokus nur auf Ihre unmittelbaren Füße richten, sieht der Boden flach aus.
Die Methode: Sie unterteilen den gesamten „Berg“ (die möglichen Zustände des Systems) in winzige, rechteckige Boxen. Innerhalb jeder winzigen Box nehmen sie an, dass die komplexe Kurve tatsächlich eine gerade Linie ist (ein „First-Order-Modell“). Dies ist viel einfacher zu berechnen. Dann fügen sie einen „Sicherheitspuffer“ (eine Fehlerschranke) um diese gerade Linie hinzu, um zu berücksichtigen, dass der echte Boden tatsächlich kurvig ist.

2. Die „Intelligente Verfeinerung“ (Adaptive Partitionierung)

Manchmal ist eine gerade Linie keine gute Annäherung für einen sehr kurvigen Teil des Berges.

Die Analogie: Wenn Sie auf einem flachen Pfad gehen, reicht eine große Karte gut aus. Aber wenn Sie auf eine steile Klippe oder eine kurvige Wendung treffen, müssen Sie näher heranzoomen und eine viel detailliertere Karte nur für diesen spezifischen Ort zeichnen.
Die Methode: Wenn der Computer feststellt, dass die Schätzung durch die „gerade Linie“ zu weit von der echten Maschine abweicht, teilt er diese Box automatisch in der Mitte und versucht es erneut mit kleineren, detaillierteren Boxen. Er zoomt also nur dort hinein, wo es tatsächlich nötig ist, was massiv Zeit spart.

3. Das „Parallele Team“ (Parallelisierung)

Die Analogie: Anstatt dass eine Person den ganzen Berg alleine überprüft, stellen Sie sich ein Team von 8 Wanderern vor. Jeder Wanderer übernimmt gleichzeitig einen anderen Abschnitt des Berges, um ihn zu prüfen.
Die Methode: Die Autoren haben ihre Methode „parallelisierbar“ gemacht, was bedeutet, dass sie mehrere Computerprozessoren gleichzeitig nutzen kann, um verschiedene Teile des Systems simultan zu prüfen. Dies macht den Verifizierungsprozess unglaublich schnell.

Was sie erreicht haben

Durch diesen „Hineinzoomen, Gerade-Linien-Check und Team-Check“-Ansatz waren sie in der Lage:

Schneller zu werden: Sie verifizierten Systeme bis zu 820 Mal schneller als bisherige beste Methoden.
Größer zu werden: Sie konnten viel größere und komplexere Systeme (bis zu 7 Dimensionen) handhaben, bei denen sich bisherige Methoden geschlagen gaben.
Präziser zu werden: Sie sagten nicht nur „es ist sicher“ oder „es ist unsicher“. Sie konnten exakt bestimmen, wo es sicher war und wo es versagen könnte, selbst wenn das Gesamtsystem nicht perfekt war.

Zwei neue Abenteuer

Die Autoren zeigten auch, dass diese Methode für zwei schwierige neue Aufgaben funktioniert:

Komprimierung von KI: Sie nahmen ein riesiges, aufgeblähtes KI-Modell (wie eine gigantische Enzyklopädie) und schrumpften es auf eine winzige Version (wie einen Taschenführer) zusammen, während sie bewiesen, dass die kleine Version fast exakt wie die große handelt.
Vorhersage von Trajektorien mit Koopman-Operatoren: Sie nutzten ihre Methode, um eine KI zu prüfen, die die gesamte zukünftige Flugbahn eines Systems (wie einen Ball, der einen Hügel hinunterrollt) auf einmal vorhersagt, anstatt nur den nächsten Schritt. Dies ist nützlich für Dinge wie die Steuerung von Raumfahrzeugen oder Roboter.

Zusammenfassend:
Dieses Paper liefert uns einen neuen, superschnellen Weg, um zu beweisen, dass der KI-„Cartoon“ einer komplexen Maschine sicher genug ist, um eingesetzt zu werden. Anstatt das Ganze auf einmal mit einer langsamen Brute-Force-Methode zu prüfen, zerlegen sie es in winzige Teile, prüfen die Teile mit einfacher Mathematik und zoomen nur dort hinein, wo es notwendig ist. Dies ermöglicht es uns, KI in sicherheitskritischen Situationen zu vertrauen, in denen wir dies zuvor nicht konnten.

Technisches Resümee: Zertifizierte neuronale Approximationen nichtlinearer Dynamiken

Problemstellung

Nichtlineare dynamische Systeme sind grundlegend für cyber-physische Systeme, jedoch schwierig direkt zu verifizieren und zu steuern. Eine gängige Strategie besteht darin, eine Abstraktion zu konstruieren – ein vereinfachtes Modell, das das Originalsystem approximiert. Neuronale Netze haben sich als effektive Werkzeuge für diesen Zweck erwiesen, da sie in der Lage sind, Zustandsräume implizit zu partitionieren und vereinfachte Dynamiken zu erlernen.

Für diese neuronalen Abstraktionen ist es jedoch entscheidend, dass sie für kritische Anwendungen sicher sind, indem sie über formale Garantien hinsichtlich ihrer Nähe zum echten System verfügen. Konkret muss zertifiziert werden, dass das neuronale Netz $N(x)$ die wahre Dynamik $f(x)$ innerhalb eines begrenzten Fehlers $\epsilon$ (d. h. $\|f(x) - N(x)\|_\infty \le \epsilon$ ) über ein gegebenes Gebiet approximiert.

Bestehende Verifikationsmethoden verlassen sich stark auf SMT-Solver (Satisfiability Modulo Theories, z. B. dReal), um über nichtlineare reelle Arithmetik zu schlussfolgern. Während diese Solver fundiert sind, leiden sie unter schwerwiegenden Skalierbarkeitsproblemen und scheitern oft daran, größere Netzwerke oder hochdimensionale Systeme innerhalb einer angemessenen Zeitspanne zu verifizieren. Dieser rechnerische Flaschenhals schränkt die praktische Anwendung neuronaler Abstraktionen auf komplexe, hochdimensionale Szenarien ein.

Methodik

Die Autoren schlagen ein neuartiges, skalierbares Verifikationsframework vor, das die Abhängigkeit von teuren SMT-Solvern für nichtlineare Arithmetik eliminiert. Stattdessen nutzt die Methode zertifizierte First-Order-Taylor-Modelle und eine parallelisierbare adaptive Partitionierungsstrategie.

1. Zertifizierte First-Order-Taylor-Modelle

Anstatt das nichtlineare Prädikat $\exists x : \|f(x) - N(x)\| > \epsilon$ direkt zu verifizieren, approximiert die Methode die wahre Dynamik $f(x)$ lokal mittels Taylor-Entwicklungen erster Ordnung.

Lokale Linearisierung: Das Eingangsgebiet $X$ wird in Hyperrechtecke unterteilt. Innerhalb eines Hyperrechtecks $H_\delta(c)$ , das um $c$ zentriert ist, werden die Dynamiken durch eine lineare Funktion plus einen Restterm begrenzt:
$f(x) \in (f(c) + J_f(c)(x - c)) \oplus R$
wobei $J_f(c)$ die Jacobi-Matrix und $R$ ein zertifizierter Fehlergrenzwert ist, der aus der Lagrange-Fehlergrenze (für glatte Funktionen) oder CROWN (für ReLU-Netzwerke) abgeleitet wurde.
Verifikation via linearer Solver: Diese Transformation wandelt das Verifikationsproblem in die Prüfung der Erfüllbarkeit linearer Ungleichungen um. Die Autoren verwenden Marabou 2.0, ein Tool zur Verifikation neuronaler Netze, das auf linearer Grenzwertpropagation basiert, um diese Bedingungen zu verifizieren. Dies vermeidet die Rechenkosten der nichtlinearen Arithmetik-Argumentation.

2. Adaptive Zertifikatsverfeinerung

Um die durch lineare Approximationen entstehende Konservativität (bei der der Fehlerwert $R$ zu groß sein könnte) zu adressieren, verwendet das Framework eine adaptive Verfeinerungsstrategie:

Splitting-Kriterien: Ein Hyperrechteck wird aufgeteilt, wenn:
1. Der Taylor-Restwert-Grenzwert zu konservativ ist ( $R_{max} - R_{min} > \epsilon$ ).
2. Ein vom Solver gefundener potenzieller Gegenbeispiel die wahre Fehlerbedingung nicht erfüllt (ein „spurious“ bzw. Schein-Gegenbeispiel aufgrund der Linearisierung).
Zielgerichtete Partitionierung: Die Aufteilungsachse wird basierend auf dem Beitrag der Eingangsdimensionen zum Approximationsfehler gewählt, wobei Dimensionen, die an nichtlinearen Termen beteiligt sind, priorisiert werden. Dies ermöglicht eine ausgab Abhängige Verfeinerung, bei der verschiedene Ausgabendimensionen unterschiedliche Partitionierungsgrade erfordern können.
Parallelisierung: Der Verifikationsprozess wird mittels eines Shared-Stack (Depth-First-Search) parallelisiert, auf den ein Pool von Worker-Prozessen zugreift. Jeder Worker verarbeitet ein Hyperrechteck, zertifiziert es oder teilt es auf und legt die Sub-Regionen zurück in den Stack.

3. Training

Neuronale Netze werden trainiert, um sowohl den mittleren quadratischen Fehler als auch den maximalen $L_\infty$ -Fehler über Stichproben zu minimieren. Die Verlustfunktion enthält einen Term für den Worst-Case-Fehler, um die Effizienz der Stichprobenverwendung zu verbessern.

Kernbeiträge

SMT-freie Verifikation: Die Einführung einer Methode basierend auf zertifizierten Linearisierungen, die den primären Engpass vorangegangener Ansätze (die nichtlineare reelle Arithmetik-Argumentation) beseitigt.
Adaptive parallele Verfeinerung: Eine skalierbare Strategie, die eine adaptive Verifikation mit nicht-uniformer Genauigkeit über das Eingangsgebiet ermöglicht und so die Konservativität signifikant reduziert, ohne die Fundiertheit (Soundness) zu gefährden.
Skalierbarkeit: Die Fähigkeit, höhere Dimensionen (bis zu 7D) und deutlich größere neuronale Netze als State-of-the-Art-Methoden zu handhaben.
Neuartige Anwendungen: Die Erweiterung der neuronalen Abstraktionen auf zwei bisher schwer handhabbare Szenarien:
- Neuronale Kompression: Verifizierung, dass ein komprimiertes Netz einem größeren „Lehrer“-Netz $\epsilon$ -nah bleibt.
- Entdeckung von Koopman-Operatoren: Verifizierung von Trajektorien-Vorhersagen, bei denen die Ausgabe des Netzes eine Sequenz zukünftiger Zustände darstellt (über 100 Zustände in der letzten Schicht).

Experimentelle Ergebnisse

Die Methode wurde mit etablierten Benchmarks aus der Literatur (z. B. WaterTank, JetEngine, Van der Pol Oscillator) sowie neuen, anspruchsvollen Aufgaben evaluiert.

Performance vs. State-of-the-Art: Im Vergleich zum dReal-basierten Ansatz (Abate et al., 2022) zeigte die vorgeschlagene Methode erhebliche Beschleunigungen. Beispielsweise war die neue Methode beim WaterTank-Benchmark etwa 820 Mal schneller. Während dReal bei den meisten großen Modellen (z. B. 3x[64]-Architektur für JetEngine, SteamGovernor) zeitlich ablief (1-Stunden-Limit), konnte die vorgeschlagene Methode 100 % des Gebiets für alle getesteten Modelle, einschließlich hochdimensionaler Systeme wie dem Low Thrust Spacecraft (7D), erfolgreich zertifizieren.
Koopman-Operatoren: Das Framework konnte erfolgreich ein Trajektorien-Vorhersage-Netzwerk basierend auf der Koopman-Theorie verifizieren. Trotz der Tatsache, dass das Netzwerk einen niedrigen mittleren quadratischen Fehler auf Validierungsdaten erreichte, identifizierte die Verifikation spezifische Gegenbeispiele, bei denen der Fehler die Toleranz ( $\epsilon=0.1$ ) überschritt. Entscheidend war, dass das System 99,03 % des Eingangsgebiets zertifizierte und somit granulare Einblicke lieferte, wo das Modell vertrauenswürdig ist – eine Fähigkeit, die Methoden fehlt, die lediglich ein einzelnes Gegenbeispiel zurückgeben.
Neuronale Kompression: Die Methode verifizierte ein komprimiertes Netz (reduziert von 4,2 Mio. auf 67k Parameter, eine Reduktion um 98,4 %), das die Dynamik des Lorenz-Attraktors approximiert. Der Verifikationsprozess prüfte über 3,5 Millionen Hyperrechtecke und schloss in etwa 89 Stunden ab, was die Machbarkeit für groß angelegte, nicht-analytische Dynamiken demonstriert.

Bedeutung und Ansprüche

Das Paper behauptet, dass seine primäre Bedeutung in der Lösung des Skalierbarkeitsengpasses der neuronalen Abstraktionsverifikation liegt. Durch die Entkopplung der Verifikation des neuronalen Netzes (gehandhabt durch lineare Solver) von der Verifikation der nichtlinearen Dynamik (gehandhabt durch lokale Linearisierung und Verfeinerung) ermöglichen die Autoren die formale Verifikation komplexer, hochdimensionaler Systeme, die zuvor unhandhabbar waren.

Die Autoren betonen, dass ihr Ansatz formale Fehlergrenzen liefert, die es erlauben, neuronale Approximationen sicher als Surrogatmodelle einzusetzen, indem der Fehler als begrenzte Störung interpretiert wird. Diese Fundiertheit erlaubt es, auf der Abstraktion verifizierte Eigenschaften (wie Sicherheit oder Erreichbarkeit) rigoros auf das konkrete System zu übertragen. Die Arbeit hebt zudem die Vielseitigkeit des Frameworks hervor, indem sie zeigt, dass es über Standard-Dynamiksysteme hinaus auf allgemeine Funktionsapproximationsaufgaben wie Netzwerkkompression und Deep-Learning-Architekturen für die Operatorentheorie angewendet werden kann.