OpenAI slapp over 700 matematikkbevis på én dag – Lean sjekker rundt 42 prosent av dem

Hva som faktisk ble sluppet

Repoet openai/math inneholder i dag 721 manuskripter, ordnet i 373 «familier». En familie samler et hovedresultat med varianter, følgeresultater og alternative bevis, så antallet ulike problemer er altså rundt 370, ikke over 700. Tre manuskripter ble trukket tilbake dagen etter på grunn av en fortegnsfeil, og flere er rettet siden.

Resultatene dekker tallteori, kombinatorikk, teoretisk informatikk og matematisk fysikk. Blant dem er arbeid knyttet til Riemann-hypotesen og kjente problemer fra Erdős-samlingen. Alt er lisensiert under Apache 2.0.

OpenAI kaller selv manuskriptene «rådata fra forskning» heller enn ferdige artikler, og skriver at selskapet overlater til matematikerne å avgjøre hvem som skal ha æren. Ingen av dem er fagfellevurdert.

Slik ble de laget

Ifølge OpenAI startet det som en vanlig modellevaluering. De eksisterende matteprøvene var blitt for lette, så selskapet begynte å gi modellen åpne forskningsproblemer i stedet. Totalt fikk den rundt 4 000 problemer.

Hvert resultat brukte i snitt tre timer tenketid på ChatGPT Pro-nivå. Det er ikke ett raskt svar, men en lang tankekjede der modellen prøver, feiler og bygger videre, og noen resultater bygger på det modellen selv har funnet tidligere. Etterpå ble svarene sortert, gruppert og silt etter hvor betydningsfulle de var. To av de største resultatene, blant dem et om nullpunktfrie områder for Riemanns zetafunksjon, ble ikke laget med standardoppsettet, og ett av dem er redigert av mennesker for å bli lettere å lese.

Det er altså ikke slik at noen spurte en chatbot og fikk et bevis. Det er tusenvis av timer regnekraft, en lang trakt av utvelgelse og en modell som ikke er tilgjengelig for andre.

Lean: maskinen som sjekker beviset

Råteksten vi fikk inn sier at «over en fjerdedel» av bevisene er sjekket i Lean, og at de dermed «definitivt holder vann». Begge delene trenger en korreksjon.

Lean er et programmeringsspråk og en bevisassistent der et bevis skrives så presist at en datamaskin kan sjekke hvert eneste steg. Godtar Lean beviset, er det ingen logiske hull i det. Ifølge repoet er rundt 42 prosent av hovedresultatene formalisert på denne måten, altså godt over en fjerdedel.

Men Lean sjekker bare at beviset holder for den påstanden som er skrevet inn i Lean. Om den formelle påstanden faktisk er den samme som det manuskriptet hevder, må fortsatt et menneske vurdere. Lean sier heller ingenting om resultatet er nytt, eller om det bare fullfører noe andre allerede var i gang med. De resterende rundt 58 prosentene har ingen maskinell sjekk i det hele tatt, og OpenAI skriver selv at noen av dem kan inneholde feil.

Det er likevel denne kombinasjonen som er det egentlig nye. En språkmodell er god til å finne ideer, men kan ta feil med stor selvsikkerhet. Lean er nådeløst presis, men finner ingenting selv. Sammen får du et system der AI-en foreslår og maskinen kontrollerer. Det samme prinsippet ser vi i kodeagenter som kjører tester før de leverer.

Kritikken

Terence Tao, en av verdens mest kjente matematikere, har vært blant de skarpeste kritikerne. Han har omtalt ett av Riemann-resultatene som det største framskrittet på problemet på femti år. Samtidig kaller han det respektløst at forskere som jobbet med de samme problemene ikke fikk noen forvarsel, og at unge forskere så prosjektene sine bli overkjørt over natta. Han peker også på at de som stiller modellen spørsmål, ikke nødvendigvis forstår eller kan forklare bevisene.

Andre matematikere har kalt enkelte manuskripter nesten uleselige uten AI-hjelp, og en talsperson for OpenAI har innrømmet overfor Scientific American at selskapets egne matematikere ennå ikke forstår mange av resultatene. Flere har også bedt om tilgang til modellen og promptene, uten å få det. Uten det kan ingen utenfor OpenAI gjenta forsøket.

Det er en interessant kontrast til det Tao selv beskrev i våren, da han brukte AI som matematikkollega i et åpent samarbeid der mennesker forsto og kontrollerte hvert steg. Det OpenAI har gjort, er det motsatte: hundrevis av resultater på én gang, og så får fagfeltet rydde opp.

Hva betyr det?

Påstander om at dette er «den største dagen i matematikkens historie» er det for tidlig å ta stilling til. Det vil ta måneder, kanskje år, før matematikerne har gått gjennom alt. Noen resultater vil holde, noen vil vise seg å være små utvidelser av kjent arbeid, og noen kan inneholde feil.

Men metoden er verdt å merke seg. Lange tenkeøkter, maskinell bevissjekk og massiv utvelgelse er en oppskrift som ikke er begrenset til matematikk. Alt som kan sjekkes automatisk, enten det er bevis, kode eller kretsdesign, er et felt der AI kan prøve tusen ganger og bare levere det som består kontrollen. Det store spørsmålet er hvordan resten av oss skal forholde oss til resultater som verken er fagfellevurdert eller forstått av dem som publiserte dem.

Ressurser

• openai/math på GitHub – manuskriptene, Lean-bevisene og beskrivelse av metoden
• Lean – bevisassistenten som brukes til å sjekke bevisene
• Scientific American – reaksjoner fra matematikere
• Fortune – bakgrunn og kritikk
• Tech Insider om Lean-andelen – hva de 42 prosentene betyr