Et kodelager, ikke en artikel
OpenAI udgav den 6. oktober et katalog over matematiske resultater frembragt af det, firmaet kalder en intern frontmodel, og lagde det hele i et GitHub-lager i stedet for at indsende det til tidsskrifter. Kataloget rummer 722 manuskripter ordnet i 372 resultatfamilier, hvor en familie samler et hovedresultat med følgeargumenter, konsekvenser eller alternative beviser.
Firmaet oplyser, at arbejdet kom ud af modeludviklingen og ikke af et selvstændigt forskningsprogram. “Som en del af modeludviklingen evaluerer vi vores modeller på åbne forskningsproblemer”, står der i lagerets introduktionsfil. “Vi udvidede disse evalueringer, efter at ydelsen på vores eksisterende matematiske evalueringer blev mættet.”
Hvad tallene siger om beregningen
OpenAI oplyste mere om metoden end sædvanligt. Gennem evalueringen blev der stillet omkring 4.000 problemer til modellen. Det gennemsnitlige udgivne resultat krævede svarende til cirka tre timers ræsonnementsberegning i ChatGPT Pro. At samle output i familier og manuskripter og kræve det, OpenAI kalder et passende betydningsniveau, gav tallet 722.
To poster blev behandlet anderledes. Arbejdet med en nulfri region for Riemanns zetafunktion og et bevis for Hodges formodning for abelske varieteter med kompleks multiplikation faldt uden for den faste procedure, og OpenAI oplyser, at teksten om zetaresultatet — der gælder området, hvor realdelen af s overstiger 11/12 — blev redigeret af et menneske af hensyn til læsbarheden.
Forbeholdene står i lageret, ikke i blogindlægget
Samlingen indeholder resultater på forskellige verifikationsstadier. Mange manuskripter har formaliseringer i Lean, et sprog der lader en computer kontrollere et bevis, men ikke alle. OpenAI skriver direkte, at “nogle af de uformaliserede resultater kan have problemer”, og siger, at de rettes hurtigt, når de findes, med formaliseringer føjet til lageret løbende.
Den indramning betyder noget, fordi det er firmaet selv og ikke en bedømmer, der afgør, hvad der er betydeligt nok til at blive udgivet. OpenAI oplyser at have rådført sig med den uafhængige rådgivende gruppe for matematik og kunstig intelligens ved Institute for Advanced Study om god praksis, og at have bygget på gruppens råd og offentlige anbefalinger, da den besluttede, hvordan resultaterne skulle udgives.
Ti ræsonnementsresuméer
Ved siden af manuskripterne udgav OpenAI forkortede resuméer af modellens ræsonnement for ti resultater, blandt dem irrationalitetseksponenten for pi, de symmetriske og generelle Mahler-formodninger, kvasipolynomielle grænser for aritmetiske følger, Kaplanskys formodning om direkte endelighed i karakteristik to og det tredimensionale relativistiske Vlasov-Maxwell-system. Firmaet udgav også citeringsanvisninger per manuskript og sagde, at udgivelseshistorikken bevares, med rettelser registreret som nye versioner.
Hvad der er værd at følge
Modellen, der frembragte alt dette, er ikke tilgængelig. OpenAI siger, at firmaet “arbejder på ansvarligt at udgive modellen, der frembragte disse resultater”, og at det vil finansiere en række workshops, konferencer og særlige programmer om at forstå store resultater frembragt af AI, med detaljer senere.
Den praktiske prøve er nu Lean-biblioteket. Formaliserede beviser kan kontrolleres maskinelt af enhver; uformaliserede manuskripter skal læses af matematikere, og 722 er meget læsning. Hvor hurtigt formaliseringskataloget fyldes — og hvor mange uformaliserede resultater der overlever kontakten med faget — siger mere end tallet i overskriften.
