OpenAIs Astra setter matematikkverdenen på prøve

Hvilke problemer skal Astra ha tatt for seg?

Resultatene dekker et uvanlig bredt spekter av fagområder: høydimensjonal geometri, kodeteori, aritmetisk kretskompleksitet, gruppeteori, operatoralgebraer, kvantekompleksitet, gitterkryptografi og ekstremal kombinatorikk .

1. Pakking av kuler i høye dimensjoner – nye øvre grenser for tettheten ved kulepakking, ned mot Cohn–Elkies-grensen .
2. Binære og sfæriske koder – eksponentielt forbedrede grenser for hvor mange koder som kan finnes ved en gitt minimumsavstand .
3. Ikke-sofiske grupper – en eksplisitt konstruksjon som viser at slike grupper finnes, et sentralt åpent spørsmål i gruppeteori .
4. Connes’ rigiditetsformodning – en tilbakevisning av en langvarig formodning om von Neumann-algebraer .
5. Aritmetisk kretskompleksitet – nye nedre grenser for beregning av permanenten, blant annet en formelgrense av størrelsesorden n⁴/log n .
6. Kvantebasert parallell repetisjon – en eksponentiell parallellrepetisjonsteorem for generelle kvantespill mellom to spillere .
7. Nærmeste vektor-problemet – vanskelighet ved approksimering med polynomisk faktor, et grunnleggende problem for postkvantekryptografi .
8. Ehrharts volumformodning – det maksimale volumet til en konveks kropp der tyngdepunktet er det eneste indre gitterpunktet .
9. Ramsey-tall med flere farger – en supereksponentiell nedre grense som løser Erdős-problem 183 .
10. Formodninger om ekstremale tall – resultater om formodninger knyttet til kompaktitet og degenerasjon, som løser Erdős-problem 146 og 180 .

Lean-bevisene: Den viktigste delen av utspillet

OpenAI har ikke offentliggjort selve Astra-modellen. I stedet har selskapet lagt ut Lean 4-bevissertifikater på GitHub under Apache 2.0-lisensen . Oppbevaringsstedet skal ha en «sorry»-telling på null. I Lean betyr dette at ingen trinn er markert som uferdige eller tatt på tillit – alle formaliserte deler av de ti bevisene skal være maskinverifisert .

Det er en vesentlig forskjell fra vanlig KI-generert tekst. En språkmodell kan skrive et overbevisende, men feilaktig matematisk argument. En bevisassistent som Lean godtar derimot bare argumenter som oppfyller systemets formelle regler. Det sier ikke nødvendigvis alt om hvordan resultatet ble oppdaget, men det gjør selve den formaliserte argumentasjonen langt enklere å kontrollere.

Ifølge OpenAI brukte menneskelige forskere den samme modellen til å utarbeide de endelige manuskriptene .

Matematikkmiljøet er imponert – og skeptisk

Reaksjonene har vært delte. Forskere som Noam Brown har omtalt kunngjøringen som et viktig steg for vitenskapelig resonnering . Samtidig har kritikere pekt på flere begrensninger.

Dette er ikke Millennium-prisproblemene

Ingen av de ti problemene er blant Clay Mathematics Institutes sju Millennium-prisproblemer, som for eksempel P mot NP eller Riemann-hypotesen . Det gjør ikke problemene uviktige, men det setter overskriftene i perspektiv. En eksplisitt konstruksjon av en ikke-sofisk gruppe vil i så fall løse et spørsmål som har stått siden Mikhail Gromov introduserte begrepet sofisitet i 1999 .

Ingen fagfellevurdering ennå

Resultatene ble offentliggjort direkte av OpenAI, uten at de først var publisert i et fagfellevurdert matematisk tidsskrift eller på en konferanse . Kritikere mener derfor at det fortsatt er uklart hvor grensen går mellom KI-generert oppdagelse, menneskelig tolkning og redaksjonell innramming. OpenAI har selv vist til Leiden-erklæringen om KI og matematikk i omtalen av denne spenningen .

Kan matematikkprestasjoner overføres til annen vitenskap?

Kognisjonsforsker Gary Marcus har argumentert for at suksess i formell matematikk kan være et «spesialtilfelle» som ikke uten videre overføres til bredere vitenskapelig resonnering . Matematikk har en særstilling fordi svarene ofte kan kontrolleres symbolsk, og fordi man kan produsere store mengder syntetiske treningsdata med garantert korrekte svar. Slik er det ikke i de fleste andre vitenskapsfelt.

Astra er fortsatt utilgjengelig

Siden modellen ikke er lansert, og OpenAI ikke har offentliggjort hele metoden for hvordan oppgavene ble løst, kan utenforstående ikke gjenskape selve prosessen uavhengig . Lean-filene gjør bevisene mer etterprøvbare, men de løser ikke spørsmålet om hvilke instrukser, søkestrategier eller menneskelige bidrag som lå bak resultatene.

Timingen vekker spørsmål

Kunngjøringen kom samtidig som OpenAI posisjonerer Astra som sin neste store modellfamilie. Det har fått enkelte kritikere til å spørre om utspillet først og fremst var lagt opp for markedsføring, eller om det var presentert med den vitenskapelige grundigheten som kreves av et forskningsresultat .

Hva betyr dette egentlig?

Dersom argumentene består en grundig ekspertkontroll, kan flere av resultatene lukke spørsmål som har vært åpne i tiår. Den mest omtalte prestasjonen – den første eksplisitte konstruksjonen av en ikke-sofisk gruppe – vil i så fall løse et problem som har vært åpent i over 25 år . Selv skeptikere erkjenner at OpenAI har lagt frem langt mer materiale som kan undersøkes, enn det som er vanlig i en typisk selskapskunngjøring .

Men den store testen handler ikke bare om hvorvidt Astra kan gjøre avansert matematikk. Spørsmålet er om ferdigheter i formelle og verifiserbare problemer kan overføres til generell vitenskapelig forskning. Det har OpenAI foreløpig ikke bevist.