Zo temt AWS de onvoorspelbaarheid van AI

Byron Cook is een expert op het zeldzame gebied van formele geautomatiseerde bewijsvoering: het zoeken naar bewijzen binnen de wiskundige logica. Bij AWS behandelen Cook en zijn team computerprogramma's, configuraties en netwerkbeleid als wiskundige objecten. Hierdoor kunnen ze redeneren over alle mogelijke uitvoeringen, invoergegevens en beveiligingsinstellingen.

"Net zoals Euclides redeneerde over alle mogelijke rechthoekige driehoeken terwijl hij de stelling van Pythagoras bewees, kunnen wij hetzelfde doen met softwareprogramma's," legt Cook uit. Deze techniek werd historisch gezien vooral gebruikt in sectoren waar de belangen extreem hoog zijn, zoals de lucht- en ruimtevaart (bijvoorbeeld na de explosie van de Ariane 5-raket), maar vormt nu de kern van de beveiliging van AWS.

De cloudinfrastructuur beveiligen

AWS zet geautomatiseerd redeneren in om de correctheid van zijn meest kritieke componenten te bewijzen, waaronder cryptografie en virtualisatie-infrastructuur.

Cook wees op de recente aankondiging van een nieuwe AWS-hypervisor (de Nitro Instance-engine) waarvan de correctheid formeel is bewezen. Bovendien hebben klanten direct toegang tot deze tools om hun eigen IAM-beleid en EC2-netwerkinstellingen door te lichten. Dit zorgt ervoor dat hun beleid correct en veilig is nog voordat het wordt uitgerold.

Cook benadrukt de tastbare voordelen:

Snellere ontwikkeling: Formele verificatie vermindert de noodzaak voor het terugdraaien van code (rollbacks) aanzienlijk. Het Amazon S3-team kan hierdoor nieuwe functies tot vier keer sneller implementeren.

Kostenbesparing: Het proces leidt vaak tot snellere programma's. Zo is de nieuwe 'policy interpreter' van AWS (die miljarden keren per seconde wordt aangeroepen) nu drie keer sneller, wat leidt tot aanzienlijke kostenbesparingen.

Klantvertrouwen: Organisaties die obsedeeerd zijn door veiligheid, zoals financiële reuzen Bridgewater Associates en Goldman Sachs, waren vroege gebruikers. Deze techniek stelde hen in staat om met een gerust hart bedrijfskritische workloads naar de cloud te verplaatsen.

Het temmen van het gevaar van Agentic AI

Hoewel formeel redeneren altijd complex en duur was en zeldzame specialisten vereiste, ziet Cook nu een enorme verschuiving: generatieve AI blijkt uitstekend in staat om deze tools aan te sturen.

Volgens Cook zorgt de combinatie van GenAI-tools met gevestigde 'theorem provers' (zoals de Lean-bewijshulp die wordt gebruikt door wiskundigen als Terence Tao) voor een snelle daling van de kosten en een hogere wendbaarheid van formele verificatie. Dit is cruciaal nu bedrijven Agentic AI omarmen.

"Als je autonome agents acties laat ondernemen zonder menselijk toezicht... dan zijn dat beslissingen waar je niet op terug kunt komen (one-way door decisions). Je wilt er dan absoluut zeker van zijn dat ze correct zijn," waarschuwt Cook.

Hij trekt een parallel tussen het bewijzen van AWS-beleid en het garanderen dat een AI-agent nauwkeurige antwoorden geeft over complexe regelgeving. Statistische methoden zoals "LLM as a judge" kunnen simpelweg de noodzakelijke correctheid niet garanderen. Hierdoor is formeel redeneren de essentiële ruggengraat voor betrouwbare, autonome agents in gevoelige sectoren zoals de geneeskunde, de financiële wereld en de advocatuur.

De toekomst van wetenschappelijke ontdekkingen

Op de vraag hoe ver we verwijderd zijn van AI die fundamentele wetenschap bedrijft, is Cook optimistisch. Op het gebied van de zuivere wiskunde zijn we er volgens hem al. Hij haalt een recent complex wiskundig vraagstuk (een Erdős-probleem) aan dat deze week werd opgelost door een combinatie van GenAI en bewijshulpmiddelen.

Cook deelde ook zijn eerdere werk waarbij hij geautomatiseerd redeneren gebruikte om genetische regulatietrajecten te modelleren, wat leidde tot de ontdekking van medicijnen die momenteel klinisch worden getest. Hij gelooft dat Agentic AI een groot deel van deze workflow kan automatiseren: van het genereren van initiële hypothesen tot het afhandelen van complexe documentatie voor toezichthouders.

"Deze redeneertools lossen problemen op die geen enkele verzameling mensen ooit zou kunnen oplossen," concludeert Cook. Hij ziet de combinatie van geavanceerde statistische AI en strikte wiskundige bewijsvoering als dé weg voorwaarts voor de verdere schaling van AI.