Tegenvoorbeeld
Een tegenvoorbeeld is één enkel geval dat een algemene bewering onderuithaalt. Stel iemand beweert: "alle zwanen zijn wit." Zolang iedereen alleen witte zwanen ziet, lijkt die uitspraak waar. Maar zodra er ergens één zwarte zwaan opduikt, zoals onderzoekers in Australië in de achttiende eeuw ontdekten, is de hele bewering ontkracht. Die ene zwarte zwaan is het tegenvoorbeeld: niet honderd aanwijzingen voor, maar één keiharde uitzondering is al genoeg om een algemene claim te laten sneuvelen.
In de technologie van de toekomst speelt dit principe een verrassend grote rol. Bedrijven die zelfrijdende auto's, vliegtuigcomputers of kunstmatige intelligentie bouwen, doen voortdurend beweringen als "dit systeem remt altijd op tijd voor voetgangers" of "dit AI-model herkent nooit een stopbord als iets anders." Een tegenvoorbeeld is dan niet zomaar een foutje, maar het specifieke scenario dat bewijst dat zo'n belofte niet klopt. Het opsporen van zulke tegenvoorbeelden, voordat een systeem de weg op gaat of in een ziekenhuis wordt gebruikt, is een van de belangrijkste manieren waarop ingenieurs proberen te garanderen dat nieuwe technologie veilig is.
Wat is het precies?
In de logica en wiskunde gaat het om uitspraken die gelden voor alle gevallen binnen een bepaalde groep, zogeheten universele beweringen. "Voor elk getal x geldt eigenschap P" is zo'n uitspraak. Om te bewijzen dat zo'n claim onwaar is, hoef je niet alle gevallen te doorzoeken: je hoeft maar één x te vinden waarvoor P niet geldt. Dat ene geval is het tegenvoorbeeld. Dit verschilt van een gewone fout of bug, omdat het specifiek gaat om het weerleggen van een algemene, geformuleerde claim.
In de techniek wordt dit idee gebruikt in een vakgebied dat formele verificatie heet. Daarbij schrijven ingenieurs een wiskundig precieze beschrijving van hoe een computerchip, stuk software of protocol zich hoort te gedragen, bijvoorbeeld "dit geheugen raakt nooit twee processen tegelijk kwijt." Een computerprogramma, een zogeheten model checker, doorzoekt vervolgens automatisch alle mogelijke toestanden van het systeem om te kijken of die eis ooit geschonden wordt. Vindt de model checker een uitvoeringspad waarin de eis niet opgaat, dan levert die niet alleen "nee, klopt niet" op, maar ook het exacte tegenvoorbeeld: de precieze stappen die tot de schending leiden. Ingenieurs gebruiken dat spoor om de bug te vinden en te repareren.
Een verwante techniek heet CEGAR, counterexample-guided abstraction refinement. Omdat echte systemen vaak te complex zijn om in één keer volledig te doorzoeken, bouwt de computer eerst een vereenvoudigd, grofmaziger model. Vindt dat vereenvoudigde model een tegenvoorbeeld, dan wordt gecontroleerd of dat tegenvoorbeeld ook in het echte, volledige systeem bestaat. Is dat niet zo, dan was het een vals alarm veroorzaakt door de versimpeling, en wordt het model verfijnd zodat die fout niet opnieuw ontstaat. Zo werkt de software zich stap voor stap naar een steeds nauwkeuriger beeld, totdat er geen tegenvoorbeelden meer te vinden zijn of een echt probleem is blootgelegd.
Bij kunstmatige intelligentie, met name bij neurale netwerken die bijvoorbeeld beelden herkennen, duikt hetzelfde idee op onder een andere naam: het adversarial voorbeeld (tegenstrijdig voorbeeld). Onderzoekers veranderen een foto van een panda met piepkleine, voor mensen onzichtbare ruisvlekjes, waardoor het netwerk plotseling overtuigd is dat het een gibbon ziet. Dat geманipuleerde plaatje is in wezen een tegenvoorbeeld voor de claim "dit model classificeert afbeeldingen correct." Het verschil met klassieke formele verificatie is dat neurale netwerken zo groot en wiskundig ondoorzichtig zijn dat een volledig, sluitend bewijs vaak onhaalbaar is; onderzoekers zoeken daarom naar steekproefsgewijze of statistische garanties in plaats van absolute zekerheid.
Wat wil men ermee bereiken?
De achterliggende drijfveer is vertrouwen. Hoe meer beslissingen we overlaten aan automatische systemen, zoals een vliegtuigcomputer, een chip in een pacemaker of een zelfrijdende auto, hoe groter het belang dat die systemen doen wat ze beloven, zonder verborgen uitzonderingen. Testen door het systeem gewoon te gebruiken en te kijken of het fout gaat, dekt nooit alle mogelijke situaties af: een zelfrijdende auto kan miljoenen kilometers probleemloos rijden en toch in de ene op een miljard situaties een voetganger over het hoofd zien. Formele verificatie en het bewust zoeken naar tegenvoorbeelden proberen juist die zeldzame, gevaarlijke uitzonderingen vooraf bloot te leggen, in plaats van ze pas te ontdekken nadat er iets misgaat in de praktijk.
Een tweede doel is efficiëntie in het ontwikkelproces zelf. Een tegenvoorbeeld wijst niet alleen aan dát er een probleem is, maar ook waar precies, wat voor ingenieurs veel sneller te repareren is dan een vage foutmelding. Tot slot speelt het een rol bij het opbouwen van vertrouwen tussen partijen: toezichthouders, verzekeraars en klanten kunnen een geverifieerd systeem met een wiskundig bewijs van correctheid eerder vertrouwen dan een systeem dat alleen "in de praktijk meestal goed werkte."
Voorbeelden uit de praktijk
Een bekend startpunt is de Pentium FDIV-bug van Intel in 1994: een zeldzame rekenfout in de deelfunctie van de processor, die Intel destijds naar schatting tientallen miljoenen dollars aan terugroepacties kostte. Deze affaire zette de chipindustrie ertoe aan om formele verificatie met model checkers structureel in het ontwerpproces van processoren op te nemen, iets wat bedrijven als Intel en ARM sindsdien standaard doen.
Het besturingssysteemkernel seL4, ontwikkeld door het Australische onderzoeksinstituut NICTA (nu voortgezet door Data61/CSIRO en de seL4 Foundation) en in 2009 gepubliceerd, is wiskundig bewezen correct voor een reeks veiligheidseigenschappen: voor die eigenschappen kon geen enkel tegenvoorbeeld worden gevonden binnen het wiskundige model. Het wordt onder meer gebruikt in defensietoepassingen en veiligheidskritische systemen.
Amazon Web Services gebruikt sinds ongeveer 2011 de formele specificatietaal TLA+, ontwikkeld door informaticus Leslie Lamport, om complexe gedistribueerde systemen zoals S3 en DynamoDB door te rekenen. In een veelgeciteerd artikel uit 2015 beschreef het AWS-team hoe de methode meerdere subtiele fouten aan het licht bracht via concrete tegenvoorbeelden, fouten die met gewoon testen vrijwel zeker gemist zouden zijn.
In het onderzoek naar adversarial voorbeelden publiceerden Ian Goodfellow en collega's in 2014 het invloedrijke artikel "Explaining and Harnessing Adversarial Examples," met de beroemde panda-naar-gibbon-demonstratie. Dat werk opende een heel onderzoeksveld naar hoe kwetsbaar beeldherkenningsmodellen zijn voor minuscule, doelbewust gekozen verstoringen.
Recenter liet DeepMind in 2024 met AlphaProof en AlphaGeometry zien hoe geautomatiseerde bewijssystemen, die intern voortdurend kandidaat-oplossingen toetsen en verwerpen op basis van tegenvoorbeelden, wiskundeopgaven op het niveau van de Internationale Wiskunde Olympiade konden oplossen, een gebied waar het vinden en uitsluiten van tegenvoorbeelden een kernonderdeel van het bewijsproces is.
Hoe ver is de techniek?
Voor digitale hardware, zoals processoren en geheugenchips, is formele verificatie met model checking inmiddels volwassen technologie en standaardpraktijk bij grote fabrikanten. Voor klassieke software is de techniek ook behoorlijk ver ontwikkeld, met compilers als CompCert die bewezen correct zijn en kernels als seL4 die in de praktijk worden ingezet, al blijft het arbeidsintensief en daarom vooral voorbehouden aan systemen waar falen catastrofale gevolgen kan hebben.
Bij neurale netwerken en moderne AI-modellen ligt dat anders. Wiskundig gezien is het volledig verifiëren van een groot neuraal netwerk een extreem zwaar probleem, in de informatica aangeduid als NP-hard, waardoor exacte garanties vaak alleen haalbaar zijn voor kleinere netwerken of beperkte eigenschappen. Tools als Marabou en alpha-beta-CROWN kunnen gedeeltelijke, begrensde garanties geven, bijvoorbeeld "binnen deze kleine afwijking van de oorspronkelijke foto verandert de classificatie niet," maar een volledig sluitend bewijs voor een heel groot taalmodel is met de huidige technieken niet haalbaar. Het zoeken naar adversarial tegenvoorbeelden blijft daardoor een kat-en-muisspel: onderzoekers vinden nieuwe aanvallen, ontwikkelaars bouwen verdedigingen, en vervolgens duiken er weer nieuwe tegenvoorbeelden op die die verdediging omzeilen. Een harde, voor eens en altijd afgesloten oplossing is er nog niet.
Wie werken eraan?
Op het gebied van formele verificatie van hardware en software lopen Intel en ARM voorop binnen de chipindustrie, terwijl Amazon via zijn formele-methodengroep TLA+ breed inzet bij AWS. Het Franse onderzoeksinstituut INRIA ontwikkelt en onderhoudt de bewijsassistent Coq, een van de belangrijkste gereedschappen wereldwijd voor wiskundig geverifieerde software. In Australië bouwde NICTA (opgegaan in Data61/CSIRO) de seL4-kernel, nu beheerd door de onafhankelijke seL4 Foundation. Universiteiten als Carnegie Mellon, Stanford, MIT en Oxford hebben gespecialiseerde onderzoeksgroepen voor formele methoden en programmaverificatie.
Op het gebied van AI-robuustheid en adversarial voorbeelden zijn onderzoeksgroepen bij Google DeepMind, OpenAI en universitaire labs (onder meer rond de voormalige Goodfellow-onderzoekslijn) toonaangevend. De jaarlijkse conferentie Computer Aided Verification (CAV) geldt als het belangrijkste podium waar wetenschappers uit al deze hoeken hun werk presenteren en vergelijken.