Amazon past wiskundige bewijsvoering toe op AI-systemen

TL;DR

• Wat: Amazon's Automated Reasoning Group gebruikt wiskundige bewijsvoering — eerder ingezet om cloudinfrastructuur waterdicht te maken — nu ook om AI-uitvoer te controleren op correctheid.
• Waarom relevant: als ondernemer die AI inzet voor klantcontact of beslissingen, wil je weten of het antwoord klopt — niet 'waarschijnlijk klopt'.
• Wat je ermee kunt: houd in de gaten of jouw AI-tooling (bijv. via AWS Bedrock) gebruik maakt van geautomatiseerde verificatie, en vraag je leverancier ernaar.

Ik stuitte op een post van Amazon Science die me aan het denken zette. Het team dat jarenlang wiskundig heeft bewezen dat de beveiliging van Amazon's cloud correct werkt, richt zich nu op AI. Wat mij triggerde: dit gaat niet over nóg een AI-feature, maar over een fundamenteel andere manier om te controleren of AI-systemen betrouwbare antwoorden geven.

Wat is automated reasoning eigenlijk?

Automated reasoning — geautomatiseerde bewijsvoering — klinkt abstract, maar het idee is eigenlijk simpel. In plaats van software te testen door er duizenden scenario's tegenaan te gooien (zoals je een auto zou testen door er eindeloos mee te rijden), bewijs je wiskundig dat de software zich in alle gevallen correct gedraagt. Vergelijk het met het verschil tussen "we hebben honderd keer gecontroleerd of het slot dicht zit" en "we hebben wiskundig bewezen dat het slot onmogelijk open kan zonder sleutel".

Amazon heeft hier een heel team voor: de Automated Reasoning Group. Onder leiding van Byron Cook werken zij al ruim tien jaar aan dit soort wiskundige garanties voor AWS-systemen. Cook zei het eerder dit jaar treffend in een interview op All Things Distributed: het team heeft een decennium besteed aan het bewijzen van de correctheid van "authorization engines, cryptographic implementations, and virtualization layers".

Wat hebben ze tot nu toe bewezen?

Drie resultaten springen eruit, en ze geven een aardig beeld van de reikwijdte.

De Nitro Isolation Engine

Dit is misschien het meest indrukwekkende voorbeeld. De Nitro Isolation Engine is het onderdeel van Amazon's cloud dat ervoor zorgt dat virtuele machines van verschillende klanten écht gescheiden blijven. Denk aan een flatgebouw waar de muren wiskundig gegarandeerd geluiddicht zijn — niet omdat je het getest hebt, maar omdat het bewezen is.

Het team schreef 330.000 regels aan wiskundige bewijsvoering in een tool genaamd Isabelle/HOL. Die bewijzen dekken vertrouwelijkheid, integriteit, geheugenveiligheid en functionele correctheid. Het resultaat: de eerste formeel geverifieerde hypervisor die commercieel in een cloudomgeving draait. Sinds juni 2026 is dit standaard actief voor bepaalde EC2-instanties.

Cryptografische code

De cryptografische implementaties die AWS gebruikt voor versleuteling zijn op dezelfde manier doorgelicht. Ik vind het eerlijk gezegd bijzonder dat een bedrijf dit soort investeringen doet — wiskundige bewijsvoering is tijdrovend en duur, maar het levert een niveau van zekerheid op dat testen simpelweg niet kan bieden.

Amazon S3 (ShardStore)

Ook de opslaglaag van S3 — het systeem waar een enorm deel van het internet zijn bestanden bewaart — is gevalideerd met formele methoden. Het team paste een aanpak toe die ze "lightweight formal methods" noemen: een pragmatische variant waarbij je de correctheid opsplitst in onafhankelijke eigenschappen en elke eigenschap met het meest geschikte gereedschap controleert. Dit leverde zestien bugs op die met traditioneel testen zeer moeilijk te vinden waren geweest.

De stap naar AI

En nu dus AI. Wat mij hier opvalt is de richting: het gaat niet om het bouwen van betere AI-modellen, maar om het controleren van wat AI-modellen zéggen. Amazon noemt dit "neurosymbolic AI" — een combinatie van neurale netwerken (de AI die tekst genereert) en symbolische logica (de wiskunde die controleert of die tekst klopt).

Concreet is dit vertaald naar Automated Reasoning checks in Amazon Bedrock Guardrails. Bedrock is Amazon's platform voor generatieve AI. De Guardrails-functie controleert de uitvoer van taalmodellen met wiskundige methoden in plaats van alleen statistische steekproeven. Volgens Amazon levert dit tot 99% nauwkeurigheid op bij het detecteren van correcte antwoorden.

Byron Cook stelt het scherp: "Would you trust an agentic investment system to move money in and out of your bank accounts?" Zijn punt is dat vertrouwen dé barrière is voor het inzetten van AI bij serieuze bedrijfsbeslissingen. En dat vertrouwen bouw je niet met beloftes, maar met bewijzen.

Wat betekent dit voor je bedrijf?

Ik denk dat hier iets zit dat relevant is voor elke ondernemer die AI inzet of overweegt. Het gaat om de vraag: hoe weet je of het antwoord dat een AI geeft, klopt?

Stel dat je als ondernemer een chatbot inzet die klanten adviseert over verzekeringen, of een AI-tool die facturen controleert. In beide gevallen heeft een fout directe consequenties — financieel, juridisch, of in klantvertrouwen. Tot nu toe was de controle op AI-uitvoer vooral statistisch: je test met voorbeelden en hoopt dat het in de praktijk ook goed gaat. Wiskundige verificatie biedt een fundamenteel ander niveau van zekerheid.

Nu is het eerlijk om te zeggen dat dit voorlopig vooral beschikbaar is via AWS Bedrock, en dat het opzetten van zogenaamde "reasoning policies" (de regels waartegen de AI-uitvoer wordt gecontroleerd) nog behoorlijk wat werk is. Dit is geen knop die je aanzet. Maar het signaal is helder: de grote cloudaanbieders investeren in bewíjsbare correctheid van AI, niet alleen in betere modellen.

Kun je je voorstellen wat dit betekent als je in een gereguleerde sector zit — zorg, finance, juridisch? De mogelijkheid om aan te tonen dat je AI-systeem wiskundig gecontroleerd is, verandert het compliance-gesprek.

Een andere kijk op AI-betrouwbaarheid

Wat ik interessant vind aan deze ontwikkeling is dat het de discussie over AI-betrouwbaarheid verschuift. Het gaat niet meer alleen over "hoe goed is het model" maar over "hoe hard kun je bewijzen dat de uitvoer correct is". Dat is een wezenlijk ander gesprek.

Er zit ook een nuance in die Cook zelf aanstipt: niet elk AI-gebruik vereist dezelfde mate van verificatie. Een AI die gedichten schrijft hoeft niet wiskundig geverifieerd te worden. Maar een AI die financiële adviezen geeft of medische informatie verstrekt — daar is deze aanpak volgens mij precies het juiste niveau van zorgvuldigheid.

Voor mij is dit vooral een signaal dat de AI-industrie langzaam volwassen wordt. De fase van "kijk wat het kan" maakt plaats voor "bewijs dat het klopt". En dat is, wat mij betreft, precies de richting die het op moet.