Branch and Bound for Relational Verification of Neural Networks

Technische Samenvatting: Branch and Bound voor Relationele Verificatie van Neurale Netwerken (SABRE)

Probleemstelling
Het artikel behandelt de uitdaging van het verifiëren van neurale netwerken tegen relationele specificaties, specifiek globale robuustheid. In tegenstelling tot lokale robuustheid, die ervoor zorgt dat de output van een netwerk stabiel blijft onder kleine perturbaties van een enkele input, vereist globale robuustheid het redeneren over de relatie tussen meerdere netwerkinferenties. Formeel gezien is een netwerk globaal robuust als, voor elke twee inputs binnen een begrensde afstand $\epsilon$, het verschil in hun outputs begrensd is door $\delta$.

Bestaande benaderingen voor relationele verificatie vertrouwen primair op sound over-approximation technieken (bijv. RaVeN) met behulp van convexe domeinen om de verschillen tussen netwerkoutputs te begrenzen. Hoewel deze methoden efficiënt zijn, zijn ze inherent incompleet en gevoelig voor het genereren van false alarms (spuriële tegenvoorbeelden) vanwege de ruwheid van de benaderingen. Hoewel Branch and Bound (BaB) een standaardtechniek is voor het verfijnen van benaderingen bij lokale robuustheid door individuele neuronen te splitsen, is de toepassing ervan op relationele verificatie beperkt gebleven. Eerdere pogingen (bijv. RABBit) pasten BaB toe op relationele problemen door individuele neuronen te splitsen, wat de auteurs naar verluidt faalt in het exploiteren van de specifieke structuur van relationele restricties en kan leiden tot suboptimale verfijning.

Methodologie: Het SABRE-framework
De auteurs stellen SABRE (Splitting Approximated Bounds for RElational verification) voor, een Branch and Bound-framework dat specifiek is ontworpen voor relationele verificatie. De kerninnovatie ligt in het verschuiven van de splitsingsstrategie van individuele neuronen naar relationele neuronen.

1. Relationele Neuronen en Probleemsplitsing:

   • Het framework modelleert het verschil tussen twee netwerkinferenties met behulp van relationele neuronen ($\Delta y^{(i)}_j = y^{(i)}_j - \hat{y}^{(i)}_j$), die het verschil vertegenwoordigen tussen overeenkomstige neuronen in twee parallelle kopieën van het netwerk.
   • In plaats van te splitsen op basis van de activatietoestand van een individueel neuron (bijv. $x > 0$ versus $x < 0$), splitst SABRE op basis van het teken van de input van het relationele neuron ($\Delta x^{(i)}_j \geq 0$ versus $\Delta x^{(i)}_j \leq 0$).
   • Deze aanpak richt zich direct op de onzekerheid in het verschil tussen outputs, met als doel de grenzen van het relationele verschil effectiever aan te scherpen dan door individuele componenten te splitsen.

2. Dual-Based Neuron Selectiestrategie:

   • Een cruciale factor in de efficiëntie van BaB is het selecteren van welk neuron op elk punt gesplitst wordt. Om de computationele kosten van het oplossen van subproblemen voor het schatten van de impact te vermijden, gebruikt SABRE een Lagrangiaanse duale formulering van het verificatieprobleem.
   • De auteurs afleiden een duaal probleem waarbij de doelfunctie een sommatie is van neuron-specifieke termen. Deze termen vangen de bijdrage van specifieke neuronen aan de uiteindelijke outputgrens onder lineaire relaxatie op.
   • Door te analyseren hoe het splitsen van een specifiek relationeel neuron de coëfficiënten in de duale doelfunctie beïnvloedt, kan SABRE de potentiële verfijning (het aanscherpen van grenzen) efficiënt schatten zonder de subproblemen daadwerkelijk op te lossen. Het algoritme selecteert het relationele neuron dat de geschatte verbetering maximaliseert.

3. Workflow:

   • Het proces begint met een benaderingsverifieerder (bijv. RaVeN) om de globale robuustheidseigenschap te controleren.
   • Als er een false alarm wordt gedetecteerd, selecteert het algoritme een relationeel neuron met behulp van de dual-based strategie.
   • Het probleem wordt in twee subproblemen gesplitst door restricties toe te voegen aan de geselecteerde input van het relationele neuron.
   • Dit recursieve proces gaat door totdat alle subproblemen zijn geverifieerd of er een echt tegenvoorbeeld is gevonden.

