Et kodelager, ikke en artikkel

OpenAI publiserte 6. oktober en katalog med matematiske resultater laget av det selskapet kaller en intern frontmodell, og la alt i et GitHub-lager i stedet for å sende det til tidsskrifter. Katalogen rommer 722 manuskripter ordnet i 372 resultatfamilier, der en familie samler et hovedresultat med følgeargumenter, konsekvenser eller alternative bevis.

Selskapet oppgir at arbeidet kom ut av modellutviklingen og ikke av et eget forskningsprogram. “Som en del av modellutviklingen evaluerer vi modellene våre på åpne forskningsproblemer”, står det i lagerets introduksjonsfil. “Vi utvidet disse evalueringene etter at ytelsen på våre eksisterende matematiske evalueringer ble mettet.”

Hva tallene sier om beregningen

OpenAI oppgav mer om metoden enn vanlig. Gjennom evalueringen ble omkring 4 000 problemer stilt til modellen. Det gjennomsnittlige publiserte resultatet krevde tilsvarende rundt tre timers resonneringsberegning i ChatGPT Pro. Å samle utdataene i familier og manuskripter, med krav om det OpenAI kaller et passende betydningsnivå, gav tallet 722.

To poster ble behandlet annerledes. Arbeidet med en nullfri region for Riemanns zetafunksjon og et bevis for Hodges formodning for abelske varieteter med kompleks multiplikasjon falt utenfor den faste framgangsmåten, og OpenAI oppgir at teksten om zetaresultatet — som gjelder området der realdelen av s overstiger 11/12 — ble redigert av et menneske for lesbarhetens skyld.

En liten bunke tomme hvite papirark på et linstoff
Mange manuskripter har Lean-formaliseringer; OpenAI oppgir at ikke alle har det. Illustrasjonsbilde. https://kaboompics.com/ · pexels · Pexels License

Forbeholdene står i lageret, ikke i bloggposten

Samlingen inneholder resultater på ulike verifiseringsstadier. Mange manuskripter har formaliseringer i Lean, et språk som lar en datamaskin kontrollere et bevis, men ikke alle. OpenAI skriver rett ut at “noen av de uformaliserte resultatene kan ha problemer”, og sier at de rettes raskt når de blir funnet, med formaliseringer lagt til lageret fortløpende.

Den innrammingen betyr noe, fordi det er selskapet selv og ikke en fagfelle som avgjør hva som er betydelig nok til å publiseres. OpenAI oppgir å ha rådført seg med den uavhengige rådgivende gruppen for matematikk og kunstig intelligens ved Institute for Advanced Study om god praksis, og å ha bygget på gruppens råd og offentlige anbefalinger da den bestemte hvordan resultatene skulle slippes.

Ti resonneringssammendrag

Ved siden av manuskriptene slapp OpenAI forkortede sammendrag av modellens resonnement for ti resultater, blant dem irrasjonalitetseksponenten for pi, de symmetriske og generelle Mahler-formodningene, kvasipolynomiske grenser for aritmetiske følger, Kaplanskys formodning om direkte endelighet i karakteristikk to og det tredimensjonale relativistiske Vlasov-Maxwell-systemet. Selskapet publiserte også siteringsanvisninger per manuskript og sa at slippehistorikken bevares, med rettelser registrert som nye versjoner.

Et skrivebord med matematikkbok, passer, linjal, kalkulator og håndskrevne utregninger
Selskapet oppgir at hvert publiserte resultat krevde rundt tre timers ChatGPT Pro-beregning. Illustrasjonsbilde. MART PRODUCTION · pexels · Pexels License

Hva som er verdt å følge

Modellen som laget alt dette, er ikke tilgjengelig. OpenAI sier at selskapet “arbeider med å slippe modellen som produserte disse resultatene på en ansvarlig måte”, og at det vil finansiere en rekke verksteder, konferanser og særskilte programmer om å forstå store resultater laget av KI, med detaljer senere.

Den praktiske prøven er nå Lean-biblioteket. Formaliserte bevis kan kontrolleres maskinelt av hvem som helst; uformaliserte manuskripter må leses av matematikere, og 722 er mye lesing. Hvor fort formaliseringskatalogen fylles — og hvor mange uformaliserte resultater som tåler kontakt med fagfeltet — sier mer enn tallet i tittelen.