🤖 machine learning

Mining Verdict Boundaries for Neural Network Verification

Dieses Paper schlägt einen effizienten Branch-and-Bound-Ansatz für die Verifizierung neuronaler Netze vor, der Pfadmonotonie und exponentielle Suche nutzt, um simultan mehrere Aktivierungsfunktionen zu spalten und dadurch irrelevante Teilprobleme zu überspringen sowie Urteilsgrenzen präzise zu lokalisieren, ohne die kostspielige sequentielle Grenzwertfortpflanzung bestehender Methoden anzuwenden.

Ursprüngliche Autoren: Jiawei Ren, Guanqin Zhang, Zhenya Zhang, Yulei Sui

Veröffentlicht 2026-08-03

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Jiawei Ren, Guanqin Zhang, Zhenya Zhang, Yulei Sui

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 versuchen, einem Roboter das Autofahren sicher beizubringen. Sie wollen absolut sicher sein, dass der Roboter niemals einen Unfall baut, egal was auf der Straße passiert. Das ist die Welt der neuronalen Netzwerk-Verifikation. Betrachten Sie ein neuronales Netzwerk als ein riesiges, komplexes Labyrinth aus Schaltern und Hebeln. Um zu beweisen, dass der Roboter sicher ist, müssen wir jeden möglichen Pfad durch dieses Labyrinth prüfen, um sicherzustellen, dass keiner von ihnen zu einem Unfall führt.

Das Problem ist, dass diese Labyrinthe riesig sind. Jeden einzelnen Pfad nacheinander zu prüfen, ist wie der Versuch, den Ozean mit einem Strohhalm zu trinken – es dauert eine Ewigkeit. Deshalb nutzen Wissenschaftler einen cleveren Trick namens Branch and Bound. Stellen Sie sich vor, Sie suchen einen verborgenen Schatz in einem riesigen Wald. Anstatt jeden einzelnen Baum abzulaufen, teilen Sie den Wald in kleinere Abschnitte auf. Sie prüfen einen Abschnitt schnell aus der Ferne; wenn er sicher aussieht, überspringen Sie den Rest dieses Gebiets. Wenn er gefährlich aussieht, teilen Sie diesen Abschnitt in noch kleinere Stücke auf und prüfen ihn weiter. Diese „Teile und Herrsche“-Methode ist großartig, aber sie erfordert immer noch viel Laufarbeit und Überprüfungen. Die große Frage ist: Wie können wir aufhören, einen Abschnitt zu prüfen, sobald wir wissen, dass er sicher ist, ohne Zeit mit dem Durchwandern jedes einzelnen Baumes in diesem Patch zu verschwenden?

Genau dieses Problem wollten die Forscher in dieser Arbeit lösen. Sie stellten fest, dass die „Sicherheitsbewertung“ (Safety Score) in der Regel auf eine vorhersehbare Weise besser wird, während man tiefer in diese Waldabschnitte vordringt. Es ist wie das Besteigen eines Hügels: Sobald man beginnt, nach oben zu steigen, steigt man immer weiter an, bis man den Gipfel erreicht. Die alte Methode des Prüfens war wie das Machen eines winzigen Schritts nach dem anderen, wobei nach jedem einzelnen Schritt geprüft wurde, ob man den Gipfel erreicht hat. Das ist gründlich, aber quälend langsam.

Die Autoren, Jiawei Ren und sein Team, erkannten, dass sie Schritte überspringen konnten. Sie schlugen eine neue Methode namens BMiner vor. Anstatt winzige Schritte zu machen, nutzen sie zwei kluge Tricks, um voraus zu springen. Der erste Trick ist wie eine exponentielle Suche: Man macht einen riesigen Sprung, dann einen doppelt so großen Sprung, dann einen dreifach so großen Sprung, bis man den Gipfel überschießt. Sobald man weiß, dass man über den Gipfel gesprungen ist, geht man einfach ein paar Schritte zurück, um die exakte Stelle zu finden. Der zweite Trick ist noch klüger: die gradientenbasierte Suche. Das ist so, als würde man die Steilheit des Hügels betrachten. Wenn der Boden sehr steil ansteigt, weiß man, dass man nahe am Gipfel ist, also kann man einen großen, selbstbewussten Sprung machen. Wenn der Hügel flach ist, macht man einen kleineren Schritt.

