Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

Titel: Schaalbare verificatie van Neuronale Controlebarrièrefuncties met behulp van Lineaire Grenspropagatie

Auteurs: Nikolaus Vertovec, Frederik Baymler Mathiesen, Thom Badings, Luca Laurenti, en Alessandro Abate.
Publicatie: Proceedings of Machine Learning Research (PMLR), 8th Annual Conference on Learning for Dynamics and Control (2026).

---

1. Probleemstelling

Controlebarrièrefuncties (Control Barrier Functions - CBF's) zijn een cruciaal hulpmiddel voor het garanderen van veiligheid in niet-lineaire dynamische systemen, zoals autonome voertuigen en robotmanipulatoren. Een CBF zorgt ervoor dat het systeem binnen een "veilige set" blijft (forward invariance).

Recentelijk zijn Neuronale CBF's (CBF's die worden gerepresenteerd als een kunstmatig neurale netwerk) populair geworden vanwege hun uitdrukkingskracht en vermogen om complexe, niet-lineaire dynamica en veiligheidsbeperkingen te modelleren. Echter, het trainen van zo'n netwerk is slechts de eerste stap; het verifiëren dat een getraind netwerk daadwerkelijk een geldige CBF is, vormt een groot computatiekundig knelpunt.

De bestaande verificatiemethoden (zoals SMT-solvers of Mixed-Integer Programming) hebben te kampen met:

• Schaalbaarheid: Ze kunnen niet omgaan met grote neurale netwerken of systemen met hoge dimensies.
• Beperkingen in activatiefuncties: Veel methoden zijn beperkt tot ReLU-activaties en werken niet goed met andere niet-lineaire functies (zoals tanh of sigmoid), die vaak nodig zijn voor complexe dynamica.
• Computationele kosten: Het exacte redeneren over niet-lineaire vergelijkingen is extreem duur.

Het doel van dit paper is een schaalbaar verificatieramenwerk te ontwikkelen dat grotere netwerken en willekeurige niet-lineaire activatiefuncties aankan, zonder afhankelijk te zijn van dure SMT-oplossers.

---

2. Methodologie

De auteurs stellen een nieuw raamwerk voor dat de exacte niet-lineaire verificatie vervangt door het afleiden van voldoende lineaire voorwaarden via over- en onderbenaderingen. De kern van de methode bestaat uit drie stappen:

A. Lineaire Grenspropagatie (LBP) voor Netwerkwaarden en Gradienten

De methode baseert zich op Linear Bound Propagation (LBP), een techniek om lineaire boven- en ondergrenzen te vinden voor de output van een neurale netwerk over een bepaald domein.

• Uitbreiding voor Gradienten: Een unieke bijdrage is de uitbreiding van LBP om niet alleen grenzen te vinden voor de output $B_\theta(x)$, maar ook voor de gradient $\frac{\partial B_\theta(x)}{\partial x}$.
• McCormick Relaxatie: Omdat de gradient van een neurale netwerk een product is van gewichten en afgeleiden van activatiefuncties (bilineaire termen), gebruiken de auteurs McCormick relaxaties. Dit stelt hen in staat om lineaire grenzen te construeren voor deze producten zonder extra forward-passes van het netwerk.
• Resultaat: Voor een gegeven domein $\Delta$ worden lineaire grenzen afgeleid van de vorm:
  $$\underline{J}(x) \leq \frac{\partial B_\theta(x)}{\partial x} \leq \overline{J}(x)$$
  waarbij $\underline{J}$ en $\overline{J}$ lineaire functies zijn.

B. Modellering van de Dynamica

De systeemdynamica (de functies $f(x)$ en $g(x)$ in de vergelijking $\dot{x} = f(x) + g(x)u$) worden benaderd met gecertificeerde Taylor-uitbreidingen van de eerste orde over het domein. Dit levert ook lineaire boven- en ondergrenzen op voor de dynamica.

C. Lineaire Surrogaat voor de CBF-voorwaarde

De CBF-voorwaarde vereist dat voor alle $x$ in de veilige set:
$$L_f B(x) + \sup_{u \in U} [L_g B(x) u] + \alpha(B(x)) \geq 0$$
De auteurs combineren de lineaire grenzen van de gradient, de dynamica en de control-term tot een lineair surrogaat ($\phi_{linear}$).

