Talking with Verifiers: Automatic Specification Generation for Neural Network Verification

Die Arbeit stellt ein Framework vor, das natürliche Sprachspezifikationen automatisch in formale Abfragen übersetzt, um die Anwendbarkeit neuronaler Netzwerk-Verifikationswerkzeuge auf komplexe, semantische Anforderungen in verschiedenen Domänen zu erweitern.

Das Wesentliche

Stellen Sie sich vor, Sie haben einen extrem klugen, aber sehr wortwörtlichen Sicherheitsinspektor für ein selbstfahrendes Auto. Dieser Inspektor ist ein Meister in der Mathematik und kann beweisen, dass das Auto unter bestimmten Bedingungen sicher fährt. Aber er hat ein riesiges Problem: Er versteht nur eine sehr trockene, technische Sprache.

Wenn Sie ihm sagen: „Pass auf, dass das Auto nicht ausbricht, wenn ein Kind auf die Straße läuft", versteht er das nicht. Er braucht stattdessen eine Liste von Koordinaten: „Wenn sich ein Objekt zwischen X=10 und X=20 befindet und die Geschwindigkeit Y ist..."

Das ist das Problem, das die Autoren dieses Papiers lösen wollen. Sie nennen es „Talking with Verifiers" (Mit den Prüfern sprechen).

Hier ist die einfache Erklärung, wie sie das machen, mit ein paar anschaulichen Vergleichen:

1. Das Problem: Der Dolmetscher fehlt

