OpenAI trekt drie wiskundige onderzoeksartikelen van zijn AI-model terug. Een tekenfout maakte een bewijs ongeldig en ondermijnde ook twee andere artikelen die daarop voortbouwden. De correctie volgt één dag nadat het bedrijf honderden wiskundige AI-resultaten openbaar maakte.
Met de
publicatie van zijn wiskundige onderzoeksresultaten geeft OpenAI wetenschappers toegang tot manuscripten en computercontroleerbare bewijzen. Het bedrijf wil daarmee nieuwe kennis beschikbaar maken. De eerste correcties laten tegelijk zien hoeveel er afhangt van de controle: onderzoekers moeten niet alleen afzonderlijke bewijzen beoordelen, maar ook nagaan welke resultaten op elkaar steunen.
Hoe raakt één fout drie onderzoeksartikelen?
OpenAI beschrijft de oorzaak in zijn
overzicht van correcties en intrekkingen. Het manuscript Algebraicity of Weil classes on split abelian eightfolds bevatte een tekenfout die een cruciale bewijsstap ongeldig maakte. Twee andere artikelen gebruikten dezelfde wiskundige constructie. Daardoor trof de fout niet één los resultaat, maar een keten van argumenten.
Het bedrijf herzag daarnaast veertien andere manuscripten. OpenAI herstelde onder meer bewijsstappen, corrigeerde stellingen en verduidelijkte voorwaarden. Bij de ingetrokken artikelen staan toelichtingen op de ontbrekende onderbouwing. Eerdere versies blijven toegankelijk, zodat onderzoekers kunnen volgen wat het bedrijf heeft aangepast.
Een ongeldig bewijs maakt de bijbehorende stelling overigens niet automatisch onwaar. Het betekent dat de aangeleverde redenering de conclusie niet bewijst. Een ander argument kan die conclusie later alsnog onderbouwen. Omgekeerd maakt een overtuigend geschreven onderzoeksartikel een wiskundige claim nog niet correct.
Wat heeft de wiskundige AI van OpenAI onderzocht?
De
actuele catalogus van OpenAI bevat 719 manuscripten, verdeeld over 372 families. Iedere familie groepeert verwante artikelen, zoals een hoofdresultaat, aanvullende argumenten en alternatieve bewijzen. De collectie telt dus geen 719 afzonderlijk opgeloste problemen.
OpenAI legde het interne model ongeveer 4.000 problemen voor. Vervolgens bundelde het bedrijf verwante uitkomsten en selecteerde het resultaten op wetenschappelijke betekenis. Sommige uitkomsten bouwen bovendien voort op eerder werk van de modellen.
Die werkwijze maakt een eenvoudig slagingspercentage misleidend. Het aantal voorgelegde problemen en het aantal gepubliceerde manuscripten meten verschillende dingen. Ze vertellen zonder aanvullende informatie niet welk deel van de oorspronkelijke vragen het model correct oploste.
OpenAI vergelijkt het gemiddelde computergebruik per resultaat met ongeveer drie uur denken in
ChatGPT Pro. Die vergelijking beschrijft de gebruikte rekenkracht. Het bedrijf belooft daarmee niet dat een publiek ChatGPT-abonnement dezelfde problemen binnen drie uur oplost. OpenAI publiceert ook tien samenvattingen van de modelredeneringen om meer inzicht te geven in de onderzoeksaanpak.
AI Wereld berichtte eerder over een afzonderlijk
wiskundig experiment met GPT-5 Pro in de convex optimalisatie. De nieuwe collectie verbreedt het materiaal dat onderzoekers kunnen bestuderen: van een individuele proef naar honderden samenhangende manuscripten.
Hoe controleert Lean de wiskundige bewijzen?
OpenAI meldt dat ongeveer 42 procent van de hoofdresultaten inmiddels een formalisering heeft. Daarbij legt het bedrijf stellingen en bewijsstappen vast in een precieze computertaal. De
bewijsassistent Lean kan vervolgens controleren of de conclusie logisch volgt uit de vastgelegde definities en uitgangspunten.
Dat verschilt wezenlijk van een AI-model vragen of een antwoord klopt. Lean beoordeelt geen overtuigende formuleringen, maar controleert formele bewijsstappen. De software biedt daarmee een manier om wiskundige argumenten technisch te toetsen.
Wel moeten onderzoekers nagaan wat zo’n controle precies afdekt. OpenAI vermeldt in zijn
instructies voor bewijsverificatie dat sommige controles alleen ondersteunende resultaten toetsen. Ze controleren niet de hoofdstelling van het bijbehorende artikel. Een geldig bewijs voor een bouwsteen is dus nog geen volledig bewijs voor de constructie die daarop rust.
AI Wereld beschreef deze combinatie van oplossingen zoeken en bewijzen formaliseren eerder bij
Aristotle Agent van Harmonic. Zulke systemen richten zich niet alleen op het produceren van antwoorden, maar ook op de controleerbaarheid van hun redeneringen.
Het ontbreken van een formalisering bewijst op zichzelf geen fout. Voor die resultaten ontbreekt alleen deze specifieke vorm van softwarecontrole. OpenAI waarschuwt dat ongeformaliseerde resultaten problemen kunnen bevatten en zegt aanvullende formaliseringen te publiceren zodra die beschikbaar komen.
Waarom vragen wiskundigen ook toegang tot het model?
De onafhankelijke Advisory Group on Mathematics and Artificial Intelligence, afgekort AGMAI, adviseerde OpenAI over de publicatie. In zijn
verklaring van 6 oktober trekt de groep een duidelijke grens: zijn betrokkenheid geeft de resultaten geen wetenschappelijk keurmerk. De wiskundige gemeenschap moet zelf hun betekenis beoordelen.
De adviesgroep wil bovendien voorkomen dat wetenschappers vooral achter AI-bedrijven aan werken. Wiskundigen moeten eigen vragen kunnen stellen, eigen methoden ontwikkelen en
onderzoek doen buiten de onderwerpen die een bedrijf selecteert om een model te demonstreren. Daarvoor hebben zij toegang tot krachtige systemen en voldoende rekenmiddelen nodig.
In zijn
aanbevelingen voor verantwoorde publicatie vraagt AGMAI AI-labs zelfs te stoppen met het testen van geavanceerde wiskundige problemen op modellen die de bredere wetenschappelijke gemeenschap niet kan gebruiken. De groep waarschuwt dat zulke verschillen een tweedeling kunnen creëren tussen AI-bedrijven en andere onderzoeksinstellingen.
AGMAI vraagt daarnaast om leesbare bewijzen, zorgvuldige literatuurverwijzingen en onafhankelijke onderzoeksarchieven. De groep baseerde zijn aanbevelingen mede op ruim 600 reacties uit de wiskundige gemeenschap. Wetenschappelijke openheid draait daarmee niet alleen om bestanden beschikbaar stellen, maar ook om de mogelijkheid voor anderen om het werk te begrijpen en erop voort te bouwen.
OpenAI zegt workshops, conferenties en andere onderzoeksprogramma’s te financieren die dat begrip moeten vergroten. Het bedrijf werkt ook aan een verantwoorde vrijgave van het gebruikte model. Een releasedatum noemt het niet. Onderzoekers kunnen voorlopig dus wel de gepubliceerde uitkomsten bestuderen, maar nog niet met hetzelfde model hun eigen onderzoeksvragen verkennen.