Formal Reasoning About Confidence and Automated Verification of Neural Networks

Dit paper introduceert een uniek raamwerk dat door het toevoegen van extra lagen aan neurale netwerken zowel robuustheid als vertrouwen formeel verifieert, wat aanzienlijk beter presteert dan bestaande ad-hoc methoden op een grote reeks benchmarks.

De kern

Titel: Hoe we Neural Networks leren om niet alleen te "zeggen wat", maar ook "hoe zeker ze zijn"

Stel je voor dat een kunstmatige intelligentie (een neurale netwerk) als een zeer snelle, maar soms wat nerveuze taxichauffeur is. Deze chauffeur kan je overal naartoe brengen (bijvoorbeeld een foto herkennen als een "paard" of een "auto"). Maar wat gebeurt er als je de foto een heel klein beetje verwisselt? Misschien een pixel hier, een schaduw daar?

In het verleden hebben onderzoekers zich vooral zorgen gemaakt over de route: "Verandert de chauffeur van bestemming als ik de foto een beetje aanpas?" Als de chauffeur plotseling zegt "Oh, dit is ineens een koe!" terwijl het nog steeds een paard is, dan is het systeem onbetrouwbaar. Dit noemen we robustheid.

Maar er is een groot probleem: de oude methoden keken alleen naar de bestemming, niet naar het zekerheidsgevoel van de chauffeur.

Het Probleem: De Nerveuze Chauffeur

Stel je voor dat de chauffeur een foto van een paard ziet.

1. Scenario A: Hij zegt: "Dit is een paard!" (99% zeker). Dan verandert de foto een beetje, en hij schreeuwt: "Oh nee, dit is een koe!" (99% zeker). Gevaarlijk!
2. Scenario B: Hij zegt: "Dit is een paard!" (99% zeker). Dan verandert de foto een beetje, en hij zegt: "Hmm, dit lijkt op een koe, maar ik ben er maar 10% zeker van." Minder gevaarlijk.

De oude methoden zagen in beide gevallen een "koe" en riepen: "Het systeem is kapot!" Maar in Scenario B is de chauffeur eigenlijk heel voorzichtig. Hij twijfelt. De auteurs van dit paper zeggen: "Wacht even, als hij twijfelt, moeten we hem niet direct afvuren. We moeten kijken naar zijn zekerheid."

De Oplossing: Een Nieuwe Grammatica en Extra Laagjes

De onderzoekers (Afzal, Akshay, Genest en Gupta) hebben een slimme manier bedacht om dit "zekerheidsgevoel" in de wiskunde van de computer te vertalen.

1. De Grammatica (De Regels van het Spel)
Ze hebben een soort "taal" of grammatica bedacht waarmee je allerlei vragen kunt stellen aan de AI.

• Vraag 1: "Verandert de naam van het dier?" (De oude vraag).
• Vraag 2: "Verandert de naam, TENZIJ de zekerheid onder de 80% zakt?" (De nieuwe, slimme vraag).
• Vraag 3: "Zakt de zekerheid van de naam, zelfs als de naam hetzelfde blijft?" (Bijvoorbeeld: Hij blijft "paard" zeggen, maar was eerst 99% zeker en nu 20%. Dat is ook gevaarlijk!).

2. De "Truc" met Extra Laagjes (Het Magische Toevoegsel)
Het grootste probleem was dat de bestaande "testers" (verificatietools) niet konden omgaan met deze complexe zinnen over zekerheid. Ze waren gemaakt voor simpele ja/nee-vragen.

De auteurs hebben een ingenieuze oplossing gevonden: Ze bouwen een extra laag aan de AI.
Stel je voor dat je een robot hebt die alleen "Ja" of "Nee" kan zeggen. Je wilt dat hij ook "Misschien" kan zeggen. In plaats van de robot te herschrijven (wat heel moeilijk en duur is), plak je een extra blok (een paar extra lagen) achter de robot.

• Dit extra blok doet de zware rekenwerk: het berekent de "zekerheid" (de softmax-functie, die wiskundig heel lastig is).
• Het zet die berekening om in een simpele "Ja/Nee" signaal dat de oude robottester kan begrijpen.
• Het resultaat: Je kunt nu elke bestaande, superkrachtige tester gebruiken om deze nieuwe, complexe vragen te beantwoorden, zonder dat je de tester zelf hoeft aan te passen. Het is alsof je een vertaler tussen de robot en de tester plakt.

