Stellen Sie sich eine Welt vor, in der die „Gehirne“ unserer Autos, medizinischen Geräte und Sicherheitssysteme aus riesigen, komplexen Netzen von Mathematik bestehen, die man neuronale Netze nennt. Diese digitalen Gehirne sind unglaublich gut darin, Gesichter zu erkennen oder das Wetter vorherzusagen, aber sie sind auch notorisch schwer zu verstehen. Da sie durch das Finden von Mustern in Daten lernen und nicht durch das Befolgen strenger, schriftlicher Regeln, ist es schwierig zu wissen, ob sie Fehler machen werden, wenn die Dinge seltsam werden. Dies ist ein großes Problem für die Sicherheit: Wenn das Gehirn eines selbstfahrenden Autos eine falsche Vermutung anstellt, können Menschen zu Schaden kommen. Also arbeitet eine Gruppe von Wissenschaftlern an einer Möglichkeit, mathematisch zu beweisen, dass diese Netzwerke immer korrekt reagieren werden, egal welche Eingabe sie erhalten. Stellen Sie sich diesen Prozess wie einen Detektiv vor, der versucht, ein riesiges Rätsel zu lösen, indem er jeden einzelnen möglichen Hinweis überprüft. Der Detektiv muss das Rätsel in immer kleinere Teile zerlegen und jeden Teil prüfen, um zu sehen, ob er zu einem Widerspruch (einem „Bug“) oder zu einem sicheren Ergebnis führt. Die Herausforderung besteht darin, dass es so viele mögliche Hinweise gibt, dass das Überprüfen aller einzeln länger dauern würde als das Zeitalter des Universums. Der Detektiv benötigt eine kluge Strategie, um zu entscheiden, welchen Hinweis er als Nächstes prüfen soll, in der Hoffnung, dass eine einzige Wahl das gesamte Rätsel schnell löst.

Dieses Paper stellt eine clevere neue Strategie für diesen Detektiv vor, die „Lookahead Branching“ genannt wird. Die Forscher fanden heraus, dass es – bei der Arbeit mit zwei verschiedenen Arten von Verifizierungswerkzeugen (eines namens Marabou und ein anderes namens α-β-CROWN) – statt nur basierend auf dem, was gerade passiert, zu raten, welchen Hinweis man als Nächstes prüfen sollte, besser ist, kurz in die Zukunft zu blicken und zu simulieren. Stellen Sie sich vor, Sie spielen eine Partie Schach. Ein Standardspieler schaut sich vielleicht das Brett an und wählt den Zug, der im Moment am besten aussieht. Aber ein Großmeister denkt jedoch: „Wenn ich hierhin ziehe, wird mein Gegner dorthin ziehen, und dann kann ich dorthin ziehen...“ Die Autoren schlagen vor, dass neuronale Netzwerk-Verifizierer genau das tun sollten: Bevor sie eine Entscheidung treffen, sollten sie kurz „träumen“, was passieren würde, wenn sie verschiedene Pfade einschlugen. Sie fanden heraus, dass das Werkzeug durch das Aufwenden von etwas zusätzlicher Zeit, um die zukünftigen Schritte zu simulieren, bessere Entscheidungen treffen kann, was zu schnelleren Lösungen führt und mehr Probleme als zuvor löst. In ihren Tests half dieser Ansatz den Werkzeugen, bis zu 57 % mehr Instanzen zu lösen und machte sie signifikant schneller, insbesondere bei den schwierigsten Problemen.

Der Kern des Papers ist die Frage, wie man dieses „Träumen“ effizient gestaltet. Die Forscher haben ein allgemeines Rezept erstellt, das in jedes dieser Verifizierungswerkzeuge eingefügt werden kann. Der Prozess funktioniert so: Wenn das Werkzeug ein Problem aufteilen muss, wählt es nicht einfach eine Option. Stattdessen wählt es ein paar vielversprechende Kandidaten aus und simuliert das Aufteilen für jeden von ihnen. Es blickt ein paar Schritte voraus (die „Lookahead-Tiefe“), um zu sehen, wie sich das Problem verändert. Wenn eine Aufteilung zu einer Situation führt, in der viele andere verwirrende Teile des Netzwerks plötzlich klar werden (wie ein Neuron, das „instabil“ war und plötzlich „festgelegt“ ist), erhält diese Aufteilung eine hohe Punktzahl. Das Werkzeug wählt dann die Aufteilung mit der höchsten Punktzahl.

