OpenAI legger ut 722 KI-genererte matematikkmanuskripter på GitHub, mange med Lean-bevis

722 manuskripter, ordnet i 372 familier, ligger nå i repoet openai/math, opprettet 6. oktober. Ifølge OpenAI ble modellen stilt rundt 4000 problemer under evalueringen, og hvert resultat brukte i snitt tilsvarende tre timers tenketid med ChatGPT Pro. Katalogen er det som sto igjen etter at OpenAI samlet resultatene i familier og krevde et visst nivå av betydning.

Repoet har PDF-er og kildefiler, et Lean-bibliotek som formaliserer mange, men ikke alle, resultatene, og forkortede sammendrag av modellens resonnering for ti av dem, blant annet irrasjonalitetseksponenten til π og Kaplanskys direkte-endelighetsformodning i karakteristikk to.

«Noen av de uformaliserte resultatene kan ha feil. Vi vil forsøke å rette slike feil raskt» — OpenAI, i README-fila til repoet

Formen på utgivelsen er et svar til Advisory Group on Mathematics and Artificial Intelligence ved Institute for Advanced Study. Rådet publiserte anbefalinger 29. september etter over 600 svar fra matematikere, og ba om modellnavn, prompter, sammendrag av resonnering, tidsbruk og beregningskostnad for hvert resultat. OpenAI leverer deler av dette, men modellen er fortsatt navnløs, og resonneringen er bare lagt ut for ti familier. Rådet ba også om at resultatene legges i arkiver som ikke kontrolleres av noe KI-laboratorium. OpenAI bruker sitt eget GitHub-repo og skriver at de ser etter fellesskapsdrevne alternativer.

Saken fikk 1233 poeng på Hacker News, der kommentarfeltet delte seg mellom glede over at resultatene ligger fritt på GitHub og irritasjon over at OpenAI måtte presses til å lytte.

For deg som bygger, er Lean-biblioteket den delen du faktisk kan kjøre. README-en anbefaler å kompilere små deler om gangen, og et fullt bygg kan feile på Linux hvis vm.max_map_count er satt for lavt. OpenAI skriver at selskapet jobber med å slippe modellen som produserte resultatene.