Durch die Verwendung dieser „Vorsprung-Strategien“ gelang es dem Team, neuronale Netzwerke viel schneller zu verifizieren. In ihren Tests an Standardmodellen der Computer Vision (unter Verwendung von Datensätzen wie MNIST und CIF-10) reduzierte ihre Methode die Zeit, die für den Sicherheitsbeweis benötigt wurde, um durchschnittlich 17 % bis 30 %. In den besten Fällen sparten sie fast 45 % der Zeit ein. Sie haben nicht nur geraten; sie haben diese Simulationen an 500 verschiedenen Verifikationsproblemen durchgeführt und ihre Ergebnisse mit den derzeit besten Werkzeugen verglichen. Die Ergebnisse zeigten, dass sie durch das „Mining“ der „Urteilsgrenze“ (Verdict Boundary) – dem exakten Punkt, an dem ein Problem von „unsicher“ zu „sicher“ wechselt – eine massive Anzahl unnötiger Prüfungen überspringen konnten.

Das Paper adressierte auch eine Sorge: Was ist, wenn der Hügel nicht perfekt glatt ist? Was ist, wenn es einen winzigen Hügel gibt, an dem die Sicherheitsbewertung leicht absinkt, bevor sie wieder ansteigt? Die Forscher überprüften dies und fanden heraus, dass solche Unebenheiten zwar existieren, aber selten und meist klein sind. Ihre Methode ist robust genug, um diese Hindernisse zu bewältigen, ohne verwirrt zu werden. Kurz gesagt: Sie haben nicht nur einen schnelleren Wanderer gebaut; sie haben Jetpacks für den Verifikationsprozess gebaut, die es uns ermöglichen, das „Sicher“-Fazit viel schneller und mit weniger Aufwand zu erreichen.

Technisches Resümee: Mining von Urteilsgrenzwerten für die Verifizierung neuronaler Netze

Problemstellung

Die Verifizierung neuronaler Netze ist entscheidend für die Gewährleistung der Sicherheit in Domänen wie dem autonomen Fahren, insbesondere gegenüber adversariellen Störungen. Während Branch and Bound (BaB) als ein State-of-the-Art-Ansatz für die vollständige Verifizierung hervorgetreten ist, leidet es unter erheblicher Ineffizienz. BaB arbeitet, indem es ein Verifizierungsproblem adaptiv in Teilprobleme (dargestellt als Baum) aufteilt und auf jedes dieser Teilprobleme fertige, approximierte Verifizierer anwendet.

Die in dieser Arbeit identifizierte Kernineffizienz liegt darin, wie bestehende BaB-Ansätze die Urteilsgrenze (verdict boundary) lokalisieren. Eine Urteilsgrenze ist der Punkt entlang eines Baumpfades, an dem sich der Verifizierungsstatus von „unverifiziert“ (Approximationsfehler $\hat{p} < 0$ ) zu „verifiziert“ (Approximationsfehler $\hat{p} > 0$ ) verschiebt. Aufgrund der nahezu monotonen Natur von $\hat{p}$ entlang eines Pfades (da das Aufteilen des Problems den Approximationsfehler reduziert) sind die vor der Grenze liegenden Knoten unverifiziert und die nachfolgenden Knoten verifiziert.

Aktuelle Methoden (z. B. $\alpha\beta$ -Crown) führen eine lineare Suche entlang jedes Pfades durch, wobei sie jeden Knoten sequenziell besuchen, um diese Grenze zu finden. Dies erfordert kostspielige Grenzwertpropagation an jedem besuchten Knoten, selbst für Knoten, die eindeutig unverifiziert oder verifiziert sind, was zu redundanten Rechenaufwänden führt.

