Technische Samenvatting: Hiërarchische End-to-End Taylor-begrenzingen voor Volledige Verificatie van Neuronale Netwerken

Probleemstelling

Het artikel behandelt de uitdaging van bereikbaarheidsanalyse van neuronale netwerken, specifiek de taak om de verzameling van uitkomsten die door een neuronale netwerken over een gegeven invoerdomein bereikt kunnen worden, te berekenen of nauwkeurig te begrenzen. Dit probleem is centraal voor het certificeren van veiligheid en robuustheid in leergestuurde fysische systemen, zoals autonoom rijden en medische diagnose.

Hoewel de exacte berekening van de bereikbare verzameling over het algemeen onuitvoerbaar is voor niet-convexe functies, vertrouwen bestaande methoden op uitvoerbare overbenaderingen. De auteurs stellen vast dat huidige state-of-the-art methoden voor gladde, tweemaal differentieerbare netwerken (zoals die met tanh- of sigmoid-activaties) doorgaans ten hoogste informatie van de tweede orde (gradienten en Hessiaan) benutten, maar falen in het systematisch benutten van hogere-orde gladheid (specifiek, de Lipschitz-st continuïteit van de Hessiaan) om benaderingsfouten te beheersen. Het doel is om strakkere, bewijsbare bovengrenzen af te leiden voor de maximale waarde van een functie $f(x)$ over een begrende invoerverzameling $X$, geformuleerd als:
$$\max_{x \in X} f(x)$$
waarbij $X$ doorgaans een $\ell_2$- of $\ell_\infty$-bol is.

Methodologie: HITAB-raamwerk

De auteurs stellen HITAB (Hierarchical End-to-End Taylor Bounds) voor, een verificatieraamwerk dat een hiërarchie van bovengrenzen construeert op basis van nulde-, eerste- en tweede-orde lokale informatie, aangevuld met de Lipschitz-constante van de Hessiaan ($L_{\nabla^2 f}$).

1. Hiërarchie van Taylor-begrenzingen

Het raamwerk definieert een reeks majorisatoren $\bar{f}$ die de functie $f(x_c + \delta)$ begrenzen rond een nominale punt $x_c$:

• Nulde Orde: Gebruikt de functiewaarde $f(x_c)$ en de globale Lipschitz-constante $L_f$. De begrenzing is lineair in de verstoringgrootte $\epsilon$.
• Eerste Orde: Integreert de gradient $\nabla f(x_c)$ en de gradient-Lipschitz-constante $L_{\nabla f}$. Dit levert een kwadratische restbegrenzing op.
• Tweede Orde (Kernbijdrage): Integreert de Hessiaan $\nabla^2 f(x_c)$ en de Hessiaan-Lipschitz-constante $L_{\nabla^2 f}$. Dit resulteert in een Taylor-model van de tweede orde met een gecertificeerde kubische restterm:
  $$f(x_c + \delta) \leq f(x_c) + \nabla f(x_c)^\top \delta + \frac{1}{2}\delta^\top \nabla^2 f(x_c) \delta + \frac{1}{6}L_{\nabla^2 f}\|\delta\|_2^3$$
  In tegenstelling tot lager-orde begrenzingen is het maximaliseren van deze tweede-orde majorisator over een Euclidische bol over het algemeen niet-convex en onuitvoerbaar. De auteurs stellen een "Split-and-Bound"-relaxatie voor om een gesloten-vormige, computationeel uitvoerbare bovengrens af te leiden.

2. Compositional Schatting van de Hessiaan-Lipschitz-constante

Een kritieke technische hindernis is het berekenen van $L_{\nabla^2 f}$ voor diepe neuronale netwerken. De auteurs ontwikkelen een laagsgewijze propagatieprocedure (Stelling 5) om deze constante te begrenzen.

