Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing

Dit artikel introduceert RobLight, een tool die de structurele robuustheid van Graph Neural Networks verbetert door krachtige solvers te vervangen door efficiënte, polynomiale partiële solvers voor het oplossen van satisfiability-problemen.

De kern

Titel: Hoe we Graph Neural Networks (GNN's) veilig maken met een slimme "snuffelhond" in plaats van een zware "tank"

Stel je voor dat je een zeer slimme, maar kwetsbare detective hebt die foto's van sociale netwerken bekijkt om te bepalen of iemand een crimineel is. Deze detective is een Graph Neural Network (GNN). Hij kijkt niet alleen naar de mensen (de knopen), maar vooral naar wie met wie bevriend is (de lijntjes).

Het probleem? Een slimme hacker kan de detective gek maken door heel kleine veranderingen aan te brengen in het netwerk. Bijvoorbeeld: "Ik maak even alsof deze twee mensen vrienden zijn, terwijl ze dat niet zijn." Als de detective hierdoor van mening verandert, is hij niet robuust (veilig).

Vroeger probeerden wetenschappers te bewijzen dat zo'n detective veilig was door een enorme, zware machine (een "MIP-solver") te gebruiken. Dit was alsof je een hele tank inzet om te controleren of een muis in een doosje zit. Het werkt, maar het is traag, duur en kan alleen kleine doosjes aan.

De auteurs van dit paper hebben een nieuw idee bedacht: RobLight. In plaats van de zware tank, gebruiken ze een lichtgewicht, snelle "snuffelhond" die slim zoekt.

Hier is hoe het werkt, vertaald naar alledaagse taal:

1. Het Probleem: De "Wat als?"-Vraag

Stel je een netwerk voor als een grote stad met wegen. De detective kijkt naar een specifieke persoon. De vraag is: "Als een hacker maximaal 5 wegen kan veranderen (wegmaken of aanleggen), kan hij de detective dan zover krijgen om die persoon als 'goed' te bestempelen, terwijl hij eigenlijk 'slecht' is?"

Om dit te beantwoorden, moet je eigenlijk alle mogelijke versies van die stad uitproberen. Maar dat zijn er miljarden. Dat is waarom de oude methoden (de tanks) vastliepen; ze probeerden alles systematisch af te rekenen en werden snel moe.

2. De Oplossing: De Slimme Snuffelhond (RobLight)

De auteurs zeggen: "Waarom proberen we niet eerst te snuffelen?"

In plaats van elke mogelijke stad te bouwen en te testen, gebruiken ze een lichtgewicht test (een "partial oracle"). Dit is als een snuffelhond die zegt:

• "JA": "Ik ruik zeker dat er een hack mogelijk is!" (Dan stoppen we, de detective is niet veilig).
• "NEE": "Ik ruik zeker dat er geen hack mogelijk is, zelfs niet als je alles probeert." (Dan is de detective veilig).
• "IK WEET HET NIET": "Ik ruik iets, maar ik ben niet zeker. Laten we dan een stapje verder gaan."

De magie zit hem in het feit dat deze hond snel is. Hij kan in een fractie van een seconde zeggen "Nee" of "Ja" voor de meeste situaties. Alleen als hij twijfelt, moet hij een stapje dieper graven.

3. De Slimme Trucs (Optimalisaties)

De auteurs hebben de snuffelhond nog slimmer gemaakt met een paar trucs:

• De "Wat is er veranderd?"-Truc (Incrementele Berekening):
  Stel je voor dat je een legpuzzel hebt. Als je één stukje verplaatst, hoef je niet de hele puzzel opnieuw te maken. Je kijkt alleen naar de stukjes die eromheen liggen. RobLight doet precies dit. Als een hacker één lijn verandert, berekent de tool alleen de impact op de directe buren, niet op het hele netwerk. Dit bespaart enorm veel tijd.

• De "Vooruitkijken"-Truc (Operator Reordering):
  Soms is het slimmer om eerst te rekenen en dan te groeperen, in plaats van andersom. Stel je voor dat je een groep mensen moet tellen. Als je eerst hun gewichten optelt en dan vermenigvuldigt, krijg je een ruwe schatting. Maar als je eerst vermenigvuldigt en dan optelt, krijg je een veel nauwkeurigere schatting. RobLight doet dit slimme rekenen, waardoor hij sneller kan zeggen: "Nee, zelfs in het slechtste geval is de detective veilig."

• De "Budget"-Truc:
  De hacker heeft een beperkt budget (bijv. maar 5 veranderingen). De tool gebruikt dit om te weten dat bepaalde veranderingen onmogelijk zijn. Als de hacker al 5 veranderingen heeft gedaan, kan hij er geen 6e doen. De tool gebruikt deze grenzen om de zoekruimte drastisch te verkleinen.

4. Het Resultaat: Snelheid en Kracht

In de experimenten hebben ze getest of hun nieuwe tool (RobLight) beter werkt dan de oude zware methoden.

• Snelheid: RobLight is tien keer tot honderd keer sneller.
• Kracht: Waar de oude methoden vastliepen bij netwerken met 3 lagen, kan RobLight probleemloos netwerken met 4 lagen (en soms meer) aan.
• Breedte: Het werkt voor verschillende soorten netwerken en verschillende soorten "hacks" (verwijderingen of toevoegingen van lijntjes).

Conclusie

Dit paper laat zien dat je niet altijd de zwaarste wapens nodig hebt om een probleem op te lossen. Door slim te zoeken, te snuffelen en slimme trucs te gebruiken, kun je veel sneller en efficiënter bewijzen dat een kunstmatige intelligentie veilig is tegen manipulatie.

Het is alsof je in plaats van een hele legermacht te sturen om een huis te zoeken, gewoon een slimme hond stuurt die de meeste deuren al open weet te vinden voordat je überhaupt de sleutel hebt gepakt. Voor de veiligheid van AI in de echte wereld (zoals in ziekenhuizen of financiële systemen) is dit een enorme stap voorwaarts.

Technische samenvatting

Probleemstelling

Graph Neural Networks (GNN's) zijn de dominante architectuur voor leren op grafen, maar ze zijn kwetsbaar voor adversariale aanvallen. Een dergelijke aanval omvat kleine verstoringen in de invoer (bijvoorbeeld het toevoegen of verwijderen van randen in de grafstructuur) die leiden tot een verkeerde classificatie door het model.

Het probleem van robustheidsverificatie bestaat erin te garanderen dat de classificatie van een GNN onveranderd blijft binnen een bepaald "verstooringsbudget" (bijvoorbeeld maximaal $\Delta$ randen die kunnen worden gewijzigd).

• Huidige uitdaging: Bestaande state-of-the-art technieken reduceren dit probleem vaak tot Mixed Integer Programming (MIP) of andere zware constraint solving-problemen. Deze methoden zijn NP-compleet en schalen slecht; ze zijn momenteel beperkt tot zeer kleine GNN's (meestal maximaal 3 lagen) en kleine datasets.
• Specifiek voor GNN's: In tegenstelling tot beeldherkenning (waar alleen pixelwaarden veranderen), veranderen bij GNN's de structuur van de graf (randen), wat de zoekruimte exponentieel vergroot en de toepassing van generieke solvers inefficiënt maakt.

Methodologie

De auteurs introduceren RobLight, een tool die de robustheidsverificatie benadert door in plaats van zware, complete solvers, gebruik te maken van lichtgewicht, partiële orakels (partial oracles) binnen een diepte-eerst zoekalgoritme (DFS).

De kern van de methode bestaat uit de volgende componenten:

1. Onvolledige Grafen en Refinement:

   • Het probleem wordt gemodelleerd met behulp van "onvolledige grafen" (incomplete graphs), waarbij randen als "bekend", "onbekend" of "niet-bestaand" worden gemarkeerd.
   • Het algoritme doorzoekt de ruimte van mogelijke voltooide grafen (completions) die binnen het verstooringsbudget vallen.

2. Partiële Orakels (Partial Oracles):

   • In plaats van een volledige MIP-oplosser te gebruiken, gebruikt RobLight een partiële orakel dat drie uitkomsten kan geven: SAT (er bestaat een aanval), UNSAT (geen aanval mogelijk), of UNKNOWN (onbepaald).
   • Als het orakel "UNKNOWN" retourneert, splitst het algoritme de zoekruimte verder op door een onbekende rand te fixeren (als bestaand of niet-bestaand) en recursief verder te zoeken.
   • Het orakel bestaat uit twee onderdelen:
     • Non-robustness tester: Controleert of de "gronding" (de voltooiing die het dichtst bij de originele graf ligt) al een aanval vertoont.
     • Bound propagator: Berekent boven- en ondergrenzen voor de features van de GNN op basis van de onvolledige graf. Als de ondergrens van de juiste klasse lager is dan de bovengrens van een andere klasse, is de robustheid bewezen (UNSAT).

3. Optimalisatiestrategieën:
   Om de efficiëntie te maximaliseren, worden diverse optimalisaties toegepast:

   • Incrementele berekening: Bij het wijzigen van een rand worden alleen de features en grenzen van de beïnvloede knoppen en hun buren opnieuw berekend, in plaats van de hele graf.
   • Operator herordening: Voor aggregatiefuncties (zoals som of gemiddelde) wordt de volgorde van matrixvermenigvuldiging en aggregatie omgewisseld. Dit leidt tot strakkere (smallere) grenzen, waardoor het orakel vaker "UNSAT" kan teruggeven.
   • Budget-aware bound tightening: De beperkingen van het verstooringsbudget (globaal en lokaal) worden expliciet gebruikt om de berekende grenzen te verscherpen.
   • Heuristieken voor randkeuze: Het algoritme kiest eerst de onbekende randen die het dichtst bij het doelwit (de te classificeren knoop) liggen, omdat deze de grootste impact hebben op de uiteindelijke uitkomst.

Belangrijkste Bijdragen

1. Paradigmaverschuiving: Het paper toont aan dat het vervangen van zware, generieke solvers (zoals Gurobi voor MIP) door efficiënte, gespecialiseerde partiële orakels een significant betere prestatie oplevert voor GNN-robustheid.
2. Schalbaarheid: De methode is in staat om GNN's met 4 lagen te verifiëren, wat verder gaat dan wat eerdere state-of-the-art tools (beperkt tot 3 lagen) aankunnen.
3. Flexibiliteit: RobLight ondersteunt verschillende aggregatiefuncties (som, maximum, gemiddelde), gerichte en ongerichte grafen, en zowel deletie- als insertie-aanvallen.
4. Open Source: De tool en de datasets zijn beschikbaar gesteld voor replicatie.

Resultaten

De auteurs hebben RobLight geëvalueerd op diverse benchmarks (Cora, CiteSeer, Cornell, Texas, Wisconsin voor knoopclassificatie; MUTAG en ENZYMES voor grafclassificatie) en vergeleken met de state-of-the-art tools SCIP-MPNN en GNNev.

• Prestatie: RobLight presteert meer dan een orde van grootte sneller dan de concurrenten.
  • Bijvoorbeeld op het Cora-dataset met een som-aggregatie: RobLight loste 10.832 instanties op met een gemiddelde tijd van 0,36 seconden, terwijl SCIP-MPNN 53,63 seconden nodig had en GNNev 27,13 seconden.
• Diepte: RobLight kon consistent 4-laagse netwerken verifiëren, terwijl de concurrenten vaak time-out gaven of slechts tot 3 lagen konden gaan.
• Robustheid vs. Non-robustheid: Voor niet-robuste instanties (waar een aanval bestaat) is RobLight extreem snel omdat het partiële orakel snel een tegenvoorbeeld vindt. Voor robuuste instanties is de zoekruimte groter, maar de optimalisaties zorgen ervoor dat de exploratie-ratio (het aantal benodigde recursieve calls) laag blijft.
• Robustheidsstraal: De tool kan ook de exacte "robustheidsstraal" (het maximale budget waarbij het model nog robuust is) berekenen, iets wat eerdere tools niet konden doen voor deze complexiteit.

Beteekenis en Conclusie

Dit werk is significant omdat het aantoont dat voor specifieke problemen in de verificatie van neurale netwerken, heuristic search in combinatie met lichtgewicht solvers superieur kan zijn aan het gebruik van krachtige, generieke NP-hard solvers.

De auteurs concluderen dat bestaande solvers (zoals MIP-solvers) de inherente structuur van het GNN-robustheidsprobleem niet optimaal kunnen benutten. Door de zoekstrategie en de orakels direct te laten profiteren van de grafstructuur en de eigenschappen van de GNN (zoals aggregatiemechanismen), kan de verificatie veel efficiënter worden uitgevoerd. Dit opent de deur voor robuustheidsverificatie in grotere en complexere grafische modellen, wat essentieel is voor de veilige toepassing van GNN's in kritieke domeinen zoals de levenswetenschappen.