Lösungsorientierte gegenüber globaler ReLU-Auswahl: Teilweises MILP kehrt für die DNN-Verifikation zurück

Um komplexe Instanzen zu bewältigen, greifen wir erneut auf einen Divide-and-Conquer-Ansatz zurück, um die Komplexität zu reduzieren: anstelle von wenigen, aber komplexen BaB-Aufrufen setzen wir auf zahlreiche kleine, sogenannte partielle MILP-Aufrufe. Der entscheidende Schritt besteht darin, nur wenige, aber besonders wichtige ReLU-Neuronen auszuwählen, die mittels (kostenintensiver) binärer Variablen behandelt werden. Frühere Ansätze waren in dieser Hinsicht suboptimal. Um diese wichtigen ReLU-Variablen zu identifizieren, schlagen wir eine neuartige, lösungsbewusste ReLU-Bewertung („Solution-Aware ReLU Scoring“, kurz {\sf SAS}) vor und adaptieren zudem die BaB-SR- und BaB-FSB-Branching-Funktionen zu globalen ReLU-Bewertungen („Global Scoring“, kurz {\sf GS}). Wir vergleichen die Ansätze theoretisch sowie experimentell und zeigen, dass {\sf SAS} effizienter bei der Auswahl einer Menge von Variablen ist, die mittels binärer Variablen geöffnet werden sollen. Im Vergleich zu früheren Ansätzen reduziert {\sf SAS} die Anzahl der binären Variablen um etwa den Faktor sechs, während die Genauigkeit unverändert bleibt. In der Implementierung im Rahmen von {\em Hybrid MILP}, bei dem zunächst α,β-CROWN mit einer kurzen Time-out-Zeit zur Lösung einfacher Instanzen eingesetzt wird, gefolgt von partiellen MILP-Aufrufen, entsteht ein äußerst genauer und dennoch effizienter Verifikator. Dieser verringert die Anzahl der unentschiedenen Instanzen um bis zu 40 % auf sehr niedrige Werte (8 %–15 %), wobei die Laufzeit dennoch vernünftig bleibt (durchschnittlich 46 s bis 417 s pro Instanz), selbst für relativ große CNNs mit zwei Millionen Parametern.