Belangrijkste Bijdragen

• Nieuwe Splitsingsstrategie: Het artikel introduceert een BaB-framework dat prioriteit geeft aan het splitsen van relationele neuronen in plaats van individuele neuronen, met het argument dat dit direct de bron van de benaderingsfout in relationele specificaties aanpakt.
• Dual-Based Selectieheuristiek: De auteurs breiden de duale formulering benadering (voorheen gebruikt voor lokale robuustheid) uit naar de relationele setting, wat een efficiënte, datagedreven selectie van het meest impactvolle relationele neuron mogelijk maakt om te splitsen.
• SABRE Implementatie: Een volledig verificatieframework dat deze strategieën integreert en in staat is om globale robuustheidseigenschappen over diverse netwerkarchitecturen aan te pakken.

Experimentele Resultaten
De auteurs hebben SABRE geëvalueerd op 817 verificatie-instanties verspreid over vijf datasets: ACAS Xu, MNIST-F, MNIST-C, CIFAR en GTSRB. De evaluatie vergeleek SABRE met:

• RaVeN: Een state-of-the-art benaderingsverifieerder zonder verfijning.
• ClasIS & DualIS: Varianten van BaB die individuele neuronen splitsen (ClasIS gebruikt standaard selectie; DualIS gebruikt de voorgestelde duale formulering maar toegepast op individuele neuronen).
• RandRS: Een variant van SABRE die gebruikmaakt van willekeurige neuronselectie.

Belangrijkste Bevindingen:

• Prestaties vs. RaVeN: SABRE presteerde aanzienlijk beter dan RaVeN en loste een substantieel groter aantal instanties op door effectief benaderingen te verfijnen die RaVeN niet kon verifiëren.
• Relationele vs. Individuele Splitsing: Op de meeste benchmarks (ACAS Xu, MNIST-F, MNIST-C, GTSRB) loste SABRE (relationele splitsing) meer instanties op, verkende minder subproblemen en had minder tijd nodig dan individuele splitsingsmethoden (ClasIS, DualIS).
  • Opmerking over CIFAR: Op de CIFAR-dataset met kleine perturbatieradii ($\epsilon$) presteerden individuele splitsingsmethoden aanvankelijk beter dan SABRE. De auteurs schrijven dit toe aan het hoge aantal instabiele ReLU's in CIFAR-modellen, wat de lokale impact van relationele splitsen verwatert. Echter, naarmate $\epsilon$ toenam, werd relationele splitsing effectiever.
• Selectiestrategie: De dual-based selectiestrategie (SABRE) presteerde aanzienlijk beter dan willekeurige selectie (RandRS) over alle datasets, waarbij het aantal subproblemen en de verificatietijd in veel gevallen met ongeveer 50% werd verminderd.
• Maximale Verifieerbare Perturbatie: SABRE certificeerde consistent grotere perturbatiegebieden ($\epsilon^*$) dan de baseline-methoden, met name op ACAS Xu en MNIST-F, waar het vaak slaagde in het vinden van niet-triviale grenzen terwijl andere methoden er niet in slaagden ook maar iets te certificeren.

Betekenis en Claims
Het artikel claimt dat SABRE een belangrijke stap voorwaarts is in relationele verificatie door aan te tonen dat het splitsen van relationele neuronen een effectievere strategie is voor het verfijnen van benaderingen in globale robuustheidsverificatie dan het splitsen van individuele neuronen. De auteurs benadrukken dat hun dual-based selectiestrategie betrouwbare sturing biedt voor het prioriteren van splitsingen, wat leidt tot verbeterde verificatie-efficiëntie en schaalbaarheid.

Het werk benadrukt dat hoewel de aanpak incompleet blijft (vanwege de aard van de benadering), de voorgestelde technieken de mate van verfijning per split maximaliseren, waardoor de formele verificatie van relationele eigenschappen praktischer wordt voor veiligheidskritische cyber-fysieke systemen. De auteurs merken bescheiden op dat toekomstig werk hybride strategieën kan verkennen die dynamisch schakelen tussen individuele en relationele splitsing, maar zij stellen dat hun huidige exclusieve focus op relationele neuronen al superieure prestaties oplevert op de meerderheid van de geteste benchmarks.