Waarom is dit geweldig? (De Experimenten)

Ze hebben dit getest op een enorme hoeveelheid tests (8.870 benchmarks!), van simpele cijfers herkennen tot complexe auto's en verkeersborden.

• Snelheid: Hun methode was veel sneller dan de oude, handmatige manieren om dit te testen.
• Grootte: Het werkte zelfs op gigantische netwerken met 138 miljoen parameters (zoals die gebruikt worden in moderne AI).
• Resultaat: Ze ontdekten dat veel netwerken die de oude testers als "gevaarlijk" bestempelden, eigenlijk best veilig waren, zolang ze maar twijfelden bij de verkeerde antwoorden. En ze vonden ook netwerken die "veilig" leken, maar waarvan de zekerheid zo instabiel was dat ze toch gevaarlijk waren.

Samenvattend in één zin

De auteurs hebben een slimme "plug-in" bedacht die het mogelijk maakt om bestaande AI-testers te gebruiken om te kijken of een AI niet alleen het juiste antwoord geeft, maar ook weet hoe zeker ze daarover is, waardoor we veiliger en slimmere AI-systemen kunnen bouwen.

Het is als het geven van een "twijfel-knop" aan een robot, zodat hij niet alleen roept "Ik weet het!", maar ook fluistert "Ik denk het wel, maar ik ben niet 100% zeker", en we dat verschil kunnen meten en controleren.

Technische samenvatting

Probleemstelling

Neurale netwerken worden steeds vaker ingezet in veiligheidskritieke toepassingen (zoals autonoom rijden en medische diagnose). Een bekend probleem is dat kleine verstoringen in de invoer (adversarial examples) kunnen leiden tot verkeerde classificaties. Hoewel er veel werk is gedaan aan het verifiëren van robustheid (de eigenschap dat de uitkomst niet verandert bij kleine invoerveranderingen), negeren de meeste bestaande methoden de betrouwbaarheid (confidence) van het netwerk.

De huidige benaderingen behandelen classificaties vaak als binair (juist/fout) en negeren de waarschijnlijkheid (confidence) die door de softmax-functie wordt gegenereerd. Dit leidt tot twee belangrijke lacunes:

1. Te strikte robustheid: Een netwerk wordt als "niet-robust" bestempeld als er een verkeerde classificatie optreedt, zelfs als de betrouwbaarheid van die fout extreem laag is.
2. Te zwakke robustheid: Een netwerk kan als "robust" worden beschouwd omdat de label niet verandert, terwijl de betrouwbaarheid van de juiste classificatie drastisch daalt bij kleine verstoringen.

Daarnaast is het technisch moeilijk om complexe eigenschappen (zoals combinaties van betrouwbaarheidsdrempels en logische voorwaarden) direct te verifiëren met state-of-the-art tools. Veel verifiers zijn geoptimaliseerd voor simpele post-condities (lineaire ongelijkheden) en hebben moeite met complexe Boolese combinaties of niet-lineaire functies zoals softmax.

Methodologie

De auteurs stellen een unificerend raamwerk voor dat drie hoofdcomponenten combineert:

1. Een Expressieve Grammatica voor Specificaties
Ze definiëren een grammatica die het redeneren over betrouwbaarheid en robustheid generaliseert. Deze grammatica ondersteunt:

• Lineaire Expressies (LE): Lineaire combinaties van logit-waarden.
• Betrouwbaarheidsbeperkingen (CC): Voorwaarden gebaseerd op de softmax-uitvoer (bijv. Conf(y, t) > b).
• Post-condities (PC): Boolese combinaties (AND, OR) van bovenstaande elementen.
  Dit maakt het mogelijk om diverse varianten van robustheid te specificeren, zoals Relaxed Robustness, Strong Robustness, Smoothness en Top-k Robustness.

2. Approximatie van de Softmax-functie
Omdat de softmax-functie niet-lineair is (exponentieel) en niet direct in lineaire verifiers kan worden verwerkt, stellen de auteurs een lineaire rational arithmetic (LRA) approximatie voor.

