Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement

Technische Samenvatting: Precieze Verificatie van Transformers door ReLU-Gestuurde Abstractie-Verfijning

Probleemstelling
De formele verificatie van Transformer-modellen is kritiek geworden vanwege hun inzet in veiligheidskritieke toepassingen zoals autonoom rijden en gezondheidszorg. Het verificeren van Transformers is echter aanzienlijk uitdagender dan het verificeren van klassieke feed-forward neurale netwerken (FFNN's) vanwege de hoge complexiteit van hun inferentieberekeningen, met name de inproducten binnen self-attention-lagen. Bestaande verificatiemethoden vertrouwen op abstracte interpretatie om convexe over-approximaties van outputbereiken te construeren. Hoewel deze methoden efficiënt zijn, lijden ze vaak onder een "volledigheidsprobleem": de over-approximatie introduceert aanzienlijke fouten, wat leidt tot frequente vals-positieve alarmen waarbij de geapproximeerde output een robuustheidseigenschap schendt, terwijl de feitelijke output dat niet doet. Specifiek gebruiken huidige state-of-the-art methoden (bijv. Shi et al. [23]) stijve planaire grenzen voor inproducten die bewezen correct zijn, maar vaak suboptimaal, omdat ze de hyperbolische paraboloïde die wordt gevormd door het product van twee variabelen niet strak kunnen begrenzen.

Methodologie
De auteurs stellen BuFFeT (BoUnd Fusing-based reFinEment for Transformers) voor, een nieuw verificatiekader dat de precisie verbetert door meerdere planaire grenzen voor inproducten te fuseren en deze weer te geven met ReLU-functies.

1. Constructie van Dubbele Grenzen: Het artikel identificeert dat de standaard planaire grens die in eerdere werken wordt gebruikt (Eq. 4) slechts één zijde van de hyperbolische paraboloïde die een inproduct voorstelt ($z=xy$) dekt. De auteurs leiden een "dubbele" planaire grens af (Eq. 5) die de tegenovergestelde zijde dekt.
2. ReLU-gebaseerde Representatie: Om de exponentiële complexiteit van het doorgeven van niet-lineaire min/max-functies (die zouden ontstaan door simpelweg het minimum van de twee planaire grenzen te nemen) te vermijden, stellen de auteurs de gefuseerde grens voor met ReLU-functies. Specifiek wordt de strakkere bovengrens geformuleerd als de oorspronkelijke grens minus een ReLU-term, en de strakkere ondergrens is de oorspronkelijke grens plus een ReLU-term (Eq. 8 en 9).
3. Strategieën voor Abstractie-Verfijning: De kerninnovatie ligt in het optimaliseren van de lineaire relaxatie van deze ReLU-termen. De lineaire ondergrens van een ReLU wordt geparametriseerd door een helling $\alpha \in [0, 1]$. De auteurs breiden twee strategieën uit klassieke FFNN-verificatie uit om de optimale $\alpha$ te bepalen:
   • r-BuFFeT (Regelgebaseerd): Past een heuristiek uit [24] toe die $\alpha$ (ofwel 0 of 1) selecteert op basis van het inputbereik van de ReLU om het gebied van over-approximatie te minimaliseren. Dit kiest in feite de betere van de twee planaire grenzen voor een specifiek geval.
   • o-BuFFeT (Optimalisatiegebaseerd): Behandelt $\alpha$ als een beslissingsvariabele in een optimalisatieprobleem. Het formuleert de verificatietak als het minimaliseren van een verliesfunctie (softplus van de negatieve marge) onderworpen aan de lineaire constraints die zijn afgeleid uit de ReLU-grenzen. Met behulp van moderne op gradiënten gebaseerde oplosmethoden (bijv. Adam) verfijnt het iteratief $\alpha$ om een oplossing te vinden die robuustheid certificeert, en zoekt effectief de ruimte van mogelijke grenzen af.

Belangrijkste Bijdragen

• Nieuw ReLU-gebruik: Het artikel introduceert een methode om precieze, niet-lineaire grenzen voor inproducten weer te geven met ReLU-functies, waardoor de kloof wordt overbrugd tussen Transformer-verificatie en de uitgebreide literatuur over ReLU-relaxatie in klassieke neurale netwerken.
• Theoretische Unificatie: De auteurs tonen aan dat de planaire grenzen die in de state-of-the-art-aanpak [23] worden gebruikt en hun dubbele, specifieke instantiaties zijn van hun ReLU-gebaseerde representatie (respectievelijk overeenkomend met $\alpha=0$ en $\alpha=1$), wat verklaart waarom deze vaste strategieën vaak suboptimaal zijn.
• Twee Nieuwe Kaders: Het voorstellen van r-BuFFeT en o-BuFFeT biedt twee verschillende paden voor efficiënte en precieze verificatie, waarbij de optimalisatiegebaseerde aanpak een mechanisme biedt om approximaties iteratief te verfijnen totdat robuustheid is gecertificeerd.

Experimentele Resultaten
De auteurs hebben BuFFeT geëvalueerd op 10 Transformer-modellen (inclusief standaardarchitecturen met 1 tot 6 lagen en TinyBERT) die zijn getraind op sentimentanalyse-datasets (SST en Yelp). De evaluatie omvatte 1.400 verificatietaken tegen de state-of-the-art-baseline [23].

• Precisie: Beide BuFFeT-aanpakken toonden aanzienlijke precisieverbeteringen. Voor diepere modellen (bijv. $N=6$) verbeterde r-BuFFeT de maximaal geverifieerde verstoring ($\epsilon$) met tot 1,8 keer, terwijl o-BuFFeT tot 3,6 keer verbetering behaalde ten opzichte van de baseline. o-BuFFeT presteerde consequent beter dan r-BuFFeT, met name op complexe modellen.
• Efficiëntie: r-BuFFeT veroorzaakte een bescheiden tijdsvertraging (1,1x tot 1,7x de baseline) vanwege de berekening van ReLU-inputbereiken. o-BuFFeT introduceerde een hogere vertraging (33x tot 96x de baseline) vanwege het iteratieve optimalisatieproces. De auteurs merken echter op dat verificatie voor modellen met 6 lagen en TinyBERT nog steeds binnen enkele minuten kon worden voltooid, en dat de vertragingratio stabiel bleef ongeacht de modeldiepte.
• Robuustheid: In gevallen waarin de baseline faalde om robuustheid te verifiëren (negatieve marge), slaagde o-BuFFeT erin de approximatie te verfijnen om de eigenschap te certifiëren, wat zijn vermogen demonstreert om vals-positieve alarmen te elimineren.

Betekenis en Claims
Het artikel beweert dat BuFFeT de betrouwbaarheid van Transformer-verificatie aanzienlijk verbetert door approximatiefouten die leiden tot vals-positieve alarmen te verminderen. De primaire betekenis ligt in de methodologische brug die het creëert: door gebruik te maken van ReLU-representaties, maakt de aanpak het mogelijk om gevestigde analysetechnieken uit klassieke neurale netwerkverificatie toe te passen op de unieke uitdagingen van Transformers (specifiek self-attention-inproducten). De auteurs positioneren dit werk als het effenen van het pad voor toekomstig onderzoek in Transformer-verificatie, en suggereren dat het gebruik van ReLU-gebaseerde verfijning kan worden uitgebreid naar andere domeinen en kan worden gecombineerd met bestaande technieken voor betekenisvolle NLP-verificatie. Het werk claimt niet alle verificatieuitdagingen op te lossen, maar biedt een praktische afweging tussen efficiëntie en precisie die de state of the art aanzienlijk verbetert.