Technische Samenvatting: Veriphi – Attack-Guided Neural Network Verification met Dataset-Afhankelijke Trainingsmethoden

1. Probleemstelling

De inzet van deep learning in veiligheidskritische domeinen vereist robuuste verificatie van neurale netwerken. Hoewel adversariële training (bijv. PGD) empirische robuustheid biedt, ontbreken formele garanties. Daarentegen bieden gecertificeerde trainingsmethoden (bijv. Interval Bound Propagation, IBP) wiskundige bewijzen van robuustheid, maar hebben zij vaak moeite met schaalbaarheid en nauwkeurigheid bij complexe datasets.

Er bestaat een kritische kloof in de literatuur met betrekking tot methode-selectie: praktijkgebruikers missen sturing over of zij prioriteit moeten geven aan gecertificeerde training of aan adversariële training voor specifieke probleemcontexten. Bovendien kampen bestaande verificatie-instrumenten vaak met uitdagingen bij het balanceren van computationele efficiëntie met de noodzaak van formele grenzen, met name bij het opschalen van academische benchmarks naar modellen van productieformaat.

2. Methodologie: Het Veriphi-framework

De auteurs presenteren Veriphi, een GPU-versneld verificatiesysteem dat deze uitdagingen aanpakt via een tweefasige strategie en een systematische evaluatie van trainingsmethodologieën.

2.1 Verificatiearchitectuur

Veriphi maakt gebruik van een attack-guided verificatiestrategie bestaande uit twee fasen:

1. Fast Falsification (Fase 1): Het systeem probeert eerst tegenvoorbeelden te vinden met behulp van snelle adversariële aanvallen (FGSM en I-FGSM) met een configureerbare timeout (standaard 10s). Als een aanval erin slaagt de output van het netwerk te falsificeren, wordt het proces onmiddellijk beëindigd met een "FALSIFIED"-resultaat, waardoor de dure formele verificatie wordt overgeslagen.
2. Formele Verificatie (Fase 2): Als de aanvalsfase er niet in slaagt een tegenvoorbeeld te vinden, roept het systeem het $\alpha, \beta$-CROWN framework aan (via de auto-LiRPA bibliotheek) om gecertificeerde grenzen te berekenen. Een netwerk wordt geverifieerd als de ondergrens van de ware klasse de bovengrenzen van alle andere klassen overstijgt binnen de perturbatiebudget $\epsilon$ in de $L_\infty$-norm.

2.2 Trainingsmethodologieën

De studie vergelijkt systematisch drie benaderingen van training:

• Baseline: Standaard cross-entropy minimalisatie.
• PGD Adversarial Training: Optimaliseert de worst-case loss over een perturbatiebudget met behulp van Projected Gradient Descent.
• IBP Certified Training: Optimaliseert een convexe buitenste grens van de loss met behulp van Interval Bound Propagation, met een weegfactor $\kappa$ die tijdens de training lineair toeneemt.

2.3 Modelarchitectuur en Experimentele Opstelling

De experimenten maken gebruik van Tiny Recursive Models (TRM-MLP), een verificatievriendelijke architectuur met ReLU-activaties en lineaire operaties zonder batch normalisatie.

• Datasets: MNIST (eenvoudig, 784 dimensies) en CIFAR-10 (complex, 3.072 dimensies).
• Productieschaal: Een reëel probleem in de luchtvaartlogistiek (Airbus Beluga) waarbij een model met 105,8 miljoen parameters betrokken is.
• Hardware: VSC-5 supercomputer met dual A100 GPU's.

3. Belangrijkste Resultaten

3.1 Effectiviteit van Dataset-Afhankelijke Training

De belangrijkste bevinding is dat de effectiviteit van trainingsmethoden fundamenteel afhankelijk is van de datasetcomplexiteit:

