Formal Reasoning About Confidence and Automated Verification of Neural Networks

Diese Arbeit stellt ein generalisiertes Framework vor, das durch die Einführung zusätzlicher Schichten in neuronale Netze eine einheitliche formale Verifikation von sowohl Robustheit als auch Konfidenz ermöglicht und dabei bestehende ad-hoc-Ansätze signifikant übertrifft.

Das Wesentliche

Das Problem: Der nervige Schüler und sein Selbstvertrauen

Stell dir vor, du hast einen Schüler (ein Neuronales Netzwerk), der Bilder von Tieren erkennt. Wenn du ihm ein Bild von einem Pferd zeigst, sagt er: „Das ist ein Pferd!" und ist sich zu 99 % sicher.

Bisher haben Forscher nur darauf geachtet, ob dieser Schüler bei kleinen Änderungen am Bild (z. B. ein paar Pixel verrauscht, wie ein kleiner Fleck auf der Linse) immer noch das richtige Wort sagt. Das nennt man Robustheit.

Aber hier ist das Problem:

1. Der falsche, aber selbstbewusste Schüler: Manchmal sagt der Schüler bei einem leicht veränderten Bild plötzlich „Das ist ein Auto!", aber er ist sich nur zu 5 % sicher. Er weiß eigentlich nicht, was er sagt. Ist das ein großes Problem? Vielleicht nicht, denn er war sich ja nicht sicher.
2. Der richtige, aber unsichere Schüler: Manchmal sagt er immer noch „Pferd", aber seine Sicherheit fällt von 99 % auf 30 %. Er zögert. Ist das auch ein Problem? Ja, denn ein selbstbewusster Schüler, der plötzlich zögert, ist gefährlich (z. B. beim autonomen Fahren).

Bisherige Werkzeuge zur Überprüfung haben nur geschaut: „Hat er das Wort geändert?" Sie haben ignoriert, wie sicher er sich war. Das ist wie ein Lehrer, der nur prüft, ob die Antwort stimmt, aber nicht darauf achtet, ob der Schüler panisch oder gelassen wirkt.

Die Lösung: Eine neue Sprache für das Selbstvertrauen

Die Autoren dieses Papiers sagen: „Wir brauchen eine neue Art, Fragen zu stellen!"

Sie haben eine Grammatik (eine Art Bauplan für Fragen) entwickelt, die es erlaubt, Dinge wie zu fragen:

• „Ist die Antwort immer noch 'Pferd', ODER ist er sich so unsicher (unter 20 %), dass wir ihm verzeihen können?"
• „Ist er sich immer noch zu 80 % sicher, auch wenn das Bild leicht verzerrt ist?"
• „Sind die Top-2-Tipps (z. B. Pferd oder Esel) immer noch dieselben, auch wenn er nicht mehr zu 100 % sicher ist?"

Das ist wie ein neuer Fragebogen für den Schüler, der nicht nur nach dem Ergebnis fragt, sondern auch nach dem Gefühl dahinter.

Das große Hindernis: Die Übersetzer-Probleme

Das Problem ist: Die Computerprogramme, die diese Schüler testen (die Verifikatoren), sind wie sehr spezialisierte Übersetzer. Sie verstehen nur einfache Sätze wie „Antwort ist A" oder „Antwort ist B". Sie verstehen keine komplexen Sätze mit „UND", „ODER" und „WENN die Sicherheit unter X fällt".

Wenn man ihnen diese neuen, komplizierten Fragen direkt gibt, stolpern sie oder brauchen ewig, um sie zu lösen. Man müsste den Code jedes einzelnen Programms umschreiben, was wie das Umrüsten eines ganzen Autos wäre, nur um ein neues Navi zu installieren.

Der geniale Trick: Das Anhängen eines Anhängers

Hier kommt die kreative Idee der Autoren ins Spiel. Statt den Verifikator (das Auto) zu ändern, bauen sie einen kleinen Anhänger an das neuronale Netzwerk (den Schüler) an.

