OpenAI bracht recent honderden beweerde oplossingen voor moeilijke wiskundeproblemen naar buiten. Dat trok veel aandacht, maar ook kritiek van wiskundigen die zeggen dat de resultaten nog niet voldoen aan de gebruikelijke vakstandaarden.

Wat OpenAI heeft gepubliceerd

OpenAI maakte honderden manuscripten met zogenoemde oplossingen vrij. Het bedrijf zegt dat het advies kreeg van een groep vooraanstaande wiskundigen, de Advisory Group on Mathematics and Artificial Intelligence (AGMAI), die is verbonden aan het Institute for Advanced Studies in Princeton. AGMAI gaf richtlijnen voor hoe laboratoria moeten handelen bij het oplossen van lastige wiskundevragen.

Toch zitten er directe verschillen tussen wat AGMAI vroeg en wat OpenAI deed. Een van AGMAI’s eerste aanbevelingen was om te stoppen met het testen van zeer geavanceerde wiskundige problemen op zogeheten proprietary modellen — modellen waarvan de code of trainingdata niet openbaar zijn. OpenAI publiceerde juist resultaten van zijn eigen, niet-openbare modellen.

Bovendien gaf OpenAI weinig inzicht in het denkproces van de modellen. Van de 719 vrijgegeven manuscripten toonde slechts 10 de zogenoemde chain-of-thought, het stappenplan of de redenering die het model gebruikte om tot een oplossing te komen.

Waar wiskundigen zich zorgen over maken

Experts zeggen dat wiskunde niet alleen draait om een eindantwoord; het gaat om begrip en controle door mensen. AGMAI benadrukte dat resultaten zo moeten worden gepresenteerd dat andere wiskundigen ze echt kunnen doorgronden, controleren en gebruiken.

Volgens het nieuwsbericht had 42% van de vrijgegeven bewijzen het formalisatieproces niet doorlopen. Formaliseren betekent hier dat een bewijs is omgezet naar een vorm die door speciale software gecontroleerd kan worden, zodat de juistheid met veel minder twijfel kan worden vastgesteld.

AGMAI stelde ook dat OpenAI moet bijdragen aan het werk van menselijke wiskundigen die de AI-oplossingen begrijpelijk en bruikbaar maken. Zonder die menselijke betrokkenheid blijft er twijfel over de juistheid en de betekenis van de resultaten.

De gerenommeerde wiskundige Terence Tao waarschuwde dat AI-prompters vaak alleen gericht zijn op het behalen van een resultaat en daarna geen betrokkenheid tonen bij het veld. Zij begrijpen het AI-resultaat mogelijk niet goed genoeg om vragen te beantwoorden, lezingen te geven of de oplossing te plaatsen in het bredere wiskundige werk.

Het probleem met automatisch formaliseren

Een recent wetenschappelijk artikel van onderzoekers aan de University of Cambridge en King’s College London laat zien waar het mis kan gaan. De onderzoekers vergeleken de natuurlijke-taalversie van een bewijs (de uitleg in gewone tekst) met de formele versie die OpenAI in Lean maakte.

Lean is een programmeertaal die gebruikt wordt om wiskundige bewijzen formeel te beschrijven en zo automatisch te controleren of ze logisch kloppen. Het idee is dat een correct Lean-programma aantoont dat een bewijs klopt.

De onderzoekers vonden minstens twee gevallen waarin de menselijke uitleg en de Lean-code niet volledig overeenkwamen. Zulke misvertalingen bewijzen niet automatisch dat een bewijs fout is, maar ze laten wel zien dat een AI niet altijd betrouwbaar zichzelf kan controleren.

AGMAI vroeg OpenAI ook om machine-leesbare metadata die de koppeling tussen de natuurlijke taal en de formele artefacten laat zien. Die metadata ontbreken bij deze vrijgaven. Zonder die koppeling is het lastiger voor andere wiskundigen om snel te zien of de formele versie echt hetzelfde zegt als de uitleg in gewone woorden.

De auteurs van het artikel concluderen dat automatisch geformaliseerde bewijzen niet blind vertrouwd moeten worden zonder dezelfde peer review en controle die gebruikelijk is bij menselijke bewijzen.

Conclusie

OpenAI heeft een omvangrijke stap gezet door veel mogelijke oplossingen vrij te geven. Tegelijkertijd benadrukken wiskundigen dat publicatie alleen niet genoeg is: er moet menselijk begrip en grondige controle volgen.

Belangrijke punten zijn:

• Veel vrijgegeven bewijzen missen inzicht in het modeldenken: slechts 10 van 719 toonden chain-of-thought.

• Een groot deel van de bewijzen is niet formeel gecontroleerd; 42% heeft het formalisatieproces niet doorlopen.

• Onderzoekers vonden discrepanties tussen de gewone taaluitleg en de formele Lean-versies, wat vragen oproept over automatische vertaling.

• AGMAI vroeg expliciet om meer transparantie en om steun voor menselijke wiskundigen die de resultaten moeten verifiëren.

Voor nu blijft het duidelijk dat AI veel kan bijdragen, maar dat mensen nodig blijven om de conclusies betrouwbaar te maken en te plaatsen binnen het vakgebied.