OpenAI-wiskundebewijzen: 372 AI-resultaten op GitHub

OpenAI heeft 372 nieuwe wiskundige resultaten vrijgegeven die door een van zijn interne frontiermodellen zijn gemaakt. Het bedrijf stuurde ze niet naar wetenschappelijke tijdschriften. In plaats daarvan zette het ze allemaal in een openbare GitHub-repository, samen met revisielogs en bronvermeldingen. Volgens het bedrijf lost elk resultaat een open probleem op of zet het een flinke stap richting een oplossing.

De verzameling is breed. Sommige resultaten verbeteren belangrijke computeralgoritmen. Andere hebben betrekking op de Riemann-hypothese, een van de bekendste onopgeloste problemen in de wiskunde. Volgens OpenAI heeft hetzelfde model al een oplossing voor een Navier-Stokes-probleem opgeleverd, en die oplossing wordt al weken formeel beoordeeld.

Eén prompt, één agent, drie uur

Vooral de werkwijze springt in het oog. Volgens OpenAI kwam bijna elk resultaat voort uit één enkele prompt aan één enkele AI-agent, al waren er soms meerdere pogingen nodig. Per resultaat ging er gemiddeld ongeveer drie uur rekenkracht van ChatGPT Pro Thinking in zitten.

Het Navier-Stokes-werk zag er heel anders uit. Daarvoor was een zwerm van 10.000 agents nodig en miljoenen dollars aan rekenkracht. De nieuwe reeks wijst erop dat de kosten per resultaat sterk zijn gedaald, in elk geval voor de problemen die OpenAI zelf uitkoos.

OpenAI publiceerde ook toelichtingen op zijn methode:

samenvattingen van het redeneerproces van het model
statistieken over het aantal problemen dat het model heeft geprobeerd
schattingen van de rekenkosten

Lean als snelle route voor controle

Veel van de bewijzen worden geleverd met formaliseringen in Lean, een programmeertaal voor wiskundige bewijzen die een computer kan controleren. OpenAI zegt dat er meer formaliseringen aankomen.

De reden is praktisch. Honderden door AI gegenereerde bewijzen kunnen de capaciteit van wiskundigen om ze met de hand te controleren al snel overstijgen. Andere vakgebieden liepen tegen vergelijkbare problemen aan. Google zette bijvoorbeeld een open source bug bounty stop nadat het werd overspoeld met door AI gegenereerde meldingen. Met machinaal controleerbare bewijzen probeert OpenAI zo'n knelpunt in de wiskunde te voorkomen.

Tijdschriften overgeslagen

De keuze voor GitHub in plaats van tijdschriften met peerreview zegt iets. Ze suggereert dat de traditionele academische publicatieweg te traag is voor zo'n hoeveelheid mogelijk nieuwe resultaten.

OpenAI raadpleegde de Advisory Group on Mathematics and Artificial Intelligence van het Institute for Advanced Study (IAS), het onderzoekscentrum in Princeton. Fields-medaillewinnaar Timothy Gowers is een van de leden. OpenAI volgde de openbare aanbevelingen van de groep maar losjes. Het publiceerde geen van zijn prompts en deelde alleen gemiddelde rekenkosten in plaats van cijfers per probleem.

Het bedrijf stelde bovendien vooraf een grens. De wiskundigen mochten adviseren over hoe de resultaten werden gecommuniceerd, maar niet over de vraag of ze werden geproduceerd of hoe snel.

OpenAI zegt workshops en conferenties te gaan financieren die zich richten op het begrijpen van door AI gemaakte resultaten. Het geeft toe dat de bronvermeldingen en de presentatie beter moeten. Ook zegt het een verantwoorde release van het model voor te bereiden om "wetenschappers rechtstreeks te voorzien van de modernste mogelijkheden."

Correct is niet hetzelfde als betekenisvol

Lean kan bevestigen dat een bewijs logisch klopt. Het kan niet vaststellen of een resultaat origineel is of wiskundig van belang. OpenAI gokt erop dat zijn resultaten de grenzen van de menselijke kennis verleggen. Of wiskundigen dat ook vinden, is nog onduidelijk, en de eerste reacties lopen uiteen van enthousiasme tot frustratie.

Enkele van de meest vooraanstaande figuren in het vak hebben al hun zorgen geuit. In een open brief met de titel "A Severe Misalignment of AI in Mathematics" beschreven 25 Fields-medaillewinnaars een diepe kloof tussen de doelen van de AI-industrie en die van de wiskunde. Volgens hen is het oplossen van problemen slechts een middel en een graadmeter. Het echte doel is conceptueel begrip en inzicht. Ze betoogden dat het massaal produceren van ware uitspraken vruchtbare grond zou kunnen vernietigen in plaats van nieuwe ideeën op te leveren, en dat de schade zich naar andere vakgebieden zou uitbreiden.

Gowers waarschuwde dat de wiskundige literatuur binnen tien tot twintig jaar enorm kan groeien, terwijl er geen menselijke gemeenschap meer is die haar echt begrijpt. Terence Tao, eveneens Fields-medaillewinnaar, zei dat de opleiding van jonge wiskundigen de menselijke kant van het vak moet benadrukken en het gebruik van AI-tools streng moet beperken, zodat echt leren en begrijpen blijven bestaan.

Onze kijk

Deze release lijkt net zo goed over het proces te gaan als over de wiskunde. Eén agent die per probleem drie uur draait, verandert de economie van het produceren van bewijzen. Als die kosten zo blijven, zal de productie sneller blijven groeien dan menselijke beoordelaars kunnen bijhouden. Lean helpt bij één deel van het probleem, namelijk de correctheid. De lastigere vragen zijn of een resultaat relevant is en of het origineel is, en die hangen nog steeds af van mensen die nu al overbelast zijn.

Ook de spelregels verdienen aandacht. OpenAI vroeg vooraanstaande wiskundigen om advies, maar liet hen geen invloed uitoefenen op de vraag of en hoe snel het werk werd geproduceerd. Bovendien hield het zijn prompts en de kosten per probleem achter. Daardoor reageert de onderzoeksgemeenschap op de release in plaats van die mee vorm te geven. Elders in de academische wereld duikt vergelijkbare spanning op, zoals bleek uit onze berichtgeving over een MIT-rapport over afbrokkelend vertrouwen onder docenten.

Er zijn een paar dingen om in de gaten te houden:

Of onafhankelijke wiskundigen bevestigen dat een deel van de 372 resultaten echt nieuw en belangrijk is.
Hoe de beoordeling van het Navier-Stokes-werk afloopt.
Of de beloofde modelrelease van OpenAI onderzoekers een tool geeft die ze zelf kunnen sturen, zoals harnassen als BootLoops dat met andere modellen proberen.

Als de release alleen maar bijdraagt aan een ongelezen stapel bewijzen, kan de waarschuwing van de Fields-medaillewinnaars de juistere voorspelling blijken.