Technische Samenvatting: Set-gebaseerde Training van Neuronale Barrière-certificaten voor Veiligheidsverificatie van Dynamische Systemen

1. Probleemstelling

De veiligheidsverificatie van continue-tijd dynamische systemen is kritiek voor autonome agenten in veiligheidskritieke omgevingen (bijvoorbeeld zelfrijdende voertuigen, UAV's, robotmanipulatoren). Een systeem wordt als veilig beschouwd als geen enkele traject die start vanuit een initiële verzameling $X_I$ een onveilige verzameling $X_U$ binnentreedt.

Bestaande verificatiemethoden ondervinden aanzienlijke beperkingen:

• Op simulatie gebaseerde methoden lijden onder exponentiële groeicijfers van de runtime in verhouding tot de systeemdimensionaliteit.
• Bereikbaarheidsanalyse maakt gebruik van set-gebaseerde berekeningen om exponentiële runtime te vermijden, maar kan computatie-intensief zijn.
• Barrière-certificaten bieden een formeel bewijs van veiligheid door een scalair functie $B$ te definiëren die $X_I$ scheidt van $X_U$ via zijn nivo-niveau. Echter, recente benaderingen om op neurale netwerken gebaseerde barrière-certificaten te synthetiseren, vertrouwen op een iteratief trainings-verificatiecyclus. In deze cyclus wordt een neurale netwerk getraind op staatsruimte-monsters, waarna het formeel wordt geverifieerd met een externe solver (bijvoorbeeld SMT). Als de verificatie faalt (tegenvoorbeelden gevonden), wordt het netwerk opnieuw getraind. Dit proces is kostbaar, vereist mogelijk vele cycli, en garandeert geen convergentie naar een geldig certificaat binnen één enkele procedure.

2. Methodologie: Set-gebaseerde Training

De auteurs stellen een nieuwe set-gebaseerde trainingsbenadering voor die formele verificatie direct integreert in het trainingsproces van het neurale netwerk, waardoor de noodzaak voor een aparte verificatiestap wordt geëlimineerd.

Kernconcept

In plaats van te trainen op discrete monsters en later te verifiëren, traint de methode het neurale netwerk $B_\theta$ met behulp van een zorgvuldig set-gebaseerde verliesfunctie. Deze verliesfunctie wordt berekend over volledige verzamelingen (omsluitingen) van de staatsruimte in plaats van individuele punten. Wanneer de verliesfunctie nul bereikt, wordt de geldigheid van het barrière-certificaat formeel bewezen door constructie.

Belangrijke Technische Componenten

A. Zorgvuldige Set-gebaseerde Verliesfunctie
De verliesfunctie codeert de drie eigenschappen die vereist zijn voor een barrière-certificaat (Stelling 1):

1. Eigenschap P I (Onveilige Staten): Alle staten in $X_U$ moeten positieve waarden opleveren. De verliesfunctie $L_I$ straft de ondergrens van de set-gebaseerde afbeelding van $X_U$.
2. Eigenschap P II (Initiële Staten): Alle staten in $X_I$ moeten niet-positieve waarden opleveren. De verliesfunctie $L_{II}$ straft de bovengrens van de set-gebaseerde afbeelding van $X_I$.
3. Eigenschap P III (Dynamiek van het Nivo-niveau): De Lie-afgeleide $L_f B_\theta$ moet negatief zijn op het nivo-niveau $X_Z = \{x \mid B_\theta(x) = 0\}$.
   • Aangezien $X_Z$ onbekend en niet-convex is, berekent de methode een strakke omsluiting van $X_Z$ met behulp van een vereniging van zonotopen via een recursieve branch-and-bound strategie (het splitsen van de inputruimte en het verwijderen van regio's zonder nulpunten).
   • Voor elke zonotoop in de omsluiting wordt de Lie-afgeleide omsloten met behulp van set-gebaseerde voorwaartse propagatie van gradiënten en de systeemdynamiek.
   • De verliesfunctie $L_{III}$ straft de bovengrenzen van deze omsluitingen van de Lie-afgeleide.

De totale verliesfunctie is $L = L_I + L_{II} + L_{III}$. Als $L=0$, wordt het systeem formeel geverifieerd als veilig.

B. Set-gebaseerde Voorwaartse Propagatie
Om deze verliezen te berekenen, propageert de methode zonotopen (een specifiek type convex polytoop) door de lagen van het neurale netwerk:

• Lineaire Lagen: Exact berekend via affiene afbeeldingen.
• Niet-lineaire Lagen: Omsloten met behulp van conservatieve over-approximaties (bijvoorbeeld range-bounding).
• Gradiënten en Lie-afgeleiden: De verzameling gradiënten wordt achterwaarts gepropageerd, en de Lie-afgeleide wordt berekend als het inwendig product van de gradiëntverzameling en de stromingsverzameling.

C. Algorithmus
De trainingslus (Algorithmus 1) initialiseert het netwerk, berekent set-gebaseerde verliezen voor $P_I$, $P_{II}$ en $P_{III}$, update parameters via gradiëntafdaling, en beëindigt de uitvoering zodra de totale verliesfunctie nul is.

3. Belangrijkste Bijdragen

1. Synthese in één Procedure: Een nieuwe benadering om neuronale barrière-certificaten te synthetiseren in één enkele set-gebaseerde trainingsprocedure, waarmee de iteratieve trainings-verificatiecyclus wordt verwijderd.
2. Zorgvuldige Verliesfunctie: Een set-gebaseerde verliesfunctie die zorgvuldig alle eigenschappen van barrière-certificaten codeert. Een verlieswaarde van nul vormt een formeel bewijs van veiligheid.
3. Iteratieve Verfijning: Een iteratieve procedure om dynamisch de omsluiting van het nivo-niveau en de vereiste Lie-afgeleide voor Eigenschap P III te genereren.
4. Uitgebreide Evaluatie: Evaluatie op 13 benchmarks die lineaire, polynoom- en niet-polynoom dynamiek omvatten, inclusief hoog-dimensionale systemen (tot 9D) en complexe verzamelingconfiguraties.

4. Experimentele Resultaten

De benadering is geïmplementeerd met behulp van de CORA toolbox en vergeleken met state-of-the-art tools: SynNBC en FOSSIL (iteratieve trainings-verificatie) en PRoTECT (optimalisatie van sommen van kwadraten).

• Succespercentage: De voorgestelde methode behaalde een succespercentage van 100% over alle 13 benchmarks.
  • In tegenstelling hiermee faalden SynNBC en PRoTECT bij niet-polynoom dynamiek en benchmarks met meerdere initiële/onveilige verzamelingen.
  • FOSSIL behaalde hoge succespercentages, maar degradeerde bij hoger-dimensionale systemen (bijvoorbeeld 70% op Peruffo 6D, 80% op Peruffo 8D).
• Runtime: De set-gebaseerde trainingsbenadering was aanzienlijk sneller dan FOSSIL. Bijvoorbeeld, op de Peruffo (8D) benchmark duurde de voorgestelde methode gemiddeld 1,0s, vergeleken met 47,7s voor FOSSIL.
• Trainings-efficiëntie: De methode convergeerde doorgaans in een paar trainings-epoch. In tegenstelling hiermee vereiste FOSSIL vaak meerdere trainings-verificatiecycli, waarbij elke cyclus tot 1.000 epoch kon omvatten.
• Ablatiestudies:
  • Netwerkarchitectuur: Ondiepe netwerken (enkele lineaire laag) volstonden voor lineaire systemen maar faalden bij niet-polynoom systemen. Diepere netwerken waren vereist voor complexe dynamiek.
  • Omsluiting van het Nivo-niveau: Complexere dynamiek vereiste meer uitgebreide omsluitingen van het nivo-niveau (meer splitsingen/iteraties) om Eigenschap P III te voldoen.

5. Betekenis en Beweringen

Het artikel beweert dat deze benadering een paradigmaverschuiving in veiligheidsverificatie vertegenwoordigt door de trainings- en verificatiefasen samen te voegen.

• Formele Garanties: In tegenstelling tot standaard training van neurale netwerken, die geen formele veiligheidsgaranties biedt, zorgt deze methode ervoor dat een verlies van nul impliceert een geldig barrière-certificaat.
• Schaalbaarheid: De operaties reduceren tot efficiënte matrixvermenigvuldigingen, wat resulteert in polynoomcomplexiteit die goed schaalt met de systeemdimensionaliteit.
• Veelzijdigheid: De benadering is grotendeels agnostisch ten opzichte van systeemdynamiek, en handelt op natuurlijke wijze complexe niet-lineaire (niet-polynoom) dynamiek en complexe verzamelrepresentaties (bijvoorbeeld verenigingen van verzamelingen, niet-convexe regio's) af, waar interval-gebaseerde methoden moeite mee hebben.
• Efficiëntie: Door de kostbare iteratieve cyclus te elimineren, biedt de methode een efficiëntere weg naar formele verificatie voor hoog-dimensionale en niet-lineaire systemen.

De auteurs concluderen dat hun set-gebaseerde synthese efficiënt barrière-certificaten kan genereren zonder dat daaropvolgende verificatie vereist is, en presteert beter dan eerdere werken, met name op hoog-dimensionale en niet-polynoom systemen.