Googles KI løste matteproblemer som hadde stått åpne i 56 år for noen hundre dollar

Et forskningssystem fra Google DeepMind har laget fullstendige, maskinkontrollerte bevis for ni åpne problemer som matematikeren Paul Erdős en gang stilte, to av dem uløste i 56 år. Det samme systemet avgjorde 44 formodninger hentet fra nettencyklopedien over heltallsfølger, lukket et 15 år gammelt spørsmål i algebraisk geometri og strammet en kjent grense innen konveks optimering. Det iøynefallende tallet betyr mindre enn metoden. Hvert eneste av disse bevisene ble kontrollert av en maskin, ikke bare påstått av en.

Erdős, som døde i 1996, etterlot seg hundrevis av presise og sta spørsmål, mange lette å formulere og brutalt vanskelige å lukke. Gjennom tiår ble de en slags stående eksamen for faget. Følgeformodningene kommer fra en offentlig database som matematikere graver i etter mønstre, der en gjettet formel kan ligge ubevist i årevis. Det er ikke konstruerte testoppgaver laget for å smigre en modell. Det er det reelle etterslepet i den åpne matematikken.

Den forskjellen er hele historien. Systemet, kalt AlphaProof Nexus, skriver argumentene sine i Lean, et formelt språk hvis kompilator forkaster ethvert steg den ikke kan bekrefte. Et bevis går igjennom eller ikke, uten rom for et selvsikkert avsnitt som senere viser seg å være feil. For den som vil avgjøre om en KI-‘oppdagelse’ er virkelig, går grensen her mellom en pressemelding og et resultat.

Anbefalt lesningSuncatcher-gambiten: Innsikt i Googles plan for å erobre KI-fremtiden

Under panseret kjører beviseren på Gemini 3.1 Pro, mens en lettere modell tar seg av rangeringen. Sløyfen er nesten kjedelig. Modellen skisserer et bevis i Lean, kompilatoren sender feilene tilbake, og de feilene mater det neste forsøket. Det som holder den ærlig, er den symbolske tilbakemeldingen, ikke den flytende prosaen. Teamet bygde fire versjoner av økende kompleksitet, én av dem i stand til å frembringe og rangere konkurrerende bevisutkast. Likevel løste den enkleste versjonen, en ren sløyfe av modell og kompilator, alle ni Erdős-problemene på egen hånd.

Økonomien er den stille forbløffende delen. Hvert løste problem kostet noen hundre dollar i beregningstid. Spørsmål som hadde slukt hele karrierer, ble lukket for omtrent prisen på en helgetur. Det pensjonerer ikke matematikeren. Noen må fortsatt velge hvilke problemer som er verdt å angripe, formulere dem i en form systemet kan lese og avgjøre hva et svar betyr. Det som endrer seg, er regnestykket over hva som i det hele tatt er verdt å prøve.

Forbeholdene veier tyngre enn overskriften. Ni løste av 353 forsøkte Erdős-problemer er en treffprosent på rundt 2,5. Følgetallet, 44 av 492, ligger under ni prosent. Forfatterne sier rett ut at de fleste av disse problemene fortsatt er utenfor rekkevidde, ikke minst de som krever omfattende ny teori, og at seirene samler seg der Leans matematikkbibliotek allerede er dypt. Ta bort det menneskebygde stillaset og den utvalgte listen over mål, og systemet har lite å stå på.

Forsiktigheten er fortjent. I en episode som ble grundig latterliggjort, kunngjorde et konkurrerende laboratorium at modellen deres hadde løst ti Erdős-problemer, helt til matematikere påpekte at svarene allerede sto i den publiserte litteraturen. Modellen hadde funnet dem, ikke bevist dem. AlphaProof Nexus er bygd for å være immun mot den feilen. Et Lean-bevis av et kjent resultat er fortsatt et gyldig bevis, og et Lean-bevis av noe genuint nytt kan ikke bløffes fram. Demis Hassabis, som leder DeepMind, var nøye med å si at arbeidet ikke er kunstig generell intelligens, en uvanlig forsiktig merknad fra et selskap som sjelden er beskjedent med modellene sine.

Det finnes en finere gevinst som forskerne fremhever. Selv feilforsøkene var nyttige. Fordi hvert delbevis kontrolleres formelt, kunne matematikere se nøyaktig hvilke delmål systemet kunne og ikke kunne lukke, uten å kontrollere hele argumentet for hånd. Maskinen slutter å være et orakel og blir en utrettelig medarbeider som viser arbeidet sitt og peker på hvor det vanskelige fortsatt gjemmer seg.

Resultatet står ikke alene. Det faller i samme periode som en separat påstand fra en konkurrerende resonneringsmodell, som etter sigende har motbevist en omtrent 80 år gammel Erdős-formodning i diskret geometri, et funn som yrkesaktive matematikere forfinet og stilte seg bak. To laboratorier, to metoder, det ene lent mot formell verifikasjon og det andre mot rå resonnementskjeder, nådde den samme fronten med ukers mellomrom. Konkurransen handler ikke lenger om chatboter som høres smarte ut.

Arbeidet ble lagt fram i en artikkel publisert denne måneden, og metodene hviler på åpne verktøy, nærmere bestemt Lean og dets fellesskapsbygde bibliotek, slik at utenforstående grupper kan inspisere og kjøre bevisene på nytt i stedet for å stole på en selskapsblogg. DeepMind har ikke sagt om systemet når forskere utenfor selskapet. Tallet å følge med på er ikke ni. Det er om de 2,5 prosentene blir ti, og deretter tjue, for den dagen må samtalen om hva disse maskinene er til for, begynne på nytt.

Mer som dette

Intelligensens nye fysikk: Termodynamisk databehandling og slutten på det digitale deterministiske paradigmet

Linus Torvalds slår fast at AI-skrevet kjernekode er det nye normale

Perplexitys Mac-agent koster 200 dollar i måneden og leser e-posten din

Torchlight: Infinite lanserer sesong 12 tre måneder etter sin historiske spillerrekord

WhatsApp lanserer brukernavn — du trenger ikke lenger dele telefonnummeret

Farvel til silisium: Kina avslører ‘LightGen’ – lysprosessoren som utfordrer Nvidia og bryter varmemuren