Technische Samenvatting: Differentieel Zonotopen voor het Verifiëren van Globale Robuustheid van DNN's

1. Probleemstelling

Deep Neural Networks (DNN's) worden steeds vaker ingezet in veiligheidskritische domeinen zoals transport en de gezondheidszorg, waar hun robuustheid tegen inputperturbaties essentieel is. Hoewel lokale robuustheid (het waarborgen dat voorspellingen niet veranderen bij kleine perturbaties rond een specifieke input) een goed bestudeerde veiligheidseigenschap is, is globale robuustheid een strikt sterkere vereiste. Globale robuustheid vereist dat voor alle paren inputs binnen een bepaalde afstand de voorspellingen van het model consistent blijven.

Formeel gezien is globale robuustheid een 2-veiligheidseigenschap, die de verificatie van een relatie tussen twee universeel gekwantificeerde executietracés vereist in plaats van een enkele trace. Deze complexiteit maakt globale verificatie aanzienlijk uitdagender dan lokale verificatie. Bestaande methoden voor vertrouwensgebaseerde globale robuustheid (die garanties beperken tot voorspellingen met een hoog vertrouwen om beslissingsgrenzen te vermijden) maken gebruik van gespecialiseerde satisfiability-solvers, maar lijden onder een gebrekkige schaalbaarheid en zijn momenteel beperkt tot netwerken met slechts tientallen neuronen.

2. Methodologie

Het artikel stelt een nieuw statisch analyseframework voor op basis van differentiele halo-zonotopen om globale robuustheid efficiënt te verifiëren.

2.1 Differentiele Halo-zonotopen

De kern van de technische innovatie is de uitbreiding van het zonotoop abstracte domein. Standaard zonotopen representeren verzamelingen punten via een centrum en een generator-matrix. Om globale robuustheid te verifiëren, moeten de auteurs twee executies van hetzelfde DNN met verschillende inputs gelijktijdig volgen.

• Uitdaging: Naïeve aanpassingen van differentiele zonotopen (voorheen gebruikt voor DNN-equivalentie-verificatie waarbij inputs identiek zijn) falen voor globale robuustheid. Het initialiseren van inputs als identiek of het gebruik van volledig onafhankelijke generatoren leidt tot onsoundheid of excessieve over-approximatie (verlies van precisie).
• Oplossing: De auteurs introduceren differentiele halo affiene vormen. Deze codering verdeelt de perturbatiegrens $\epsilon$ over twee generatoren:
  1. Een primaire generator die gedeeld wordt tussen de twee executies om correlatie te behouden.
  2. Secundaire generatoren die onafhankelijk zijn voor elke executie om de perturbatie te modelleren.
• Mechanisme: Deze "halo"-structuur stelt het systeem in staat om sound en precies de conditie te coderen dat twee inputs $x$ en $y$ binnen een bounding box $[l, u]$ liggen en voldoen aan $|x - y| \le \epsilon$. De differentiele zonotoop $\mathcal{Z}_\Delta$ volgt het verschil tussen de executies in lock-step, wat nauwere grenzen oplevert voor de divergentie dan het aftrekken van individuele zonotopen.

2.2 Symmetrische Vertrouwensgebaseerde Globale Robuustheid

Het artikel identificeert een beperking in de bestaande definitie van vertrouwensgebaseerde globale robuustheid (de asymmetrische variant), die vereist dat een input $x$ met een hoog vertrouwen niet kan worden geperturbeerd naar een andere klasse $y$, ongeacht de mate van vertrouwen van $y$. De auteurs stellen dat dit te restrictief is, aangezien een perturbatie die leidt tot een voorspelling met een laag vertrouwen in de praktijk acceptabel is (bijv. het triggeren van een handmatige controle).

Zij stellen een symmetrische variant voor:

• Definitie: Voor elke twee inputs $x, y$ binnen afstand $\epsilon$, als beide geclassificeerd zijn met een vertrouwen groter dan een drempelwaarde $\tau$, moeten ze tot dezelfde klasse behoren.
• Voordeel: Deze versoepeling staat een bredere klasse van netwerken toe als "robuust" terwijl het betekenisvol blijft voor veiligheidskritische toepassingen waarbij outputs met een laag vertrouwen worden afgehandeld via fallback-mechanismen.

2.3 Verificatie-algoritme

Het verificatieproces (geïmplementeerd in de tool TwoSafe) volgt deze stappen:

1. Initialisatie: Constructie van een differentiele halo-zonotoop die de inputruimte en perturbatiebeperkingen representeert.
2. Propagatie: Propagatie van de zonotoop door de DNN-lagen. Voor ReLU-activaties introduceert de methode nieuwe generatoren om de niet-lineariteit te over-approximeren, waarbij de differentiele structuur behouden blijft.
3. Eigenschapstoetsing: Aan de output formuleert het systeem een Lineair Programmeringsprobleem (LP) om te controleren of er paren outputs bestaan waarbij de klassen verschillen terwijl beide voldoen aan de vertrouwensdrempel $\tau$.
4. Verfijning: Indien de controle inconclusief is (door over-approximatie), voert het algoritme generator splitting uit. In tegenstelling tot standaard input splitting, splitst dit de generatoren van de differentiele halo-zonotoop om de approximatie te verfijnen zonder de dekking van de perturbatieruimte te verliezen.

3. Belangrijkste Bijdragen

1. Differentiele Halo-zonotopen: Een nieuw abstract domein dat zonotopen uitbreidt om paren van geperturbeerde inputs gezamenlijk en in lock-step te propageren, waardoor hun divergentie nauwgezet wordt begrensd. Dit maakt de verificatie van globale 2-veiligheidseigenschappen mogelijk met een hogere precisie dan individuele analyse.
2. Symmetrische Vertrouwensgebaseerde Globale Robuustheid: Een nieuwe definitie van globale robuustheid die alleen consistentie vereist tussen voorspellingen met een hoog vertrouwen. Deze definitie is strikt minder restrictief dan de asymmetrische variant en staat efficiënte verificatie toe binnen het voorgestelde framework.
3. Soundness Proof: Een formeel bewijs van de soundness van de differentiele zonotoop-gebaseerde statische analyse, met kernresultaten geformaliseerd in Isabelle.
4. TwoSafe Tool & Evaluatie: Implementatie van de aanpak in een nieuwe tool, TwoSafe, die de state-of-the-art (CGR baseline) aanzienlijk overtreft in zowel precisie als schaalbaarheid.

4. Experimentele Resultaten

De auteurs hebben TwoSafe geëvalueerd op vier benchmarks: Law (klein), LHC (deeltjesclassificatie), ACAS Xu (botsingsvermijding) en HAR (menselijke activiteitsherkenning).

• Schaalbaarheid: TwoSafe heeft succesvol globale robuustheid geverifieerd op netwerken met tot 500 ReLU-neuronen en 561 inputdimensies (HAR benchmark). In contrast hiermee liep de baseline (CGR) vast (time-out) of raakte het geheugen uitgeput op deze grotere netwerken.
• Precisie: De baseline rapporteerde regelmatig spuria-tegenvoorbeelden (false positives) door grove softmax-approximaties, met name op netwerken met veel outputklassen. TwoSafe vermeed deze fout-positieven.
• Prestaties: TwoSafe demonstreerde significante versnellingen. Zo verifieerde TwoSafe bijvoorbeeld de robuustheid van de LHC-benchmark in minder dan 3 seconden, terwijl de baseline na 2 uur nog steeds draaide of een time-out gaf.
• Symmetrisch vs. Asymmetrisch: De symmetrische eigenschap maakte succesvolle verificatie mogelijk in parameterregimes waar de asymmetrische eigenschap inconclusief was of faalde. Bijvoorbeeld, op de HAR-benchmark met $\epsilon=0.01$, was de symmetrische eigenschap verifieerbaar terwijl de asymmetrische variant een time-out gaf.

5. Betekenis en Claims

Het artikel claimt de inherente spanning tussen de kracht van robuustheidsgaranties en de schaalbaarheid van verificatietools te hebben opgelost. Door over te stappen van lokale naar globale robuustheidsverificatie en gebruik te maken van differentiele halo-zonotopen, tonen de auteurs aan dat het mogelijk is om aanzienlijk bredere en diepere netwerken te verifiëren dan voorheen mogelijk was.

De introductie van symmetrische vertrouwensgebaseerde globale robuustheid wordt gepresenteerd als een praktische vooruitgang, die een "betekenisvolle notie van robuustheid" biedt door te erkennen dat voorspellingen met een laag vertrouwen in de echte wereld vaak anders worden afgehandeld. Het werk vestigt de basis voor differentiele verificatie die, wanneer aangepast voor 2-veiligheidseigenschappen, kan schalen naar netwerken die een orde van grootte groter zijn dan die behandeld door eerdere technieken, waardoor certificering van globale robuustheid voor in de praktijk ingezette modellen haalbaar wordt.