Technische Samenvatting: Stress-testen van neurale netwerkverificatoren met wiskundig bewezen robuuste instanties

Probleemstelling

Neurale netwerkverificatoren zijn ontworpen om formele garanties te bieden voor modelgedrag, specifiek door te certificeren dat een getraind model robuust reageert op beperkte invoerverstoringen. De evaluatie van deze verificatoren is echter fundamenteel beperkt door het ontbreken van ground-truth labels in bestaande benchmarks. Zonder a priori te weten of een verificatie-instantie werkelijk robuust of niet-robuust is, steunt de evaluatie op indirecte heuristieken, zoals meerderheidsstemming tussen verificatoren of het aannemen van correctheid wanneer geen tegenvoorbeeld wordt gevonden. Deze aanpak verhindert exacte scoring, verduistert specifieke faalmodi en maakt het moeilijk om verificatoren systematisch te stress-testen op steeds moeilijkere instanties. Bovendien bieden huidige benchmarks beperkte diagnostische informatie over waarom een verificator faalt (bijvoorbeeld door losse relaxaties, complexe lokale geometrie of numerieke problemen).

Methodologie

De auteurs introduceren VeriStress-GT (Verifier Stress-Testing via Ground Truth), een modulair framework voor het genereren van neurale netwerkverificatie-instanties met analytisch bewezen ground-truth robuustheidslabels. In tegenstelling tot traditionele benchmarks die vertrouwen op het trainen van modellen op datasets, construeert VeriStress-GT instanties waarbij robuustheid gegarandeerd is door wiskundige constructie.

1. Robuuste Constructies

Het framework definieert een verzameling "constructors", elk gericht op specifieke architecturale klassen of knelpunten van verificatoren. Deze constructors genereren instanties waarbij het ground-truth label a priori bekend is:

• ReLU-netwerkconstructors:
  • Exact-Radius via MILP: Berekent de exacte robuustheidsstraal met behulp van Mixed-Integer Linear Programming om robuuste instanties nabij de grens te creëren.
  • Constant-on-Box Embedding: Construeert netwerken waarbij een tussenliggende latente laag constant is over de verstoringset, waardoor robuustheid gegarandeerd is ongeacht de complexiteit stroomafwaarts.
  • Mutually Exclusive Activation Patterns (MEAP): Creëert paren neuronen die individueel instabiel zijn (schakelen tussen actief/inactief) maar zo gekoppeld dat er altijd minstens één actief is, waardoor verificatoren gedwongen worden complexe afhankelijkheden van activatiepatronen te hanteren.
  • Input-Corner Stress: Genereert instanties waarbij robuustheid afhankelijk is van de convexiteit van de margefunctie, wat verificatie vereist op de hoekpunten van de verstoringbox in plaats van via lokale relaxaties.
• CNN-constructors:
  • Deep Contractive CNN: Dwingt verstoringen om door diepte te contracteren met behulp van Lipschitz-beperkte convolutieblokken.
  • Paired-Bias CNN: Een convolutie-anaaloog van MEAP, waarbij gepaarde kanalen dezelfde filters delen maar geordende biases hebben, waardoor een niet-negatief verschil gegarandeerd wordt ondanks individuele instabiliteit.
• Attention-moduleconstructors:
  • Fixed-Ordering Softmax Attention: Certificeert robuustheid door te waarborgen dat de scorevolgorde van attention-heads stabiel blijft onder verstoring.
  • Dominant-Key Linear Attention: Dwingt een dominante sleutel af in lineaire attention-mechanismen, waardoor de drift van de attention-uitvoer wordt begrensd.
• Polynoomnetwerkconstructor: Genereert instanties door expliciet de geometrie van de beslissingsgrens (een reële algebraïsche hypersurface) te controleren en de invoer dicht bij deze grens te plaatsen met een bekende buffer.

2. Profiel van de Moeilijkheidsgraad van Verificatie-instanties

Om de prestaties van verificatoren systematisch te analyseren, stellen de auteurs het Difficulty Profile voor, een tuple van vijf schatbare grootheden die de moeilijkheidsgraad van een instantie karakteriseren, onafhankelijk van een specifieke verificator:

