Incremental Neural Network Verification via Learned Conflicts

Dit paper introduceert een incrementele verificatietechniek voor neurale netwerken die geleerde conflicten hergebruikt over gerelateerde queries heen om redundantie te verminderen en verificatiesnelheid tot 1,9 keer te verhogen.

De kern

Hier is een uitleg van het paper "Incremental Neural Network Verification via Learned Conflicts" in simpele, alledaagse taal, met behulp van creatieve vergelijkingen.

Het Grote Probleem: De Vergeten Lijstjes

Stel je voor dat je een gigantisch, complex labyrint moet verkennen om te bewijzen dat er geen monster in zit. Dit labyrint is een neuraal netwerk (de "hersenen" van een AI). Om te bewijzen dat het veilig is, moeten we alle mogelijke routes door het labyrint controleren.

In het verleden deden onderzoekers dit zo:

1. Ze begonnen bij de ingang en probeerden een route.
2. Als ze een doodlopende weg vonden (een "gevaarlijke" route die niet werkt), schreven ze dit op.
3. Maar toen ze de volgende route probeerden, gooiden ze hun notitieblok weg en begonnen ze helemaal opnieuw.
4. Ze liepen dus keer op keer dezelfde dode hoeken in, terwijl ze eigenlijk al wisten dat die niet werkten.

Dit is heel inefficiënt. Het is alsof je elke dag een nieuwe route naar je werk probeert, maar elke keer vergeet dat je gisteren al wist dat de weg bij de supermarkt dicht is.

De Oplossing: "Geleerde Conflicten" (De Slimme Notities)

De auteurs van dit paper hebben een slimme truc bedacht: Incrementele Verificatie via Geleerde Conflicten.

In plaats van elke keer opnieuw te beginnen, houden ze een slim dagboek bij.

• Het Conflict: Als ze een route vinden die onmogelijk is (bijvoorbeeld: "Als je linksaf slaat én rechtsaf, dan botst je tegen een muur"), noteren ze dit als een regel: "Links + Rechts = Geen goeie route."
• De Hergebruik: Als ze de volgende dag een nieuwe route moeten controleren, kijken ze eerst in hun dagboek. Als de nieuwe route ook "Links + Rechts" bevat, weten ze direct: "Ah, dit is onmogelijk, ik hoef dit niet eens te proberen!" Ze kunnen die hele tak van de zoektocht overslaan.

Hoe werkt dit in de praktijk?

Het paper beschrijft drie situaties waar deze truc heel goed werkt:

1. De Robuustheidstest (De "Stresstest")

Stel je voor dat je wilt weten hoe sterk een auto is. Je duwt er eerst heel zachtjes tegenaan (kleine verstoring), en als hij niet breekt, duw je harder (grotere verstoring).

• Oude manier: Elke keer opnieuw testen alsof je nog nooit hebt geduwd.
• Nieuwe manier: Als je weet dat de auto al breekt bij een duw van 10 kg, dan weet je automatisch dat hij ook breekt bij 15 kg. Je hoeft de 15 kg-test niet eens te doen; je gebruikt de kennis van de 10 kg-test.
• Resultaat: Ze vinden sneller de grens van hoe sterk de AI is.

2. Het Opdelen van de Taak (De "Puzzel")

Soms is het labyrint zo groot dat je het niet in één keer kunt zien. Dan splitsen onderzoekers het op in kleinere stukjes (zoals een puzzel in stukjes snijden).

• Oude manier: Als je een stukje puzzel oplost en ziet dat het niet past, gooi je die kennis weg als je naar het volgende stukje kijkt.
• Nieuwe manier: Als je in het grote stukje ziet dat een bepaalde hoek niet past, weet je dat die hoek ook niet past in de kleinere stukjes die daaruit komen. Je gebruikt die kennis direct om tijd te besparen bij het oplossen van de kleinere stukjes.
• Resultaat: Ze vinden sneller of de puzzel oplosbaar is.

3. De Uitleg (De "Waarom"-vraag)

Soms willen we weten: "Welke pixels op een foto zorgen ervoor dat de AI denkt dat het een hond is?" We proberen features (eigenschappen) weg te halen om te zien of de AI het nog steeds herkent.