• Zij definiëren een recursieve compositiesregel voor de Hessiaan-Lipschitz-constante van laagmappen $F^I(x) = \sigma(W^I x + b^I)$.
• De begrenzing hangt af van de Lipschitz-constanten van de activatiefunctie $\sigma$ en zijn afgeleiden ($L_\sigma, L_{\sigma'}, L_{\sigma''}$), evenals van de netwerkgewichten en eerder berekende Lipschitz-constanten van de laaguitkomsten en hun gradienten.
• Dit maakt een efficiënte, modulaire berekening van $L_{\nabla^2 f}$ mogelijk, van de invoerlaag tot de uitvoerlaag.

3. Integratie met Branch-and-Bound (BaB)

Om volledige verificatie te bereiken, worden de HITAB-begrenzingen geïntegreerd in een Branch-and-Bound (BaB)-pijplijn.

• Het algoritme partitioneert het invoerdomein iteratief.
• Bij elke knoop wordt de hiërarchische begrenzing $\bar{f}_m$ (het minimum van nulde-, eerste- en tweede-orde certificaten) berekend.
• Het proces gaat door totdat de kloof tussen de boven- en ondergrenzen onder een voorgeschreven tolerantie daalt.
• Het raamwerk ondersteunt zowel $\ell_2$- als $\ell_\infty$-geconstraineerde invoerverzamelingen, met specifieke aanpassingen voor $\ell_\infty$-dozen met behulp van normrelaties.

Belangrijkste Bijdragen

1. Compositional Hessiaan-Lipschitz-begrenzing: Een nieuw, efficiënt algoritme om $L_{\nabla^2 f}$ te begrenzen in diepe feedforward-netwerken door krommebegrenzingen laag voor laag te propageren.
2. End-to-End Taylor-model van de tweede orde: Een gecertificeerde lokale bovengrens met een kubische restterm, die gebruikmaakt van de Lipschitz-continuïteit van de Hessiaan.
3. Unificatie van een Hiërarchie van Begrenzingen: Een raamwerk dat nulde-, eerste- en tweede-orde begrenzingen verenigt, en precieze voorwaarden (drempels op de verstoringgrootte $\epsilon$) biedt waaronder hogere-orde benaderingen bewijsbaar strakkere certificaten opleveren dan lager-orde benaderingen.
4. Praktische Verificatiepijplijn: De integratie van deze begrenzingen in een volledige BaB-verificator (Algoritme 1) voor gladde neuronale netwerken.

Experimentele Resultaten

De auteurs hebben HITAB geëvalueerd op een 6D quadrotor-besturingsbenchmark, waarbij een neuronale netwerkcontroller (getraind om een Model Predictive Controller na te bootsen) een systeem bestuurt terwijl het obstakels vermijdt. De taak omvatte het berekenen van bereikbare verzamelingen over 10 tijdstappen onder $\ell_\infty$-gebegrensde toestandsverstoringen.

• Vergelijking: HITAB werd vergeleken met een state-of-the-art benadering voor lokale begrenzing van de eerste orde (Sharifi en Fazlyab, 2024).
• Prestaties:
  • HITAB verminderde het aantal vertakkingen dat door het BaB-algoritme vereist was aanzienlijk (bijvoorbeeld ~119k vertakkingen versus ~908k vertakkingen bij een tolerantie van $10^{-2}$).
  • Deze reductie vertaalde zich in snellere looptijden (bijvoorbeeld ~108s versus ~320s bij een tolerantie van $10^{-2}$).
• Observatie: De informatie van de tweede orde leverde strakkere lokale benaderingen op, met name op kleinere deelgebieden die tijdens het vertakkingsproces werden gegenereerd, wat leidde tot efficiëntere convergentie.

Betekenis en Beweringen

Het artikel beweert het eerste praktische raamwerk voor bereikbaarheidsanalyse voor gladde neuronale netwerken te presenteren dat systematisch gebruikmaakt van de Lipschitz-continuïteit van kromming (Hessiaan).

• Strakkere Certificaten: Door verder te gaan dan benaderingen van de eerste orde (gradient) of standaard benaderingen van de tweede orde (Hessiaan) en de gladheid van de Hessiaan op te nemen, produceert HITAB strakkere veiligheidscertificaten.
• Systematische Verbetering: Het werk verduidelijkt de regimes waarin informatie van hogere orde voordelig is, en toont aan dat de kubische restterm aanzienlijk minder conservatisme mogelijk maakt in gebieden met kleine verstoringen.
• Volledigheid: In tegenstelling tot veel bestaande methoden voor gladde netwerken die onvolledig (heuristisch) zijn, is HITAB ontworpen om te worden ingebed in volledige verificatiepijplijnen, zodat het verificatieproces kan convergeren naar een exact antwoord, gegeven voldoende tijd.

De auteurs erkennen beperkingen, en merken op dat hun huidige implementatie CPU-gebaseerd is en dat strakkere numerieke relaxaties voor het maximalisatieprobleem van de tweede orde (buiten de gesloten-vorm van split-and-bound) een weg blijven voor toekomstig werk. Echter, stellen zij dat de huidige gesloten-vorm aanpak een gunstige afweging biedt tussen nauwkeurigheid en computatiekosten.