1. Minimum Marge ($\hat{M}_{min}$): Een empirische schatting van de nabijheid tot een tegenvoorbeeld via bemonstering.
2. IBP Relatieve Gap ($G_{IBP}$): Meet de losheid van Interval Bound Propagation (IBP) ten opzichte van de empirische marge.
3. Instabiel Aandeel ($U$): Het aandeel niet-lineaire eenheden waarvan de activeringstoestand ambigu is over de invoerset.
4. Lokale-Regio Complexiteit ($A_\tau$): Schat het aantal verschillende lokale affiene gedragingen (of Taylor-benaderingen) dat nodig is om het marge-landschap over de verstoringset te dekken.
5. Effectieve Gradiënt-Dimensionaliteit ($d_{eff}$): Meet hoe de margegevoeligheid is verdeeld over invoercoördinaten (gerelateerd aan de Participatieverhouding).

Belangrijkste Bijdragen

1. VeriStress-GT Framework: Het eerste herbruikbare framework voor het genereren van neurale netwerkverificatie-instanties met verificator-onafhankelijke ground-truth labels en controleerbare moeilijkheidsparameters.
2. Difficulty Profile: Een unificerend framework voor het karakteriseren van de moeilijkheidsgraad van verificatie-instanties, waardoor de systematische evaluatie van schaalbaarheid en faalmodi van verificatoren mogelijk wordt, verder dan eenvoudige runtime-metrieken.
3. Empirische Evaluatie: Een uitgebreide evaluatie van vijf state-of-the-art verificatoren (waaronder $\alpha,\beta$-CROWN, Marabou, NeuralSAT, PyRAT en nnenum) met behulp van het nieuwe framework.

Resultaten

De evaluatie van vijf state-of-the-art verificatoren op 225 VeriStress-GT-instanties en externe benchmarks (MNIST_fc, oval21) leverde drie primaire bevindingen op:

1. Aan het licht brengen van onjuiste claims: Ground-truth labels onthulden dat meerdere verificatoren valse robuustheidsclaims (SAT) teruggaven op instanties die analytisch robuust waren (UNSAT). Deze fouten werden grotendeels toegeschreven aan beperkingen in numerieke tolerantie. Bovendien onthulde testen met wiskundig bewezen niet-robuuste instanties een specifieke implementatiefout in een populaire verificator met betrekking tot disjunctieve uitvoerbeperkingen, die vervolgens werd opgelost.
2. Diagnostiseerbare Timeouts: Het Difficulty Profile transformeerde ondoorzichtige timeout-uitkomsten in diagnoseerbare faalmodi. Bijvoorbeeld, hoge $G_{IBP}$-waarden correleerden met fouten door extreme losheid van interval-relaxaties, terwijl hoge $d_{eff}$-waarden correleerden met timeouts in scenario's met hoge dimensionale margegevoeligheid.
3. Gerichte Stress-testen: Verschillende constructors isoleerden verschillende faalmodi. MEAP-instanties stress-testten vertakkingsbeslissingen en ambiguïteit in activatiepatronen, terwijl Input-Corner-instanties de losheid van relaxaties isoleerden van de complexiteit van niet-lineaire regio's. Dit stelt ontwikkelaars in staat om gerichte verbeteringen te realiseren (bijvoorbeeld strakkere relaxaties versus betere vertakkingsheuristieken).

Betekenis en Claims

Het paper claimt het benchmarken van verificatie te herformuleren van heuristische evaluatie naar gecontroleerde, ground-truth experimenten. Door instanties met bekende labels te bieden, stelt het framework het volgende in staat:

• Het detecteren van implementatiefouten en numerieke instabiliteiten die anders worden gemaskeerd door consensusgebaseerde evaluatie.
• Het bieden van actieerbare doelen voor het verbeteren van specifieke aspecten van de verificatiepijplijn, zoals numerieke betrouwbaarheid, relaxatiekwaliteit en zoekgedrag.
• Het bieden van een systematische manier om faalmodi van verificatoren te bestuderen door specifieke componenten van het moeilijkheidsprofiel te correleren met de prestaties van de verificator.

De auteurs benadrukken dat het framework, hoewel het beperkingen in huidige verificatoren blootlegt, ook dient als hulpmiddel om de toekomstige ontwikkeling te sturen naar robuustere en betrouwbaardere verificatiesystemen. De code en datasets zijn publiek beschikbaar om dit lopende onderzoek te faciliteren.