🤖 machine learning

Deterministic World Models for Verification of Closed-loop Vision-based Systems

Dieses Paper stellt einen deterministischen Weltmodellansatz vor, der durch die Eliminierung stochastischer latenter Variablen und die Integration von Konformalvorhersage die Verifizierung geschlossener, visuell gesteuerter Systeme präzisiert und zu engeren erreichbaren Mengen führt.

Ursprüngliche Autoren: Yuang Geng, Zhuoyang Zhou, Zhongzheng Zhang, Siyuan Pan, Hoang-Dung Tran, Ivan Ruchkin

Veröffentlicht 2026-04-03

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Yuang Geng, Zhuoyang Zhou, Zhongzheng Zhang, Siyuan Pan, Hoang-Dung Tran, Ivan Ruchkin

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

Stell dir vor, du fährst ein autonomes Auto. Es schaut durch eine Kamera auf die Straße, denkt nach und lenkt dann selbst. Das ist ein „End-to-End"-System: Kamera sieht Bild → Computer entscheidet → Auto lenkt.

Das Problem: Niemand kann zu 100 % beweisen, dass dieses System in jeder Situation sicher ist. Warum? Weil Kameras riesige, komplexe Bilder produzieren. Ein Mathematiker kann nicht einfach eine Formel schreiben, die sagt: „Wenn das Auto bei Position X ist, sieht das Bild genau so aus." Die Welt ist zu chaotisch.

Frühere Versuche, das zu lösen, benutzten künstliche Intelligenz, die wie ein Künstler mit einem „Zufalls-Modul" arbeitet. Das ist wie ein Maler, der immer ein paar Würfel wirft, um zu entscheiden, ob er einen Baum grün oder blau malt. Das macht die Bilder bunter, aber für einen Sicherheitsprüfer ist das eine Katastrophe: Wenn der Prüfer nicht weiß, wie die Würfel fallen, muss er alle möglichen Farben (und damit alle möglichen Welten) als gefährlich betrachten. Das Ergebnis: Der Prüfer sagt „Gefahr!", obwohl das Auto eigentlich sicher wäre.

Die Lösung dieser Forscher: Der „Deterministische Welt-Modell"-Baum.

Hier ist die Idee der Autoren aus dem Paper in einfachen Worten, mit ein paar Analogien:

1. Der „Zufalls-Entferner" (Deterministisches Weltmodell)

Statt eines Künstlers mit Würfelwürfen bauen die Forscher einen perfekten Übersetzer.

Die alte Methode: „Ich habe Position X und werfe einen Würfel. Vielleicht wird das Bild so, vielleicht so." (Zu viel Unsicherheit).
Die neue Methode (DWM): „Ich habe Position X. Das Bild sieht immer exakt so aus."
Der Computer lernt eine feste Regel: „Wenn der Wagen hier ist, ist das Bild genau dieses." Es gibt keine versteckten Zufallsvariablen mehr. Das ist wie ein präziser 3D-Drucker: Wenn du die gleichen Daten eingibst, kommt immer das exakt gleiche Bild heraus. Das macht die Berechnung für den Sicherheitsprüfer viel einfacher und genauer.

2. Der „Fahrlehrer" (Die neue Trainings-Methode)

Ein Bild kann schön aussehen, aber trotzdem falsch sein. Stell dir vor, das Bild zeigt ein Stoppschild, aber das Schild ist ein paar Pixel zu weit links. Für das menschliche Auge sieht es fast gleich aus, aber für den Computer-Controller könnte das bedeuten: „Bremsen!" statt „Weiterfahren!".

Die Forscher haben das Modell nicht nur trainiert, damit es hübsche Bilder macht (wie ein Maler), sondern auch, damit es sich richtig verhält (wie ein Fahrlehrer).

Der Trick: Sie haben eine zweite Regel eingeführt. Wenn das künstliche Bild den Computer zu einer anderen Entscheidung bringt als das echte Bild, gibt es eine Strafe.
Analogie: Es reicht nicht, dass der Schüler den Fahrkurs auswendig lernt. Er muss auch so fahren, als wäre er im echten Auto. Das Modell lernt also nicht nur zu malen, sondern zu handeln.

3. Der „Sicherheits-Gürtel" (Conformal Prediction)

Selbst der beste Übersetzer macht kleine Fehler. Vielleicht ist das künstliche Bild um ein winziges bisschen unscharf. Wie können wir dann garantieren, dass das echte Auto sicher ist?

Hier kommt der „Sicherheits-Gürtel" ins Spiel (Conformal Prediction).