• Eenvoudige Datasets (MNIST): IBP gecertificeerde training presteert aanzienlijk beter dan adversariële training. Bij $\epsilon = 0,06$ bereikt IBP een 7er 7% geverifieerde nauwkeurigheid vergeleken met 63% voor PGD.
• Complexe Datasets (CIFAR-10): IBP-training slaagt er niet in om betekenisvolle certificering te bieden, met slechts 1% geverifieerde nauwkeurigheid bij $\epsilon \geq 0,006$, terwijl PGD adversariële training een hoge prestatie behoudt (58–94%).
• Interpretatie: De auteurs schrijven het falen van IBP op CIFAR-10 toe aan de accumulatie van over-approximatiefouten in intervalrekening naarmate de inputdimensie toeneemt (van 784 naar 3.072), wat leidt tot vacuüm grenzen. PGD, die empirisch is, blijft robuust tegen deze toename in dimensionaliteit.

3.2 Verificatie-efficiëntie

De attack-guided benadering levert substantiële versnellingen op:

• 5,5× GPU Versnelling: Door kwetsbare samples vroegtijdig te falsificeren (in <0,1s), vermindert het systeem de gemiddelde verificatietijd van 1,21s (zuivere formele verificatie) naar 0,22s.
• Vroegtijdige Beëindiging: Op MNIST met $\epsilon=0,1$ falsificeren aanvallen 40% van de samples succesvol, waardoor de formele verificatie volledig wordt vermeden voor die gevallen.

3.3 Vergelijking van Grensmethoden

Een vergelijking tussen CROWN, $\alpha$-CROWN en $\beta$-CROWN laat afnemende meeropbrengsten zien:

• Strakkere grenzen ($\alpha, \beta$-CROWN) bieden minder dan 5% verbetering in geverifieerde nauwkeurigheid ten opzichte van standaard CROWN.
• Deze verbetering gaat gepaard met een 20–30% toename in computationele tijd, wat suggereert dat standaard CROWN de beste balans biedt tussen nauwkeurigheid en efficiëntie voor praktische toepassingen.

3.4 Validatie op Productieschaal

Veriphi is succesvol geschaald naar een 105,8M parameter model voor de Airbus Beluga luchtvaartlogistiek.

• Het systeem verifieerde de naleving van beperkingen (vliegcapaciteit, rakencapaciteit, temporele beperkingen) onder 5% parameter-perturbaties.
• Het bereikte een geverifieerde robuustheidspercentage van 40% op gesamplede problemen met een gemiddelde verificatietijd van 2,6 seconden per probleem, wat de toepasbaarheid buiten academische benchmarks aantoont.

4. Betekenis en Claims

Het artikel beweert de heersende aanname uit te dagen dat gecertificeerde training universeel beter presteert dan adversariële training. In plaats daarvan stelt het dat context cruciaal is:

• Voor eenvoudige, laag-dimensionale datasets: Is gecertificeerde training (IBP) superieur voor het bereiken van verifieerbare robuustheid.
• Voor complexe, hoog-dimensionale datasets: Is adversariële training (PGD) effectiever voor het bereiken van betekenisvolle certificeringspercentages, aangezien IBP-grenzen te ruim worden om nuttig te zijn.

De auteurs benadrukken dat hun werk de eerste systematische vergelijking biedt die datasetcomplexiteit als een primaire factor voor methode-selectie vaststelt. Daarnaast biedt de integratie van attack-guided falsificatie met formele verificatie een praktisch pad naar het schalen van verificatie naar productiemodellen van omvang, waarmee de kloof tussen theoretische garanties en echte inzet in de veiligheidskritische luchtvaartlogistiek wordt overbrugd.

Het artikel concludeert dat hoewel strakkere grenzen ($\alpha, \beta$-CROWN) marginale winst bieden, de combinatie van empirische robuustheid (PGD) met selectieve certificering op laag-dimensionale subruimtes de meest praktische toekomstige richting kan vertegenwoordigen, een hypothese die openstaat voor toekomstig onderzoek.