Methodik

Die Autoren schlagen BMiner vor, ein neues Verifizierungs-Framework, das die Aufgabe der Lokalisierung der Urteilsgrenze als ein Suchproblem in einem nahezu sortierten Array umformuliert. Anstatt Knoten einzeln zu besuchen, nutzt BMiner die Monotonie von $\hat{p}$ , um unnötige Teilprobleme zu überspringen. Das Framework führt zwei unterschiedliche Suchstrategien ein:

1. Exponentielle Suche (BMinerE)

BMinerE passt den klassischen exponentiellen Suchalgorithmus an, um die Urteilsgrenze in zwei Phasen zu lokalisieren:

Bereichserkennung: Beginnend beim aktuellen Knoten erweitert der Algorithmus den Suchbereich mit einer exponentiell zunehmenden Größe, um schnell einen Bereich $[i_l, i_r]$ zu identifizieren, der den Grenzpunkt enthält.
Binäre Suche: Soblich der Bereich etabliert ist, wird eine binäre Suche innerhalb von $[i_l, i_r]$ durchgeführt, um die exakte Grenzposition zu bestimmen.
Dieser Ansatz reduziert die Anzahl der Knotenbesuche im Vergleich zur linearen Suche erheblich, insbesondere wenn sich die Grenze nicht am Ende eines sehr langen Pfades befindet.

2. Gradientenbasierte Suche (BMinerG)

BMinerG optimiert den Prozess weiter, indem es quantitative Informationen aus den Verifizierer-Bewertungen ( $\hat{p}$ ) nutzt, um die Position der Grenze präziser zu schätzen.

Gradientenschätzung: Der Algorithmus behandelt den Absolutwert $|\hat{p}|$ als Zielfunktion und schätzt den „Gradienten“ (Änderungsrate) von $\hat{p}$ entlang des Pfades unter Verwendung zuvor besuchter Knoten.
Positionsbestimmung: Basierend auf dem geschätzten Gradienten schätzt der Algorithmus die Position, an der $\hat{p}$ die Null kreuzt. Er überprüft diesen geschätzten Knoten und aktualisiert die Gradienteninformationen iterativ.
Verfeinerung: Dieser Prozess verengt den Suchbereich $[i_l, i_r]$ aggressiver als die exponentielle Suche, bevor eine abschließende binäre Suche angewendet wird. Diese Methode zielt darauf ab, die Anzahl der Knotenbesuche zu minimieren, indem sie die Lage der Grenze basierend auf der Rate der Verbesserung der Approximation schätzt.

Beide Ansätze übernehmen und erweitern die State-of-the-Art ReLU-Selektionsstrategie (z. B. FSB), um sich in bestehende Frameworks zu integrieren. Konkret wird die Selektionsheuristik so erweitert, dass sie die Top- $k$ -Neuronen zum gleichzeitigen Splitting auswählt, wobei $k$ der Anzahl der Neuronen entspricht, die durch die Suchmethode übersprungen werden. Die Suche selbst erfolgt jedoch durch sequenzielles Überprüfen der Knoten entlang eines Pfades, um die Grenze zu identifizieren, anstatt mehrere Aktivierungsfunktionen in einem einzigen Schritt gleichzeitig zu splitten.

Zentrale Beiträge

