Stel je een wereld voor waarin de "hersenen" van onze auto's, medische apparaten en beveiligingssystemen bestaan uit gigantische, complexe webben van wiskunde die neurale netwerken worden genoemd. Deze digitale hersenen zijn ongelooflijk goed in het herkennen van gezichten of het voorspellen van het weer, maar ze zijn ook berucht moeilijk te begrijpen. Omdat ze leren door patronen in gegevens te vinden in plaats van strikte, geschreven regels te volgen, is het moeilijk om zeker te weten of ze een fout zullen maken wanneer de situatie vreemd wordt. Dit is een groot probleem voor de veiligheid: als het brein van een zelfrijdende auto een slechte gok maakt, kunnen mensen gewond raken. Dus heeft een groep wetenschappers gewerkt aan een manier om wiskundig te bewijzen dat deze netwerken altijd correct zullen reageren, ongeacht welke input ze krijgen. Denk bij dit proces aan een detective die probeert een enorme mysteries op te lossen door elke mogelijke aanwijzing te controleren. De detective moet het mysterie opdelen in steeds kleinere stukjes en elk stukje controleren om te zien of het tot een tegenstrijdigheid (een "bug") of een veilige uitkomst leidt. De uitdaging is dat er zoveel mogelijke aanwijzingen zijn dat het controleren van ze allemaal één voor één langer zou duren dan het begin van het universum. De detective heeft een slimme strategie nodig om te beslissen welke aanwijzing hij als volgende moet controleren, in de hoop dat één keuze het hele puzzel snel oplost.

Dit artikel introduceert een slimme nieuwe strategie voor die detective, genaamd "Lookahead Branching". De onderzoekers, werkend met twee verschillende soorten verificatietools (één genaamd Marabou en een andere genaamd α-β-CROWN), ontdekten dat in plaats van alleen te gokken welke aanwijzing ze nu moeten controleren op basis van wat er op dit moment gebeurt, de detective even moet pauzeren en een paar stappen in de toekomst moet simuleren. Stel je voor dat je een schaakspel speelt. Een standaardspeler kan naar het bord kijken en de zet kiezen die er op dit moment het beste uitziet. Maar een grootmeester kan denken: "Als ik hierheen beweeg, beweegt mijn tegenstander daarheen, en dan kan ik daarheen bewegen..." De auteurs suggereren dat neurale netwerk-verifieerders hetzelfde moeten doen: voordat ze een beslissing nemen, moeten ze kort even "dromen" over wat er zou gebeiden als ze verschillende paden zouden bewandelen. Ze ontdekten dat door een beetje extra tijd te besteden aan het simuleren van deze toekomstige stappen, de verifieerder betere keuzes kan maken, wat leidt tot snellere oplossingen en het oplossen van meer problemen dan voorheen. In hun tests hielp deze aanpak de tools om tot 57% meer instanties op te lossen en maakte het hen aanzienlijk sneller, vooral bij de moeilijkste problemen.

De kern van het artikel gaat over hoe je dit "dromen" efficiënt aanpakt. De onderzoekers hebben een algemeen recept gemaakt dat aan elk van deze verificatietools kan worden toegevoegd. Het proces werkt als volgt: wanneer de tool een probleem moet opsplitsen, kiest hij niet zomaar één optie. In plaats daarvan kiest hij een paar veelbelovende kandidaten en simuleert hij het opsplitsen op elk van hen. Hij kijkt een paar stappen vooruit (de "lookahead depth") om te zien hoe het probleem verandert. Als een splitsing leidt tot een situatie waarin veel andere verwarrende delen van het netwerk plotseling duidelijk worden (zoals een neuron dat "onstabiel" was plotseling "vastgelegd" wordt), krijgt die splitsing een hoge score. De tool kiest vervolgens de splitsing met de hoogste score.

De auteurs ontdekten ook dat deze simulatie niet alleen dient voor het kiezen van het beste pad; het kan ook nieuwe feiten vinden. Soms, door een splitsing te simuleren, realiseert de tool zich dat een bepaald deel van het netwerk moet in een specifieke staat zijn, nog voordat hij die splitsing officieel uitvoert. Dit stelt de tool in staat om die delen van het netwerk direct te "fixen", waardoor enorme hoeveelheden onnodig werk worden overgeslagen. Het artikel laat zien dat dit goed werkt in twee zeer verschillende soorten verificatietools: één die draait op standaard computermprocessoren (Marabou) en een andere die gebruikmaakt van krachtige grafische kaarten (α-β-CROWN).

In hun experimenten testte het team deze methode op een verscheidenheid aan neurale netwerken, van eenvoudige netwerken die handgeschreven cijfers herkennen tot complexe netwerken die worden gebruikt in computer vision. Bij de Marabou-tool hielp het gebruik van lookahead om meer problemen op te lossen en verminderde het de tijd die nodig is voor moeilijke gevallen. Bijvoorbeeld, op een specifieke set benchmarks genaamd NN4Sys, loste de tool meer instanties op met lookahead dan zonder. Bij de α-β-CROWN-tool, die bekend staat om zijn snelheid, slaagde de lookahead-strategie er nog steeds in om de oplostijd te verkorten en een paar extra problemen op te lossen die de standaardmethode miste. De onderzoekers merkten op dat hoewel het gebruiken van lookahead een klein beetje extra tijd kost om op te zetten, de beloning enorm is omdat het de verifieerder voorkomt om later tijd te verspillen aan slechte paden.

Het artikel wijst echter voorzichtig op het punt dat dit geen wondermiddel is dat alles direct oplost. Het "lookahead"-proces is computationeel duur, wat betekent dat het meer computerkracht gebruikt om vooruit te denken. De auteurs ontdekten dat het het beste werkt wanneer het aan het begin van de zoektocht wordt gebruikt, waar de beslissingen de grootste impact hebben op de toekomst. Als je probeert het voor elke stap te gebruiken, kan de kosten van het vooruitdenken zwaarder wegen dan de voordelen. Ze testten ook verschillende manieren om de lookahead in te richten, zoals hoeveel stappen er vooruit gekeken moet worden en hoeveel kandidaten er gesimuleerd moeten worden, en vonden dat een matige diepte (twee stappen vooruit kijken) goed werkte voor de moeilijkste problemen.

Het artikel voert expliciet een argument tegen het idee dat we alleen snelle, lokale informatie moeten gebruiken om beslissingen te nemen. Hoewel snelle heuristieken (vuistregels) goed zijn voor de snelheid, missen ze vaak het grotere plaatje en kunnen ze de verifieerder in een doodlopende weg leiden. De auteurs laten zien dat door een beetje meer inspanning vooraf te investeren om de gevolgen van een splitsing te simuleren, het algemene verificatieproces veel efficiënter wordt. Ze verduidelijken ook dat hun methode verschilt van het gebruiken van kunstmatige intelligentie om te leren hoe te brancheren; in plaats van een model te trainen op historische gegevens, gebruikt hun methode wiskundige simulatie om in realtime de beste zet te bepalen.

Uiteindelijk suggereert het artikel dat "Lookahead Branching" een krachtige, algemene strategie is die in verschillende verificatietools kan worden geplaatst om ze slimmer en sneller te maken. Het vervangt de bestaande tools niet, maar versterkt ze, waardoor ze met meer vertrouwen moeilijkere, veiligheidskritische problemen kunnen aanpakken. De resultaten suggereren dat voor de meest moeilijke verificatietaken, het nemen van de tijd om vooruit te kijken de extra computationele kosten waard is, wat leidt tot een robuustere en betrouwbaardere manier om te garanderen dat onze AI-systemen veilig zijn.