Die Forscher lassen das System tausende Male laufen und vergleichen: „Wie weit weicht das künstliche Bild vom echten Bild ab?"
Sie messen den schlimmsten Unterschied, den sie je gesehen haben.
Dann nehmen sie ihre berechneten sicheren Bereiche und dehnen sie um genau diesen maximalen Unterschied aus.
Die Analogie: Stell dir vor, du gehst über eine dünne Eisschicht. Du hast einen Computer, der berechnet, wo das Eis sicher ist. Aber du weißt, der Computer ist nicht perfekt. Also ziehst du einen Sicherheitsgürtel an und gehst nicht direkt auf dem berechneten Pfad, sondern einen Meter daneben. Wenn du dort sicher bist, bist du auch auf dem Pfad sicher. Dieser „Gürtel" ist mathematisch bewiesen und garantiert, dass das echte Auto sicher bleibt, auch wenn das Modell kleine Fehler macht.

Das Ergebnis

In Tests (wie beim Balancieren eines Stabes oder Bremsen eines Autos) war diese neue Methode viel besser als die alten:

Weniger Panik: Sie sagten nicht bei jeder kleinen Unsicherheit „Gefahr!", sondern erkannten echte Sicherheit.
Präzision: Sie fanden die gefährlichen Stellen genau, ohne den ganzen Raum als gefährlich zu markieren.
Garantie: Sie konnten mathematisch beweisen: „Wenn das Modell sagt, es ist sicher, dann ist es mit 95 % Wahrscheinlichkeit auch im echten Leben sicher."

Zusammenfassend:
Die Autoren haben einen Weg gefunden, künstliche Kameras so zu bauen, dass sie keine „Zufallskünstler" sind, sondern präzise Übersetzer. Sie haben sie trainiert, sich wie ein echter Fahrer zu verhalten, und haben am Ende einen mathematischen Sicherheitsgürtel um alles gelegt. So können wir endlich beweisen, dass KI-gesteuerte Autos wirklich sicher sind, ohne nur auf Glück zu hoffen.

1. Problemstellung

End-to-End-Steuerungssysteme, die Roh-Bilddaten direkt in Steuerbefehle umwandeln, werden zunehmend in sicherheitskritischen Anwendungen (z. B. autonomes Fahren, Robotik) eingesetzt. Die formale Verifikation des geschlossenen Regelkreises dieser Systeme stellt jedoch eine große Herausforderung dar.

Es gibt zwei fundamentale Hindernisse:

Fehlendes analytisches State-to-Image-Modell: Für die Verifikation wird eine geschlossene mathematische Formel benötigt, die physikalische Zustände (z. B. Position, Geschwindigkeit) in Kamerabilder übersetzt. Solche Gleichungen existieren für physikalische Dynamiken, aber nicht für die komplexe Bildgenerierung einer Kamera in unstrukturierten Umgebungen.
Explodierende Überapproximation: Herkömmliche Verifikationswerkzeuge, die mit low-dimensionalen Zustandsvektoren arbeiten, scheitern bei hochdimensionalen Bildern. Selbst wenn ein Abbildungsmodell existiert, führt die Propagierung von Bildmengen durch tiefe neuronale Netze zu kumulativen Approximationsfehlern. Herkömmliche generative Modelle (wie cGANs) nutzen stochastische latente Variablen, um die Bildvielfalt zu erhöhen. Diese Variablen haben jedoch keine physikalische Bedeutung, was zu extrem konservativen und unbrauchbar großen Überapproximationen führt, die sichere Trajektorien fälschlicherweise als unsicher kennzeichnen.

2. Methodik: Der Deterministische Weltmodell-Ansatz (DWM)

Die Autoren schlagen einen dreistufigen Ansatz vor, um diese Probleme zu lösen:

A. Deterministisches Weltmodell (DWM)
Statt stochastischer latenter Variablen wird ein latent-freier neuronaler Decoder entwickelt.

Funktionsweise: Das Modell bildet physikalische Zustände ( $s$ ) direkt auf synthetische Kamerabilder ( $\hat{I}$ ) ab: $g_\theta: S \to I$ .
Vorteil: Da die Bildgenerierung nur vom physikalischen Zustand abhängt, entspricht jedes Bild in einer verifizierten Menge einem physikalisch realisierbaren Zustand. Dies schließt die Verifikationsschleife ohne stochastische „Rausch"-Komponenten.

B. Dualer Trainingsverlust (Dual Loss)
Um sicherzustellen, dass das generierte Bild nicht nur visuell ähnlich, sondern auch für die Steuerung relevant ist, wird ein kombinierter Verlust verwendet:

Pixel-Level Rekonstruktionsverlust ( $L_{rec}$ ): Ein gewichteter MSE-Loss, der wichtige Bildbereiche (z. B. Objekte, die für die Steuerung relevant sind) stärker gewichtet als den Hintergrund.
Konsistenzverlust für die Steuerung ( $L_{ctrl}$ ): Dieser Term bestraft die Differenz zwischen den Steuerbefehlen, die aus dem generierten Bild ( $\hat{I}$ ) und dem echten Bild ( $I$ ) berechnet werden ( $||C(\hat{I}) - C(I)||^2$ ). Dies erzwingt eine Verhaltenskonsistenz mit dem realen Controller, auch wenn das Bild visuell leicht abweicht.