• Oude manier: Elke keer opnieuw proberen welke features we kunnen weglaten.
• Nieuwe manier: Als we al hebben bewezen dat "rode kleur" niet belangrijk is voor een bepaalde hond, hoeven we dat niet opnieuw te bewijzen als we een andere hond bekijken die ook rood is. We gebruiken de oude conclusies om sneller de essentie te vinden.
• Resultaat: Ze vinden sneller de belangrijkste kenmerken van een beslissing.

Wat is het resultaat?

Door deze "slimme notities" te gebruiken, besparen ze enorm veel tijd.

• In hun tests waren ze tot 1,9 keer sneller dan de oude methode.
• Het is alsof je een detective bent die een lijstje heeft van alle verkeerde wegen. In plaats van elke weg zelf te lopen, kijkt hij alleen nog maar op zijn lijstje en kan hij direct de goede weg kiezen.

Samenvattend

De kernboodschap is simpel: Leer van je fouten en onthoud ze.
In plaats van elke vraag over een AI-systeem als een compleet nieuwe uitdaging te zien, kijken onderzoekers nu naar de vragen die daarvoor kwamen. Als ze al weten dat iets niet werkt, gebruiken ze die kennis om de volgende vraag sneller te beantwoorden. Dit maakt het controleren van veilige AI-systemen veel sneller en efficiënter.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het artikel "Incremental Neural Network Verification via Learned Conflicts" in het Nederlands.

Probleemstelling

Neurale netwerkverificatie wordt vaak gebruikt als kerncomponent in grotere analyseprocedures, zoals het bepalen van robuustheidsstralen, formele uitlegbaarheid (explainability) en input-splitting. In deze scenario's worden reeksen van sterk gerelateerde verificatievragen over hetzelfde netwerk gegenereerd, waarbij de specificaties (zoals invoer-domeinen of uitvoer-beperkingen) geleidelijk worden verfijnd.

Huidige verificatietools behandelen elke vraag echter als een geïsoleerde taak. Ze starten elke verificatie vanaf nul en verwerpen alle informatie die tijdens eerdere runs is geleerd. Dit leidt tot herhaalde exploratie van dezelfde onhaalbare gebieden in de zoekruimte, wat inefficiënt is en de schaalbaarheid beperkt. Bestaande methoden voor incrementele verificatie richten zich voornamelijk op abstracte interpretatie of het herstarten van zoekbomen, maar er is nog geen systematische aanpak voor het hergebruiken van lemmas (conflicten) binnen volledige, op branch-and-bound gebaseerde verifiers.

Methodologie

Het artikel introduceert een incrementele verificatietechniek die geleerde conflicten (learned conflicts) hergebruikt over gerelateerde verificatievragen heen. De kern van de methode bestaat uit de volgende componenten:

1. Conflicten en Query-Verfijning:

   • Tijdens branch-and-bound verificatie worden onhaalbare combinaties van ReLU-activeringsfasen gedetecteerd. Deze worden vastgelegd als conflictclausules (sets van literals die logisch onverenigbaar zijn binnen een query).
   • De auteurs definiëren een verfijningsrelatie ($q_2 \preceq q_1$): een query $q_2$ is een verfijning van $q_1$ als beide over hetzelfde netwerk gaan en de invoer- en uitvoer-domeinen van $q_2$ een subset zijn van die van $q_1$.
   • Monotonie van Onhaalbaarheid: Een cruciaal theoretisch resultaat is dat als een combinatie van beslissingen onhaalbaar is voor een ruwe query ($q_1$), deze ook onhaalbaar blijft voor elke verfijnde query ($q_2$). Hierdoor kunnen conflicten die voor $q_1$ zijn geleerd, veilig worden overgeërfd naar $q_2$.

