Husker du da vi snakket om hvordan ChatGPT og andre språkmodeller egentlig bare er avanserte papegøyer? I min gjennomgang av hvordan språkmodeller fungerer, forklarte jeg hvordan de gjetter neste ord basert på sannsynlighet. De forstår egentlig ikke hva de sier; de vet bare hva som statistisk sett høres riktig ut. Det er derfor de kan hallusinere og finne på fakta med den største selvsikkerhet.
Vel, hold på hatten. For Google DeepMind har akkurat knust det argumentet i fillebiter – i hvert fall når det gjelder matematikk.
Nyheten om AlphaProof og AlphaGeometry 2 har nådd meg, og etter å ha dykket ned i dokumentasjonen, må jeg innrømme at selv en nøktern realist som meg kjenner pulsen stige. Vi har nå passert en milepæl mange trodde lå tiår frem i tid: AI har løst oppgaver fra den internasjonale matematikkolympiaden (IMO) på sølvmedalje-nivå. Dette er ikke tekstgenerering. Dette er logisk resonnering på et nivå som får selv verdens smarteste studenter til å svette.
Når maskinen slutter å gjette og begynner å bevise
For å forstå hvor stort dette er, må vi forstå hva IMO faktisk representerer. Dette er ikke barneskolematte. Det er «Matematikkens Olympus». De aller, aller skarpeste unge hjernene i verden konkurrerer her. Oppgavene krever kreativitet, intuisjon og beinhard logikk. Fram til nå har AI-systemer vært «dumme som brød» i møte med disse oppgavene, nettopp fordi de baserer seg på mønstergjenkjenning i tekst, ikke logisk sannhet.
Men DeepMinds nye systemer gjør noe fundamentalt annerledes. De kombinerer en språkmodell med reinforcement learning (forsterkende læring) – den samme typen trening som lærte AlphaGo å slå verdensmestere i brettspill. Jeg har tidligere sett lignende tendenser i hvordan man må jobbe med modeller for å unngå feil, slik jeg beskrev i guiden om hvordan jeg sluttet å krangle med ChatGPT. I stedet for å bare spytte ut tekst, oversetter systemet problemet til et formelt programmeringsspråk som heter Lean.
Dette er genistreken: I Lean er det umulig å bløffe. Enten er beviset matematisk gyldig, eller så kompilerer ikke koden. AlphaProof trener mot seg selv, prøver og feiler millioner av ganger, helt til den finner en løsning som er 100 % verifiserbar. Den «hallusinerer» ikke et svar; den beviser det.
Terence Tao og slutten på «papegøye-argumentet»
Jeg har personlig fulgt med på debatten rundt Meta og deres tilnærming til AI, spesielt med tanke på modeller som forsøker å forstå verden uten bare å bruke ord. Det minner litt om konseptet bak VL-JEPA. Dette gjennombruddet fra Google utfordrer skepsisen til dagens modeller direkte. Når maskinen klarer å løse 5 av 6 ekstremt vanskelige oppgaver i en konkurransesetting, snakker vi om en kognitiv kapasitet som går langt utover autofullfør.
Selv Terence Tao, som kanskje er verdens nålevende smarteste matematiker, har begynt å integrere disse verktøyene i sin egen forskning. Når en Fields-medaljevinner sier at dette vil endre matematikkens natur fundamentalt, bør vi lytte. Han ser for seg en fremtid hvor AI fungerer som en ufeilbarlig assistent som tar seg av de tunge, tekniske bevisene, slik at menneskelige matematikere kan fokusere på de store linjene og konseptene.
Hoppet fra AlphaGeometry 1 til versjon 2 er i seg selv en oppvisning i eksponentiell forbedring. Versjon 2 løser nå geometri-oppgaver bedre enn den gjennomsnittlige gullmedaljevinneren i IMO. Det er en hastighet på utviklingen som er vanskelig å ta inn over seg.
Hva betyr dette for oss i Norge?
Du tenker kanskje: «Fint for matematikerne, Jan Sverre, men jeg driver et transportfirma på Toten. Hva skal jeg med differensialligninger?»
Svaret ligger i overføringsverdien. Matematikk er det ultimate testfeltet fordi det finnes en objektiv sannhet. Hvis AI kan resonnere seg frem til korrekte løsninger her, uten å hallusinere, åpner det døren for anvendelser på andre kritiske områder:
- Feilfri koding: Programvareutvikling handler i bunn og grunn om logikk. En AI som kan bevise at koden sin er feilfri, vil revolusjonere IT-sikkerhet.
- Kompleks logistikk: Optimering av ruter og energibruk handler om matematisk modellering.
- Juss og kontrakter: Selv om juss ikke er like binært som matte, krever det streng logisk oppbygning. «Resonerende AI» er mye tryggere enn «Generativ AI» i juridiske sammenhenger.
Vi beveger oss nå fra en fase med Generativ AI (som lager bilder og tekst) til Resonerende AI (som løser faktiske problemer). Det er her den virkelige verdien for norske bedrifter kommer til å ligge i årene fremover. Vi må slutte å se på AI bare som en kreativ innholdsprodusent, og begynne å se på den som en analytisk motor.
Konklusjon: Et skritt nærmere sannheten
Jeg har ofte advart mot å tro at AGI (kunstig generell intelligens) er rett rundt hjørnet. Jeg står fortsatt ved at vi er et stykke unna en maskin som fungerer som et menneske. Men AlphaProof viser oss en vei forbi de begrensningene vi trodde var absolutte for bare ett år siden. Ved å tvinge AI-en til å operere innenfor formelle logiske rammer (som Lean), har DeepMind gitt oss en motgift mot hallusinering.
Maskinen har ikke lenger bare lest hele internett. Den har begynt å tenke selv. Og svaret den kommer med er ikke bare sannsynligvis riktig – det er matematisk bevist. Det er en forskjell vi ikke har råd til å ignorere.