• Als dit lineaire surrogaat voldoet aan de voorwaarden, dan is het originele, niet-lineaire probleem ook opgelost (conservatieve verificatie).
• Dit elimineert de noodzaak voor SMT-solvers die over kwantoren-vrije niet-lineaire reële aritmetica moeten redeneren.

D. Adaptieve Verfijning (Refinement)

Lineaire grenzen kunnen te conservatief zijn op grote domeinen. Om dit op te lossen, gebruiken de auteurs een simpliciale mesh (een verdeling van de ruimte in simplices) in plaats van hyperrechthoeken.

• Als de verificatie op een simplex inconclusief is (de grenzen zijn te los), wordt het simplex opgesplitst langs de langste rand.
• Dit proces wordt parallel uitgevoerd op GPU's, wat de efficiëntie aanzienlijk verhoogt.

---

3. Belangrijkste Bijdragen

1. Nieuwe Verificatiemethode: Een raamwerk dat LBP en McCormick-relaxatie combineert om lineaire grenzen te construeren voor zowel de output als de gradienten van neurale netwerken. Dit maakt verificatie mogelijk zonder dure SMT-solvers.
2. Ondersteuning voor Willekeurige Activaties: De methode werkt met elke semidifferentieerbare activatiefunctie (bijv. tanh, sigmoid, ReLU), in tegenstelling tot eerdere methoden die vaak beperkt waren tot ReLU.
3. Parallelle Verfijning: Een strategie die adaptief de ruimte opdeelt in simplices en deze parallel verwerkt, waardoor de conservatisme van de grenzen wordt verminderd en grotere netwerken kunnen worden geverifieerd.
4. Integratie van Controle: De methode houdt expliciet rekening met de controle-input $u$ in de invariantievoorwaarde, wat essentieel is voor toepassingen zoals veiligheidsfilters.

---

4. Experimentele Resultaten

De auteurs hebben hun methode getest op diverse benchmarks uit de literatuur (zoals Darboux, Barrier 2-4) en nieuwe benchmarks (2D-Control, Cart-Pole).

• Schaalbaarheid: De methode slaagt erin neurale netwerken te verifiëren die aanzienlijk groter zijn dan wat mogelijk is met state-of-the-art SMT-methoden (zoals dreal).
  • Voorbeeld: Voor het "Barrier 4" netwerk ([64, 64]) was de SMT-methode (dreal) na 635 seconden nog niet klaar (timeout), terwijl de voorgestelde methode dit in 25,37 seconden verifieerde.
  • Voor het complexere "Darboux" netwerk ([128, 256, 128]) slaagde de methode in 144 seconden, terwijl dreal opnieuw faalde.
• Efficiëntie: De verificatie-tijden zijn aanzienlijk lager, zelfs voor systemen met hoge dimensies en complexe niet-lineariteiten.
• Correctheid: In alle geteste gevallen werd 100% van de veilige set geverifieerd als geldig, wat aantoont dat de methode geen valse positieven produceert (het is conservatief).

---

5. Betekenis en Conclusie

Dit paper biedt een doorbraak in het veld van veiligheidsverificatie voor AI-gestuurde controlesystemen. Door de afhankelijkheid van trage SMT-solvers te doorbreken en te vertrouwen op lineaire relaxaties en parallelle berekening, maken de auteurs het mogelijk om grotere en expressievere neurale netwerken veilig te gebruiken in kritieke toepassingen.

De methode is niet alleen sneller, maar ook flexibeler omdat deze werkt met diverse activatiefuncties die beter geschikt zijn voor het modelleren van complexe fysieke systemen. Dit opent de deur voor het gebruik van geavanceerde "learner-verifier" frameworks in de praktijk, waar grotere netwerken kunnen worden getraind en vervolgens snel en betrouwbaar kunnen worden geverifieerd.

Toekomstige werk: De auteurs noemen dat ze van plan zijn het raamwerk uit te breiden naar andere specificaties dan alleen invariantie, zoals bereikbaarheid (reachability) en vermijding (avoidance).