Die Autoren entdeckten auch, dass diese Simulation nicht nur dazu dient, den besten Pfad auszuwählen; sie kann tatsächlich neue Fakten finden. Manchmal, indem das Werkzeug eine Aufteilung simuliert, erkennt es, dass ein bestimmter Teil des Netzwerks in einem bestimmten Zustand sein muss, noch bevor es diese Aufteilung offiziell vornimmt. Dies ermöglicht es dem Werkzeug, diese Teile des Netzwerks sofort zu „fixieren“, was riesige Teile unnötiger Arbeit einspart. Das Paper zeigt, dass dies in zwei sehr unterschiedlichen Arten von Verifizierungswerkzeugen gut funktioniert: einem, das auf Standard-Prozessoren läuft (Marabou), und einem, das leistungsstarke Grafikkarten verwendet (α-β-CROWN).

In ihren Experimenten testete das Team diese Methode an einer Vielzahl von neuronalen Netzen, von einfachen, die handgeschriebene Ziffern erkennen, bis hin zu komplexen, die in der Computer Vision eingesetzt werden. Beim Marabou-Tool half Lookahead dabei, mehr Probleme zu lösen und die benötigte Zeit für schwierige Fälle zu reduzieren. Beispielsweise löste das Tool auf einem spezifischen Benchmark-Satz namens NN4Sys mit Lookahead mehr Instanzen als ohne. Beim α-β-CROWN-Tool, das für seine Schnelligkeit bekannt ist, gelang es der Lookahead-Strategie dennoch, die Lösungszeit zu verkürzen und ein paar zusätzliche Probleme zu lösen, die die Standardmethode verpasst hätte. Die Forscher merkten an, dass der Lookahead-Prozess zwar ein wenig zusätzliche Zeit für die Einrichtung benötigt, der Ertrag jedoch enorm ist, da er verhindert, dass das Werkzeug später Zeit auf schlechten Pfaden verschwendet.

Das Paper weist jedoch vorsichtig darauf hin, dass dies kein Zaubermittel ist, das alles sofort löst. Der „Lookahead“-Prozess ist rechenintensiv, was bedeutet, dass er mehr Rechenleistung benötigt, um vorauszudenken. Die Autoren fanden heraus, dass es am besten funktioniert, wenn es ganz am Anfang der Suche eingesetzt wird, wo die Entscheidungen die größte Auswirkung auf die Zukunft haben. Wenn man versucht, es bei jedem einzelnen Schritt einzusetzen, könnten die Kosten des Vorausdenkens den Nutzen überwiegen. Sie testeten auch verschiedene Möglichkeiten, den Lookahead aufzubauen, wie zum Beispiel, wie viele Schritte man vorausblickt und wie viele Kandidaten man simuliert, und fanden heraus, dass eine moderate Tiefe (zwei Schritte vorausblicken) bei den schwierigsten Problemen gut funktionierte.

Das Paper argumentiert explizit gegen die Idee, dass wir nur schnelle, lokale Informationen zur Entscheidungsfindung verwenden sollten. Während schnelle Heuristiken (Faustregeln) gut für die Geschwindigkeit sind, übersehen sie oft das große Ganze und können den Verifizierer in eine Sackgasse führen. Die Autoren zeigen, dass die Investition von etwas mehr Aufwand im Vorfeld, um die Konsequenzen einer Aufteilung zu simulieren, den gesamten Verifizierungsprozess wesentlich effizienter macht. Sie stellen auch klar, dass sich ihre Methode von der Verwendung künstlicher Intelligenz zur Erlernung des Branching unterscheidet: Anstatt ein Modell auf Basis vergangener Daten zu trainieren, nutzt ihre Methode mathematische Simulation, um den besten Zug in Echtzeit zu ermitteln.

Letztendlich legt das Paper nahe, dass „Lookahead Branching“ eine leistungsstarke, allgemeine Strategie ist, die in verschiedene Verifizierungswerkzeuge eingesteckt werden kann, um sie intelligenter und schneller zu machen. Es ersetzt die bestehenden Werkzeuge nicht, sondern erweitert sie, sodass sie schwierigere sicherheitskritische Probleme mit größerer Zuversicht bewältigen können. Die Ergebnisse legen nahe, dass es für die schwierigsten Verifizierungsaufgaben den Aufwand wert ist, Zeit in das Vorausschauen zu investieren, was zu einem robusteren und zuverlässigeren Weg führt, um sicherzustellen, dass unsere KI-Systeme sicher sind.