1. Der Trick: Sie fügen ein paar extra Schichten (wie eine kleine Rechenmaschine) direkt hinter das neuronale Netzwerk.
2. Die Funktion: Diese extra Schichten nehmen die komplizierte Frage (z. B. „Ist die Sicherheit hoch ODER ist die Antwort gleich?") und wandeln sie in einen ganz einfachen Satz um, den der Verifikator versteht: „Ist das Ergebnis dieser Rechenmaschine größer als 0?"
3. Das Ergebnis: Der Verifikator sieht nur noch einen einfachen Satz und denkt: „Oh, das kann ich!" Er muss nicht umgebaut werden. Er kann einfach den Schüler mit dem Anhänger prüfen.

Man kann sich das vorstellen wie einen Dolmetscher, der zwischen einem komplizierten Philosophen (dem neuen Fragebogen) und einem strengen Richter (dem Verifikator) steht. Der Dolmetscher (die extra Schichten) übersetzt die komplexe Philosophie in einfache Ja/Nein-Fragen, die der Richter versteht.

Warum ist das toll?

• Flexibilität: Man kann jetzt jede Art von Robustheit prüfen, die man sich ausdenkt, ohne die Werkzeuge zu ändern.
• Geschwindigkeit: Die Autoren haben es an tausenden von Beispielen getestet (von kleinen Bildern bis zu riesigen Netzwerken wie bei ImageNet). Ihr Ansatz war viel schneller als die alten Methoden, bei denen man alles manuell umschreiben musste.
• Sicherheit: Es hilft uns zu verstehen, wann ein KI-System wirklich sicher ist und wann es nur zufällig richtig liegt, aber eigentlich unsicher ist.

Zusammenfassung in einem Satz

Die Autoren haben eine Methode entwickelt, bei der sie KI-Netzwerken einen kleinen „Rechen-Anhänger" anhängen, damit diese Netzwerke komplexe Fragen über ihr eigenes Selbstvertrauen beantworten können, ohne dass die Prüfer (die Computerprogramme) dafür umgebaut werden müssen.

Technische Zusammenfassung

1. Problemstellung

In den letzten Jahren hat sich ein großer Teil der Forschung zur Robustheit neuronaler Netze auf die Überprüfung konzentriert, ob die Klassifizierungsentscheidung bei kleinen Eingangsstörungen (Adversarial Examples) unverändert bleibt. Ein zentrales Defizit bestehender Ansätze ist jedoch die Ignorierung des Konfidenzniveaus (Vertrauenswürdigkeit) der Ausgabe.

• Das Dilemma: Ein Netzwerk kann zwar bei einer gestörten Eingabe falsch klassifizieren, aber mit sehr niedriger Konfidenz. Sollte dies als „nicht robust" gewertet werden? Umgekehrt kann die Klassifikation korrekt bleiben, aber die Konfidenz drastisch sinken, was auf eine Instabilität hindeutet.
• Herausforderung: Bestehende Verifikationswerkzeuge (wie Marabou oder $\alpha\beta$-CROWN) sind oft auf einfache Nachbedingungen (Post-Conditions) optimiert, die typischerweise nur Disjunktionen oder Konjunktionen linearer Atome über den Ausgaben erlauben. Komplexe Eigenschaften, die Konfidenz (Softmax-Funktion) und logische Kombinationen beinhalten, sind schwer direkt zu kodieren, da die Softmax-Funktion nicht-linear ist und die Verifizierung von komplexen booleschen Kombinationen in Nachbedingungen oft tiefgreifende Änderungen an den Solvern erfordert oder nur mit spezifischen, nicht skalierbaren Encodings möglich ist.

2. Methodik

Die Autoren schlagen einen einheitlichen Rahmen vor, der es ermöglicht, Konfidenz-basierte Spezifikationen formal zu modellieren und mit bestehenden Verifikations-Tools zu überprüfen, ohne den Code der Solver ändern zu müssen.

A. Grammatik für Konfidenz-Spezifikationen

Es wird eine ausdrucksstarke Grammatik definiert, die boolesche Kombinationen aus linearen Bedingungen und Konfidenz-Bedingungen (CC) erlaubt.

• Konfidenz-Bedingungen (CC): Diese basieren auf der Softmax-Funktion, die Logits in Wahrscheinlichkeiten (0–100 %) umwandelt.
• Approximation der Softmax-Funktion: Da Softmax exponentielle Terme enthält und für lineare Solver (LRA – Linear Real Arithmetic) nicht direkt handhabbar ist, wird eine Approximation eingeführt. Die Autoren leiten formale Schranken her, die Konfidenz-Bedingungen (z. B. $Conf(\bar{y}, t) < b$) in lineare Ungleichungen zwischen den Logits umwandeln. Dies geschieht unter Beibehaltung formaler Garantien für den Approximationsfehler.

B. Kodierung durch zusätzliche Schichten (Layer-Based Encoding)

Der Kernbeitrag ist eine Technik, um beliebige Nachbedingungen der definierten Grammatik in eine Form zu überführen, die von Standard-Verifikatoren als einfache Nachbedingung (z. B. $y \ge 0$) akzeptiert wird.

• Idee: Anstatt die Nachbedingung als externe Constraint zu kodieren, werden zusätzliche Schichten an das neuronale Netz angehängt.
• Mechanismus:
  • Die logische Struktur der Nachbedingung (Boolesche Kombinationen von $\land$ und $\lor$) wird in ein neuronales Netz-Subnetz übersetzt.
  • ReLU-Aktivierung: ReLU-Funktionen werden genutzt, um logische Operationen zu modellieren.
    • Für eine Konjunktion ($\land$) wird eine Summe von ReLUs verwendet, die nur dann Null ist, wenn alle Eingaben negativ sind.
    • Für eine Disjunktion ($\lor$) wird die Logik invertiert.
  • Flip-Operation: Um Konjunktionen und Disjunktionen zu kombinieren (da sie Eingaben unterschiedlich interpretieren), wird eine „Flip"-Operation eingeführt, die Signale invertiert, während die Fehlergrenzen niedrig gehalten werden.
• Vorteil: Das resultierende Netz hat eine vereinfachte Nachbedingung (z. B. „Ausgabe $y < \eta$"), die von jedem State-of-the-Art-Verifikator (wie $\alpha\beta$-CROWN oder Marabou) als Blackbox verarbeitet werden kann. Dies eliminiert die Notwendigkeit, Solver-Code anzupassen.

C. Unterstützte Robustheits-Varianten

Der Rahmen deckt verschiedene Robustheitsdefinitionen ab:

1. Relaxed Robustness: Ignoriert Fehlklassifikationen, wenn die Konfidenz unter einem Schwellenwert $\tau$ liegt.
2. Strong Robustness: Fordert, dass die Konfidenz für die korrekte Klasse auch bei Störungen über einem Schwellenwert bleibt, selbst wenn die Klasse nicht wechselt.
3. Smoothness: Begrenzt die Variation der Konfidenz innerhalb einer $\epsilon$-Umgebung (Lipschitz-Stetigkeit der Konfidenz).
4. Top-k Robustness: Fordert, dass die Top-k Vorhersagen (die $k$ höchsten Logits) unter Störungen unverändert bleiben.

3. Wichtige Beiträge

1. Generalisierte Grammatik: Einführung einer Grammatik, die Konfidenz-basierte und logische Bedingungen vereint und etablierte Konzepte (Strong, Top-k) sowie neue (Relaxed) abdeckt.
2. Formale Softmax-Approximation: Entwicklung einer Approximation der Softmax-Funktion in lineare rationale Arithmetik (LRA) mit nachweisbaren Fehlergrenzen.
3. Einheitliche Kodierungstechnik: Ein neuartiger Ansatz, der komplexe Nachbedingungen durch das Anhängen weniger Schichten in einfache lineare Bedingungen umwandelt. Dies ermöglicht die Nutzung leistungsstarker Solver wie $\alpha\beta$-CROWN für komplexe Eigenschaften.
4. Skalierbarkeit und Effizienz: Die Methode ist universell einsetzbar und erfordert keine Anpassung der Verifikations-Tools.

4. Ergebnisse und Experimente

Die Autoren führten eine umfassende Evaluierung an 8.870 Benchmarks durch, die aus den VNN-COMP Wettbewerben (2021–2024) stammen.

• Datensätze: MNIST, CIFAR-10, Traffic Sign Recognition (GTSRB) und ImageNet.
• Netzwerkgrößen: Von kleinen Netzen (0,51K ReLUs) bis hin zu sehr großen Architekturen (bis zu 13,16 Millionen Aktivierungseinheiten, 138 Millionen Parameter).
• Vergleich: Der Ansatz wurde mit ad-hoc Kodierungen in einem constraint-basierten Solver (Marabou) und mit dem State-of-the-Art-Verifier $\alpha\beta$-CROWN verglichen.
• Ergebnisse:
  • Die layer-basierte Kodierung in Kombination mit $\alpha\beta$-CROWN übertraf sowohl die ad-hoc Kodierung in Marabou als auch die layer-basierte Kodierung in Marabou signifikant.
  • Dies liegt daran, dass $\alpha\beta$-CROWN effiziente Techniken wie PGD-Angriffe und CROWN-Bound-Propagation nutzt, die durch die vereinfachte Nachbedingung voll zur Geltung kommen.
  • Die Methode skalierte erfolgreich auf große Netze (ImageNet), wo andere Ansätze oft an Speicher- oder Zeitgrenzen scheiterten.
  • Die Abhängigkeit von Schwellenwerten (z. B. Konfidenz $\tau$) zeigte erwartete Trends: Höhere Schwellenwerte für „Relaxed Robustness" führten zu mehr verifizierten „sicheren" Fällen und weniger Timeouts.

5. Bedeutung und Fazit

Dieses Paper schließt eine wichtige Lücke in der formalen Verifikation neuronaler Netze, indem es das Konzept der Konfidenz systematisch in die Robustheitsanalyse integriert.

• Praktische Relevanz: Es bietet Ingenieuren und Forschern ein Werkzeug, um realistischere Robustheitskriterien zu definieren, die nicht nur auf binären Klassifizierungsfehlern basieren, sondern auch die Unsicherheit des Modells berücksichtigen.
• Technischer Fortschritt: Die vorgestellte Technik, Nachbedingungen durch Netzschichten zu kodieren, ist ein eleganter Weg, um die Komplexität der Spezifikation von der Komplexität des Verifikators zu entkoppeln. Sie ermöglicht es, fortschrittliche Verifikatoren als Blackbox für hochkomplexe, konfidenzbasierte Eigenschaften zu nutzen.
• Zukunft: Der Ansatz ebnet den Weg für die Verifikation von sicherheitskritischen Anwendungen (z. B. autonomes Fahren, medizinische Diagnose), bei denen nicht nur die Korrektheit, sondern auch die Zuverlässigkeit (Konfidenz) der Vorhersage entscheidend ist.