Technische Samenvatting: Gecertificeerde Neurale Approximaties van Nietlineaire Dynamica

Probleemstelling

Nietlineaire dynamische systemen zijn fundamenteel voor cyber-fysieke systemen, maar zijn moeilijk direct te verifiëren en te besturen. Een veelgebruikte strategie is het construeren van een abstractie—een vereenvoudigd model dat het oorspronkelijke systeem benadert. Neurale netwerken zijn effectieve instrumenten geworden voor dit doel, omdat ze in staat zijn om de toestandsruimten impliciet te partitioneren en vereenvoudigde dynamica te leren.

Echter, voor deze neurale abstracties om veilig te zijn in kritieke toepassingen, moeten ze voorzien zijn van formele garanties met betrekking tot hun nabijheid tot het ware systeem. Men moet specifiek kunnen certificeren dat het neurale netwerk $N(x)$ de ware dynamica $f(x)$ benadert binnen een begrensde fout $\epsilon$ (i.e., $\|f(x) - N(x)\|_\infty \le \epsilon$) over een gegeven domein.

Bestaande verificatiemethoden vertrouwen zwaar op SMT-solvers (Satisfiability Modulo Theories, bijv. dReal) om te redeneren over nietlineaire reële aritmetica. Hoewel deze solvers sound (correct) zijn, lijden ze aan ernstige schaalbaarheidsbeperkingen; ze falen vaak bij het verifiëren van grotere netwerken of hogere-dimensionale systemen binnen een redelijke tijdspanne. Deze computationele flessenhals beperkt de praktische toepassing van neurale abstracties tot complexe, hoog-dimensionale scenario's.

Methodologie

De auteurs stellen een nieuw, schaalbaar verificatiekader voor dat de afhankelijkheid van dure SMT-solvers voor nietlineaire aritmetica elimineert. In plaats daarvan maakt de methode gebruik van gecertificeerde eerste-orde Taylor-modellen en een paralleliseerbare adaptieve partitioneringsstrategie.

1. Gecertificeerde Eerste-orde Taylor-modellen

In plaats van het nietlineaire predicaat $\exists x : \|f(x) - N(x)\| > \epsilon$ direct te verifiëren, benadert de methode de ware dynamica $f(x)$ lokaal met behulp van eerste-orde Taylor-expansies.

• Lokale Linearisatie: Het invoerdomein $X$ wordt gepartitioneerd in hyperrechthoeken. Binnen elke hyperrechthoek $H_\delta(c)$ gecentreerd rond $c$, worden de dynamica begrensd door een lineaire functie plus een restterm:
  $$f(x) \in (f(c) + J_f(c)(x - c)) \oplus R$$
  waarbij $J_f(c)$ de Jacobiaan is en $R$ een gecertificeerde foutgrens is afgeleid van de Lagrange-foutgrens (voor gladde functies) of CROWN (voor ReLU-netwerken).
• Verificatie via Lineaire Solvers: Deze transformatie zet het verificatieprobleem om in het controleren van de bevredigbaarheid van lineaire ongelijkheden. De auteurs gebruiken Marabou 2.0, een verificatietool voor neurale netwerken gebaseerd op lineaire grenspropagatie, om deze condities te verifiëren. Dit vermijdt de computationele kosten van nietlineaire aritmetische redenering.

2. Adaptieve Certificaatverfijning

Om de conservativiteit aan te pakken die wordt geïntroduceerd door lineaire benaderingen (waarbij de foutterm $R$ te ruim kan zijn), gebruikt het kader een adaptieve verfijningsstrategie:

• Splitsingscriteria: Een hyperrechthoek wordt gesplitst als:
  1. De Taylor-restterm te conservatief is ($R_{max} - R_{min} > \epsilon$).
  2. Een potentieel tegenvoorbeeld gevonden door de solver niet voldoet aan de ware foutconditie (een "spuurs" tegenvoorbeeld door de linearisatie).
• Doelgerichte Partitionering: De splitsingsas wordt gekozen op basis van de bijdrage van invoerdimensies aan de benaderingsfout, waarbij prioriteit wordt gegeven aan dimensies die betrokken zijn bij nietlineaire termen. Dit maakt output-afhankelijke verfijning mogelijk, waarbij verschillende outputdimensies verschillende niveaus van partitionering kunnen vereisen.
• Parallelisatie: Het verificatieproces wordt geparallelliseerd met behulp van een gedeelde stack (depth-first search) die wordt geraadpleegd door een pool van worker-processen. Elke worker verwerkt een hyperrechthoek, certificeert deze, of splitst deze en plaatst de subregio's terug op de stack.

3. Training