Bisher mussten Experten die Wünsche von normalen Menschen (wie „Das Auto darf nicht bremsen, wenn es regnet") in diese langweilige Koordinaten-Sprache übersetzen. Das ist wie wenn Sie versuchen, einem Computer zu erklären, wie man einen Kuchen backt, indem Sie ihm die chemische Formel für Mehl und Eier geben, statt einfach zu sagen: „Mische die Zutaten."

Das ist mühsam, fehleranfällig und für die meisten Leute unmöglich. Viele wichtige Sicherheitsregeln bleiben deshalb ungetestet, weil niemand sie in die Sprache des Computers übersetzen kann.

2. Die Lösung: Ein intelligenter Dolmetscher

Die Autoren haben eine Art Übersetzer-Team gebaut, das zwischen dem Menschen und dem strengen Sicherheitsinspektor steht. Dieses Team besteht aus drei Schritten, die wie eine gut organisierte Produktionskette funktionieren:

• Schritt 1: Der Zuhörer (Der KI-Sprachmodell)
  Stellen Sie sich einen sehr aufmerksamen Sekretär vor, der Ihre natürliche Sprache hört. Wenn Sie sagen: „Das Vogelbild soll auch dann richtig erkannt werden, wenn der Schnabel verdeckt ist", schreibt dieser Sekretär auf: „Objekt: Vogel-Schnabel. Aktion: Verdecken." Er ignoriert die umständliche Formulierung und holt das Wichtigste heraus.

• Schritt 2: Der Sucher (Der KI-Sicht-Modell)
  Jetzt kommt ein Detektiv ins Spiel. Er nimmt das Bild des Vogels und sucht genau nach dem, was der Sekretär notiert hat: „Wo ist der Schnabel?" Der Detektiv zeigt mit einem roten Kasten genau auf den Schnabel im Bild. Er weiß also genau, wo im Bild die Veränderung stattfinden soll.

• Schritt 3: Der Übersetzer (Der Generator)
  Dieser Schritt nimmt die Notizen des Sekretärs und die Koordinaten des Detektivs und wandelt sie in die strenge Sprache des Sicherheitsinspektors um. Er sagt dem Inspektor: „Prüfe bitte nur den Bereich innerhalb dieses roten Kastens (dem Schnabel) und simuliere, ob er verdeckt wird."

3. Das Ergebnis: Der Inspektor kann endlich arbeiten

Jetzt, wo die Anfrage in der richtigen Sprache formuliert ist, kann der ursprüngliche Sicherheitsinspektor (der Neural-Netzwerk-Verifizierer) seine Arbeit tun. Er prüft mathematisch, ob das System sicher bleibt, auch wenn der Schnabel verdeckt ist.

Warum ist das so genial?

• Keine neuen Werkzeuge nötig: Der eigentliche Sicherheitsinspektor muss nicht verändert werden. Man hat ihm nur einen Dolmetscher zur Seite gestellt.
• Für alles geeignet: Ob es um Tabellen mit Zahlen (z. B. Kreditwürdigkeit) geht, um Bilder (Vögel, Autos) oder sogar um Töne (Notfall-Sirenen), das System funktioniert.
• Menschlich: Sie können einfach sagen, was Sie wollen, so wie Sie es einem Kollegen erklären würden.

Ein anschauliches Beispiel aus dem Papier

Stellen Sie sich vor, Sie haben eine Kamera, die Vögel erkennt.

• Der alte Weg: Sie müssten manuell berechnen: „Wenn der Schnabel bei Pixel 100 bis 150 liegt und die Helligkeit um 20% sinkt..." – Das ist für einen Menschen kaum machbar.
• Der neue Weg: Sie sagen einfach: „Der Vogel wird immer noch erkannt, auch wenn sein Schnabel verdeckt ist."
  • Das System sucht den Schnabel im Bild.
  • Es verdeckt ihn digital.
  • Es prüft, ob die KI immer noch „Vogel" sagt.
  • Ergebnis: „Sicher" oder „Unsicher".

Fazit

Dieses Papier ist wie der Bau einer Brücke zwischen der menschlichen Welt (wo wir mit Begriffen und Ideen denken) und der Welt der formellen Mathematik (wo Computer Sicherheit beweisen). Es macht es möglich, dass wir komplexe Sicherheitsregeln für KI-Systeme einfach in unsere Muttersprache formulieren können, ohne selbst Mathematiker oder Programmierer zu sein. Das ist ein riesiger Schritt, um KI in sicherheitskritischen Bereichen wie Medizin oder autonomem Fahren wirklich vertrauenswürdig zu machen.

Technische Zusammenfassung

1. Problemstellung

Aktuelle Werkzeuge zur formalen Verifikation von neuronalen Netzen (DNNs) sind auf eine sehr eingeschränkte Klasse von Spezifikationen beschränkt. Diese werden typischerweise als niedrigstufige numerische Constraints über rohe Eingabe- und Ausgabedimensionen formuliert (z. B. „Ändere den Pixelwert an Position $x,y$ um $\epsilon$").

Dies führt zu zwei Hauptproblemen:

• Mangelnde Ausdruckskraft: Viele semantisch sinnvolle Anforderungen (z. B. „Das Bild eines Vogels bleibt korrekt klassifiziert, auch wenn sein Schnabel verdeckt ist") lassen sich nicht natürlich in festgelegte Koordinaten oder globale Störungsbereiche übersetzen.
• Hohe Hürde für Anwender: Endnutzer müssen ihre hochleveligen Absichten manuell in spezifische, verifikatorische Sprachen übersetzen. Dies erfordert tiefes Fachwissen, ist fehleranfällig und verhindert die breite Anwendung formaler Verifikation in sicherheitskritischen Domänen wie autonomem Fahren oder medizinischer Diagnostik.

Das Kernproblem liegt in der Diskrepanz zwischen den internen, für Menschen nicht direkt interpretierbaren Repräsentationen von Deep Learning-Modellen und den menschlich verständlichen semantischen Konzepten.

2. Methodik

Die Autoren schlagen einen neuen Ansatz vor, der eine Integrations-Schicht zwischen natürlichen Sprachspezifikationen und bestehenden Verifikations-Engines einführt, ohne die Verifikationsalgorithmen selbst zu ändern. Das System ist als End-to-End-Pipeline konzipiert, die drei Hauptstufen umfasst:

1. Parsing (LLM-basiert):

   • Ein Large Language Model (LLM) analysiert die natürliche Sprachanforderung des Nutzers.
   • Es extrahiert semantische Objekte (z. B. „Schnabel", „Alter") und Operationen (z. B. „verdecken", „amplifizieren", „unter 50 sein").
   • Das LLM strukturiert diese Informationen in eine maschinenlesbare Form.

2. Grounding / Detektion (Perzeptions-Modelle):

   • Basierend auf dem konkreten Eingabedatum (z. B. einem Bild oder einer Tabelle) werden die extrahierten semantischen Objekte lokalisiert.
   • Für strukturierte Daten (Tabellen): Eine direkte Abbildung der extrahierten Feature-Namen auf Eingabe-Indizes.
   • Für unstrukturierte Daten (Bilder/Audio): Nutzung von Open-Vocabulary-Modellen (Zero-Shot).
     • Bilder: Modelle wie Grounding DINO lokalisieren Objekte basierend auf Textbeschreibungen und liefern Bounding-Box-Koordinaten.
     • Audio: (Theoretisch skizziert) Modelle zur Sound-Event-Lokalisierung würden zeitliche Intervalle identifizieren.
   • Hinweis: Der Nutzer kann die Ergebnisse der Detektion interaktiv genehmigen, falls Unsicherheiten bestehen.

3. Spezifikations-Generierung:

   • Ein Generator wandelt die lokalisierten Koordinaten und die Operation in eine formale, numerische Verifikationsabfrage ($P_x$) um.
   • Diese Abfrage ist kompatibel mit bestehenden Verifikatoren (z. B. für lokale Robustheit).
   • Beispiel: Aus „Verdecke den Schnabel" wird eine Maske über die Bounding-Box des Schnabels generiert, gefolgt von der Bedingung, dass die Ausgabe des Netzes unverändert bleiben muss.

3. Wichtige Beiträge

1. Identifikation der Usability-Lücke: Das Paper hebt hervor, dass die manuelle Übersetzung von Nutzerabsichten in niedrigstufige Constraints ein Hauptgrund für die geringe Adoption formaler Verifikation ist.
2. Automatisierte Generierungs-Mechanismus: Entwicklung einer Pipeline, die natürliche Sprache über Multimodal-Modelle (LLMs, VLMs) in formale Constraints übersetzt. Dies funktioniert für tabellarische Daten, Bilder und (konzeptionell) Audio.
3. Modulare Integration: Der Ansatz erfordert keine Änderungen an den bestehenden Verifikations-Backends. Er nutzt stattdessen reife Komponenten (Foundation Models), sodass Verbesserungen in Sprach- oder Perzeptionsmodellen sofort die Genauigkeit der Spezifikation erhöhen.
4. Empirische Validierung: Demonstration der Machbarkeit an realen Datensätzen, um semantische Robustheit zu prüfen, die bisher nicht verifizierbar war.

4. Ergebnisse und Evaluation

Die Autoren evaluieren den Ansatz an zwei repräsentativen Benchmarks:

• Tabellarische Daten: Statlog (German Credit Data) – Kreditrisiko-Klassifikation.
• Bilddaten: CUB-200-2011 – Feinkörnige Vogelklassifikation.

Quantitative Ergebnisse:

• Parsing-Accuracy: Die LLMs (Gemini 3 Flash, GPT 5 Mini) erreichen eine hohe Genauigkeit (85–100 %) beim Extrahieren von Objekten und Aktionen aus dem Text.
• Grounding-Accuracy (Objekterkennung): Bei der Bilderkennung mit Grounding DINO liegt die Genauigkeit pro Konfiguration zwischen 23 % und 55 %.
• Ensemble-Effekt: Interessanterweise erreicht die Disjunktion aller Konfigurationen (d.h. wenn mindestens eine Konfiguration das Objekt korrekt findet) eine Trefferquote von 83 %. Dies zeigt, dass das System durch die Kombination verschiedener Parameter robust ist.
• Laufzeit: Die Parsing-Phase ist schnell (ca. 1–5 Sekunden), was die praktische Anwendbarkeit unterstreicht.

Qualitative Ergebnisse:

• Das System konnte komplexe Anfragen wie „Kann sich die Vorhersage ändern, wenn der violette Dorn unten lauter wird?" erfolgreich verarbeiten.
• Es wurde gezeigt, dass das System semantische Regionen (z. B. nur den Schnabel eines Vogels) isoliert und lokale Robustheitsprüfungen durchführt, anstatt das gesamte Bild zu stören.

5. Bedeutung und Ausblick

Dieses Werk stellt einen Paradigmenwechsel dar, indem es formale Verifikation von neuronalen Netzen für hochlevelige, semantische Anforderungen zugänglich macht.

• Praktische Relevanz: Es ermöglicht die Verifikation von Anforderungen, die in der realen Welt tatsächlich relevant sind (z. B. ethische oder regulatorische Constraints), ohne dass Experten die Mathematik hinter den Constraints manuell codieren müssen.
• Zukunft: Die Autoren planen, den Ansatz auf Video und zeitliche Audio-Konstraints zu erweitern sowie die räumliche Grounding von Bounding-Boxen auf pixelgenaue Segmentierung zu verfeinern.

Zusammenfassend demonstriert das Paper, dass die Kombination von Foundation Models mit bestehenden Verifikations-Tools eine praktikable Brücke schlägt, um die Lücke zwischen menschlicher Intention und formaler mathematischer Garantie zu schließen.