• Ze benaderen de betrouwbaarheidsvoorwaarden door de logit-waarden te vergelijken met de maximale logit-waarde van de andere klassen.
• Ze introduceren een parameter $\delta$ die afhangt van de gewenste drempelwaarde ($\tau$).
• Deze transformatie garandeert soundness: als de geapproximeerde lineaire voorwaarde geldt, geldt ook de oorspronkelijke betrouwbaarheidsvoorwaarde (met een bekende foutmarge).

3. Encoding via Toegevoegde Netwerklagen
Dit is de kerninnovatie van het artikel. In plaats van de verifiersoftware aan te passen om complexe post-condities te begrijpen, voegen ze een paar extra lagen toe aan het neurale netwerk zelf.

• De complexe post-conditie (de Boolese combinatie van lineaire en betrouwbaarheidsvoorwaarden) wordt vertaald naar een circuit van extra neurale lagen.
• Ze gebruiken ReLU-activaties om logische operaties (AND, OR) te modelleren.
• Een innovatieve "flip"-operatie wordt gebruikt om signalen om te draaien, zodat de output van een conjunctie (AND) correct kan worden gevoed als input voor een disjunctie (OR) en vice versa, zonder de structuur van de verifier te hoeven wijzigen.
• Het resultaat is een nieuw netwerk $N'$ met een vereenvoudigde post-conditie (bijv. y > 0), die door elke bestaande state-of-the-art verifier (zoals $\alpha\beta$-CROWN of Marabou) als een "black box" kan worden verwerkt.

Belangrijkste Bijdragen

1. Generalisatie van Robustheid: Een unificerend raamwerk dat bestaande concepten (zoals strong en top-k robustness) en nieuwe concepten (zoals relaxed robustness met confidence-drempels) in één grammatica verenigt.
2. Formele Softmax-approximatie: Een methode om de niet-lineaire softmax-functie om te zetten in lineaire beperkingen met formele garanties op de foutmarge.
3. Universele Encoding-techniek: Een techniek die complexe eigenschappen omzet in extra netwerklagen. Dit elimineert de noodzaak om de broncode van verifiers aan te passen en maakt het mogelijk om geavanceerde eigenschappen te verifiëren met bestaande tools.
4. Uitgebreide Experimentele Evaluatie: Tests op een grote set van 8.870 benchmarks (van MNIST tot ImageNet met 138 miljoen parameters), inclusief diverse netwerktypes en robustheidsvarianten.

Resultaten

De experimenten tonen aan dat de voorgestelde methode aanzienlijk beter presteert dan bestaande "ad-hoc" benaderingen:

• Efficiëntie: De aanpak met toegevoegde lagen, gecombineerd met de verifier $\alpha\beta$-CROWN, overtreft zowel de constraint-based solver Marabou (met ad-hoc encoding) als Marabou met de eigen lagen-encoding.
• Schaalbaarheid: De methode slaagt erin om grote netwerken (tot 13,16 miljoen niet-lineaire eenheden) te verifiëren voor complexe eigenschappen die eerder onmogelijk of zeer traag waren om te verifiëren.
• Aanpassingsvermogen: De methode werkt effectief voor alle geteste varianten (Relaxed, Strong, Smoothness, Top-k), waarbij de timeout-ratio's laag blijven, zelfs op uitdagende datasets zoals CIFAR-10 en GTSRB.
• Inzicht: De experimenten tonen aan dat het negeren van betrouwbaarheid leidt tot een overschatting van de kwetsbaarheid van netwerken (veel "foute" classificaties hebben zo'n lage betrouwbaarheid dat ze in de praktijk acceptabel zijn).

Significantie

Dit werk is significant omdat het een brug slaat tussen de theoretische complexiteit van betrouwbaarheidsverificatie en de praktische beperkingen van huidige verificatietools.

• Het democratiseert geavanceerde verificatie: gebruikers hoeven geen experts te zijn in de interne werking van complexe verifiers; ze hoeven alleen hun eigenschap te specificeren en het systeem voegt automatisch de benodigde lagen toe.
• Het introduceert een realistischere definitie van veiligheid voor neurale netwerken in kritieke systemen, waarbij niet alleen de label, maar ook de zekerheid van het model een rol speelt.
• Het biedt een standaardisatie voor het specificeren en verifiëren van een breed scala aan robustheidseigenschappen, wat essentieel is voor de verdere adoptie van AI in veiligheidskritieke domeinen.