De Amerikaanse start-up Axiom Math heeft het Stacks Project formeel geverifieerd. Dat is een van de grootste wiskundige naslagwerken die ooit door mensen is geschreven. De AI-agents van het bedrijf zetten de ongeveer 7.654 pagina's om in zo'n 16 miljoen regels code die een computer controleert.
Het Stacks Project begon in 2005 als open naslagwerk van de Columbia-wiskundige Johan de Jong. Sindsdien hebben wiskundigen er resultaten aan toegevoegd, van algebra op universitair beginniveau tot de meest geavanceerde ideeën in algebra, meetkunde en getaltheorie.
Wat formeel verifiëren is
Bij formalisering schrijf je een wiskundig bewijs opnieuw op als code, in de programmeertaal Lean. Een zogeheten bewijsassistent controleert die code regel voor regel. Komt het bewijs erdoor, dan weet je dat de logica klopt. Dezelfde techniek wordt gebruikt om chipontwerpen te controleren, en in Frankrijk vonden onderzoekers er fouten mee in software die kinderbijslag berekent.
Bij Stacks was dat extra lastig, omdat alle stellingen en definities op elkaar voortbouwen. Al die verbanden moesten in de miljoenen regels code intact blijven. Volgens Axiom werkten de agents grotendeels parallel en zochten ze zelf uit welke taken ze konden oppakken. Het bedrijf trainde daarnaast eigen modellen die goed zijn in wiskunde.
Tegenwicht voor 'AI-slop' in de wiskunde
De timing is niet toevallig. AI-bedrijven claimen in hoog tempo oplossingen voor beroemde vraagstukken. Volgens TechCrunch publiceerde OpenAI vorige maand alleen al 719 manuscripten met zulke claims. Eerder schreven we over OpenAI's claim van drie doorbraken en over de kritiek dat het bedrijf zelf kiest wie die doorbraken mag controleren. Formeel geverifieerde wiskunde maakt zulke controles minder afhankelijk van menselijke beoordelaars.
Volgens Axiom vult de verificatie een groot gat: algebraïsche meetkunde was tot nu toe nauwelijks in Lean beschikbaar. Elk gecontroleerd resultaat wordt een bouwsteen waar nieuwe bewijzen op kunnen leunen.
Ook bedoeld voor software
Axiom mikt niet alleen op wiskundigen. Het bedrijf, dat zegt 1,6 miljard dollar waard te zijn, wil een betrouwbare basis bouwen waarop AI-agents software en uiteindelijk wetenschap kunnen bouwen. Nu AI steeds meer code schrijft, groeit de vraag hoe je zeker weet dat die code klopt. Ook andere start-ups zien daar kansen in, zoals we eerder schreven over formele verificatie als antwoord op onveilige AI-code.
Topvrouw Carina Hong (25) daagt de grote programmeerbedrijven uit om formalisering op deze schaal ook te proberen. Of andere onderzoekers de Lean-versie van Stacks gaan gebruiken, moet nog blijken.