Neurale netwerken worden getraind om zowel de gemiddelde kwadratische fout als de maximale $L_\infty$-fout over gesamplede inputs te minimaliseren. De verliesfunctie bevat een term voor de slechtste-geval-fout om de sample-efficiëntie voor verificatie te verbeteren.

Belangrijkste Bijdragen

1. SMT-vrije Verificatie: De introductie van een methode gebaseerd op gecertificeerde linearisaties die de primaire computationele flessenhals (nietlineaire reële aritmetische redenering) van eerdere benaderingen wegneemt.
2. Adaptieve Parallelle Verfijning: Een schaalbare strategie die adaptieve verificatie met niet-uniforme nauwkeurigheid over het invoerdomein mogelijk maakt, wat de conservativiteit aanzienlijk vermindert zonder de soundness in gevaar te brengen.
3. Schaalbaarheid: Het vermogen om hogere-dimensionale systemen (tot 7D) en aanzienlijk grotere neurale netwerken aan te pakken dan de huidige state-of-the-art methoden.
4. Nieuwe Toepassingen: De uitbreiding van neurale abstracties naar twee voorheen onhandelbare scenario's:
   • Neurale Netwerkcompressie: Het verifiëren dat een gecomprimeerd netwerk $\epsilon$-dicht bij een groter "teacher"-netwerk blijft.
   • Koopman Operator Ontdekking: Het verifiëren van traject-niveau voorspellingen waarbij de output van het netwerk een sequentie van toekomstige toestanden representeert (over meer dan 100 toestanden in de laatste laag).

Experimentele Resultaten

De methode werd geëvalueerd op gevestigde benchmarks uit de literatuur (bijv. WaterTank, JetEngine, Van der Pol Oscillator) en nieuwe uitdagende taken.

• Prestaties vs. State-of-the-Art: Vergeleken met de dReal-gebaseerde aanpak (Abate et al., 2022), vertoonde de voorgestelde methode substantiële versnellingen. Bijvoorbeeld, op de WaterTank-benchmark was de nieuwe methode ongeveer 820 keer sneller. Terwijl dReal de tijdslimiet (1 uur) overschreed op de meeste grote modellen (bijv. 3x[64] architectuur voor JetEngine, SteamGovernor), slaagde de voorgestelde methode erin 100% van het domein te certificeren voor alle geteste modellen, inclusief hoog-dimensionale systemen zoals de Low Thrust Spacecraft (7D).
• Koopman-operatoren: Het kader verifieerde succesvol een trajectvoorspellingsnetwerk gebaseerd op Koopman-theorie. Ondanks dat het netwerk een lage gemiddelde kwadratische fout bereikte op validatiedata, identificeerde de verificatie specifieke tegenvoorbeelden waar de fout de tolerantie ($\epsilon=0.1$) overschreed. Cruciaal is dat het 99,03% van het invoerdomein certificeerde, wat een genuanceerd inzicht biedt in waar het model betrouwbaar is—een capaciteit die ontbreekt bij methoden die slechts één enkel tegenvoorbeeld teruggeven.
• Neurale Compressie: De methode verifieerde een gecomprimeerd netwerk (gereduceerd van 4,2M naar 67k parameters, een reductie van 98,4%) dat de dynamica van de Lorenz-attractor benadert. Het verificatieproces controleerde meer dan 3,5 miljoen hyperrechthoeken en voltooide dit in ongeveer 89 uur, wat de haalbaarheid voor grootschalige, niet-analytische dynamica aantoont.

Betekenis en Claims

Het artikel claimt dat de primaire betekenis ligt in het oplossen van de schaalbaarheidsbottleneck van neurale abstractieverificatie. Door de verificatie van het neurale netwerk (behandeld door lineaire solvers) te ontkoppelen van de verificatie van de nietlineaire dynamica (behandeld via lokale linearisatie en verfijning), stelt de auteur de formele verificatie van complexe, hoog-dimensionale systemen mogelijk die voorheen onhandelbaar waren.

De auteurs benadrukken dat hun aanpak formele foutgrenzen biedt die toelaten dat neurale benaderingen veilig als surrogaten kunnen worden ingezet door de fout te interpreteren als begrensde verstoringen. Deze soundness zorgt ervoor dat eigenschappen die op de abstractie zijn geverifieerd (zoals veiligheid of bereikbaarheid) rigoureus kunnen worden overgedragen naar het concrete systeem. Het werk benadrukt ook de veelzijdigheid van het kader, waarbij wordt aangetoond dat het kan worden toegepast buiten standaard dynamische systemen, zoals bij algemene functiebenaderingstaken zoals netwerkcompressie en deep learning-architecturen voor operatortheorie.