2. Incremental Conflict Analyser (ICA):

   • De techniek wordt geïmplementeerd als een module bovenop een bestaande branch-and-bound verifier (in dit geval Marabou).
   • De ICA beheert een pool van conflictclausules en gebruikt een SAT-solver (CaDiCaL) om deze clausules efficiënt te beheren.
   • Werkflow:
     • Bij het starten van een nieuwe query worden alle relevante conflicten uit eerdere runs geladen in de SAT-solver.
     • Tijdens de zoektocht (na standaard numerieke propagatie) voert de verifier een consistentiecheck uit via de SAT-solver met de huidige partiële toewijzing als aannames.
     • Als de SAT-solver "UNSAT" rapporteert, wordt de tak direct afgesneden (gepruned).
     • Als de SAT-solver implicaties (unit propagation) genereert, worden deze toegevoegd als extra grenzen aan de numerieke propagatie, waardoor de zoekruimte verder wordt ingeperd.
     • Nieuw ontdekte conflicten worden opgeslagen voor toekomstige queries.

3. Integratie:

   • De methode is "solver-agnostisch" en kan worden toegevoegd aan elke branch-and-bound verifier. Het is ontworpen als een lichte extensie die de core-reasoning van de solver niet verstoort, maar wel redundantie elimineert.

Belangrijkste Bijdragen

• Formalisatie van Conflict-Overerving: De auteurs bewijzen formeel dat conflicten die voor een query zijn geleerd, geldig blijven voor alle daaropvolgende verfijnde queries. Dit biedt een theoretische basis voor sound conflict reuse.
• Incrementeel Framework: Een nieuw framework dat conflicten opslaat, beheert en toepast via een SAT-solver binnen een branch-and-bound zoekproces.
• Implementatie en Evaluatie: De techniek is geïmplementeerd in de Marabou-verifier en geëvalueerd op drie verschillende use-cases.
• Generaliseerbaarheid: De aanpak is niet beperkt tot specifieke netwerken of taken, maar werkt voor elke reeks gerelateerde queries op een vast netwerk.

Resultaten

De evaluatie is uitgevoerd op drie representatieve verificatietaken:

1. Bepaling van de lokale robuustheidsstraal (Local Robustness Radius):
   • Hierbij worden queries opgebouwd via een binaire zoekopdracht over stralen.
   • Resultaat: Een snelheidswinst van 1,35x (reductie van 315,6s naar 233,5s gemiddeld). Het aantal opgeloste taken nam toe van 160 naar 185 binnen de time-out.
2. Verificatie met Input Splitting:
   • Hierbij wordt het invoer-domein recursief opgesplitst (divide-and-conquer).
   • Resultaat: De grootste prestatieverbetering, met een snelheidswinst van 1,92x (reductie van 84,1s naar 43,9s). De incrementele methode loste alle 491 taken op, terwijl de baseline op twee taken time-out kreeg.
3. Extractie van minimale voldoende feature sets (Formele Uitlegbaarheid):
   • Hierbij wordt gezocht naar de kleinste subset van input-features die de output bepaalt.
   • Resultaat: Hoewel de uiteindelijke grootte van de feature set vergelijkbaar bleef, verbeterde de incrementele methode het anytime-gedrag. Het vond sneller kleinere, voldoende sets door eerder onhaalbare feature-combinaties te verwijderen.

In alle gevallen leidde het hergebruik van conflicten tot een significante reductie in het aantal benodigde propagaties en een snellere detectie van onhaalbare subproblemen.

Betekenis en Conclusie

Dit werk is significant omdat het een brug slaat tussen de geavanceerde technieken van incrementele SAT/SMT-oplossing en de complexe wereld van neurale netwerkverificatie. Het toont aan dat het hergebruiken van informatie over onhaalbare gebieden (conflicten) een krachtige manier is om de schaalbaarheid van verificatie te verbeteren, vooral in iteratieve analyseprocedures.

De methode biedt een praktische oplossing voor een veelvoorkomend inefficiëntieprobleem in de praktijk: het herstarten van verificaties zonder kennis van eerdere resultaten. Door dit te verhelpen, wordt het mogelijk om complexere en grootschaligere verificatietaken uit te voeren, wat essentieel is voor de veilige implementatie van neurale netwerken in kritieke systemen. De auteurs benadrukken dat toekomstig werk zich kan richten op het minimaliseren van conflicten en het gebruik van conflicten om de branching-strategie te sturen.