Formulierung der Urteilsgrenze: Die Arbeit formalisiert den BaB-Verifizierungsprozess als Suche nach einer Urteilsgrenze in einem nahezu monotonen Baumpfad und identifiziert, dass bestehende lineare Suchstrategien suboptimal sind.
BMiner-Framework: Die Einführung zweier neuartiger Suchalgorithmen (exponentiell und gradientenbasiert), die grenzferne Teilprobleme überspringen und somit die Anzahl der aufwendigen Aufrufe an approximierte Verifizierer reduzieren.
Umgang mit Nicht-Monotonie: Die Autoren demonstrieren empirisch, dass moderne BaB-Implementierungen (wie $\alpha\beta$ -Crown) zwar eine lokale Nicht-Monotonie in $\hat{p}$ aufweisen können, diese Verstöße jedoch selten sind und die Gesamteffektivität der vorgeschlagenen Suchstrategien nicht signifikant beeinflussen.
Integration: Der Ansatz übernimmt und erweitert die State-of-the-Art ReLU-Selektionsstrategie, was eine Integration in aktuelle State-of-the-Art-Tools ermöglicht.

Experimentelle Ergebnisse

Die Autoren evaluierten BMiner auf 500 Verifizierungsinstanzen über fünf neuronale Netzmodelle (MNISTL2, MNISTL4, OVAL21BASE, OVAL21WIDE, OVAL21DEEP) unter Verwendung der Datensätze MNIST und CIFAR-10. Sie verglichen BMinerE und BMinerG mit $\alpha\beta$ -Crown (dem Gewinner von VNN-COMP) und Oliva.

Verifizierungsfähigkeit: BMinerE und BMinerG erreichten eine vergleichbare oder leicht höhere Anzahl zertifizierter Instanzen als $\alpha\beta$ -Crown, übertrafen Oliva jedoch konsistent in der Zertifizierung (obwohl Oliva bei der Falsifizierung stärker blieb).
Zeiteffizienz:
- BMinerG erzielte die signifikantesten Verbesserungen und reduzierte die durchschnittliche Verifizierungszeit um 17,0 % bis 29,2 % über alle Modelle hinweg, mit einer maximalen Reduktion von 44,7 % über die fünf neuronalen Netze.
- BMinerE bot eine konsistente durchschnittliche Verbesserung von etwa 4 %.
- In Worst-Case-Szenarien führten die aggressiven Suchstrategien gelegentlich zu einem Overhead (bis zu ~16,7 %) aufgrund von Backtracking, wenn die initiale Schätzung die Grenze überschossen hatte.
Auswirkung der Nicht-Monotonie: Die Analyse zeigte, dass die Leistung von BMinerE und BMinerG selbst auf nicht-monotonen Pfaden stabil und konsistent blieb, was bestätigt, dass lokale Verletzungen der Monotonie den Ansatz nicht behindern.
Mechanismus-Analyse: Die Leistungssteigerungen wurden der Fähigkeit zugeschrieben, lange Pfade effizient zu handhaben. Insbesondere BMinerG zeigte eine überlegene Effizienz in langen Pfaden (Länge 16–40), indem es deutlich weniger Knotenbesuche benötigte (z. B. 6,3 vs. 11,2) als BMinerE und die Baseline.

Bedeutung und Behauptungen

Das Paper behauptet, dass durch die Umformulierung des Verifizierungsprozesses als Boundary-Mining-Problem die Rechenkosten der BaB-basierten Verifizierung drastisch gesenkt werden können, ohne die Vollständigkeit zu opfern. Die Autoren betonen, dass ihr Ansatz kein Ersatz für approximierte Verifizierer ist, sondern eine Optimierung der Suchstrategie um diese herum.

Die Bedeutung liegt in der Reduktion der durchschnittlichen Verifizierungszeit um 17 % bis 30 %, was einen primären Flaschenhals in der formalen Verifizierung neuronaler Netze adressiert. Die Autoren merken bescheiden an, dass ihre aktuelle Implementierung eine CPU-basierte Ausführung nutzt, zukünftige Arbeiten jedoch die Effizienz durch GPU-Parallelisierung und Meta-Heuristik-Falsifizierung weiter steigern könnten. Sie räumen auch ein, dass die aktuelle ReLU-Selektionsstrategie eine Erweiterung bestehender Methoden ist, was den Entwurf neuartiger, prädiktionsbewusster Selektionsheuristiken zu einer zukünftigen Forschungsrichtung macht.