C. Verifikationspipeline und Conformal Prediction

Star-basierte Reachability-Analyse: Das trainierte DWM wird in eine Star-basierte Verifikationspipeline integriert. Star-Sets (eine Art von Mengenrepräsentation) werden effizient durch die transponierten Faltungsschichten des DWM, den CNN-Controller und die nichtlinearen Systemdynamiken (via PyBDR) propagiert.
Conformal Prediction (CP) für reale Garantien: Da das DWM ein Surrogat ist, wird die Lücke zum realen System durch Conformal Prediction geschlossen. Anhand von Kalibrierungsdaten (Paare aus realen und simulierten Trajektorien) wird eine statistische, verteilungsfreie Obergrenze ( $\Delta_{1-\alpha}$ ) für die maximale Trajektorienabweichung berechnet.
Inflation: Die errechneten erreichbaren Mengen des Weltmodells werden um diese CP-Grenze erweitert (Minkowski-Summe). Dies liefert eine probabilistische Garantie ( $1-\alpha$ ), dass die realen Trajektorien innerhalb der erweiterten Mengen liegen.

3. Schlüsselbeiträge

Deterministisches Weltmodell: Ein neuartiger Ansatz zur Erstellung verifizierbarer generativer Surrogate für Kamerasensoren durch Eliminierung stochastischer latenter Variablen.
Erweiterung der Star-basierten Analyse: Die erste Anwendung von Star-basierten Reachability-Analysen auf den geschlossenen Regelkreis von bildbasierten Systemen.
Realistische Garantien: Die Integration von Conformal Prediction, um die Ergebnisse des Weltmodells mit hoher Wahrscheinlichkeit auf das reale physikalische System zu übertragen.
Dual-Loss-Strategie: Ein Trainingsansatz, der visuelle Genauigkeit mit verhaltensbezogener Konsistenz (Steuerungsreaktion) kombiniert.

4. Ergebnisse

Die Methode wurde an vier Benchmarks getestet: CartPole, MountainCar, Pendulum und ein Bremssystem.

Vergleich mit cGAN-Baseline: Das DWM übertrifft den cGAN-basierten Ansatz (der latente Variablen nutzt) signifikant.
- F1-Scores: Das DWM erzielt in allen Umgebungen deutlich höhere F1-Scores (z. B. 0,9817 bei MountainCar vs. 0,7990 beim cGAN).
- Präzision und Recall: Das DWM erreicht eine Präzision von 1,0 (keine falschen Positiv-Meldungen von Unsicherheit) und einen höheren Recall als die Baseline. Die cGAN-Baseline war extrem konservativ und klassifizierte in einigen Fällen (MountainCar, Bremssystem) alle Startzustände als unsicher (Recall 1,0, aber True Negative Rate 0,0), da die erreichbaren Mengen den gesamten Zustandsraum überdeckten.
Einfluss des Dual Loss: Der Ablationsstudie zufolge reduziert der Kontroll-Konsistenz-Loss ( $L_{ctrl}$ ) die Trajektorienabweichung (Conformal Bound $\Delta_{0.95}$ ) weiter. Ohne diesen Loss sind die Bounds bereits kleiner als beim cGAN, aber mit dem Loss werden sie noch enger (z. B. von 0,111 auf 0,093 beim CartPole).
Reale Garantien: Durch die Inflation mit Conformal Prediction bleiben die Ergebnisse robust. Bei Systemen mit geringer Fehlerempfindlichkeit (MountainCar, Bremssystem) bleibt die Leistung hoch. Bei hochsensiblen Systemen (CartPole) führt die notwendige Inflation zwar zu einem Rückgang des Recall, bietet aber eine mathematisch fundierte Sicherheit, die bei reinen Surrogat-Verifikationen fehlt.

5. Bedeutung und Fazit

Das Paper adressiert eine kritische Lücke in der Sicherheitsverifikation von KI-gesteuerten Systemen. Es zeigt, dass die Verwendung stochastischer latenter Variablen in generativen Modellen für formale Verifikationszwecke kontraproduktiv ist, da sie die Überapproximation unvermeidbar in die Unbrauchbarkeit treiben.

Durch den Wechsel zu einem deterministischen, zustandsbasierten Weltmodell und die Kombination mit Conformal Prediction gelingt es erstmals, geschlossene Regelkreise von bildbasierten Controllern mit engen, aussagekräftigen erreichbaren Mengen zu verifizieren. Dies ermöglicht es, Sicherheitsgarantien für reale Systeme zu geben, ohne auf die Komplexität der Bildverarbeitung verzichten zu müssen. Die Arbeit legt den Grundstein für den sicheren Einsatz von End-to-End-Vision-Systemen in kritischen Infrastrukturen.