Fra sølv til gull: Hvordan DeepMinds AI erobret matematikkoordinatet

DeepMinds AI har gjort bemerkelsesverdige fremskritt i matematisk resonnering innen ett år. Etter å ha vunnet en sølvmedalje ved Den internasjonale matematikkolympiaden (IMO) i 2024, vant deres AI-system en gullmedalje i 2025. Denne raske fremgangen understreker de voksende evnene til kunstig intelligens i å takle komplekse, abstrakte problemer som krever menneskelignende kreativitet og innsikt. Denne artikkelen vil gå gjennom hvordan DeepMind oppnådde denne transformasjonen, de tekniske og strategiske valgene bak det, og de videre implikasjonene av disse fremgangene.

Betydningen av IMO

Den internasjonale matematikkolympiaden, etablert i 1959, er anerkjent globalt som den fremste matematikkonkurransen for videregående skoleelever. Hvert år møter toppstudenter fra hele verden seks utfordrende problemer innen algebra, geometri, tallteori og kombinatorikk. Å løse disse problemene krever mye mer enn beregning; deltakerne må vise ekte matematisk kreativitet, streng logisk tenkning og evnen til å konstruere elegante bevis.

For kunstig intelligens presenterer IMO en unik utfordring. Mens AI har mestret mønstergjenkjenning, dataanalyse og sogar komplekse spill som Go og sjakk, krever olympiadematematikk kreative, abstrakte resonnering og syntese av nye ideer, ferdigheter som tradisjonelt anses å være kjennetegn på menneskelig intelligens. Derfor har IMO blitt en naturlig testbed for å vurdere hvor nære AI er å oppnå virkelig menneskelignende resonnering.

Sølvmedalje-gjennombruddet i 2024

I 2024 introduserte DeepMind to AI-systemer for å takle IMO-nivåproblemer: AlphaProof og AlphaGeometry 2. Begge systemer er eksempler på “neuro-symbolisk” AI, som kombinerer styrkene til store språkmodeller (LLM) med rigor til symbolisk logikk.

AlphaProof ble designet for å bevise matematiske utsagn ved hjelp av Lean, et formelt matematisk språk. Det kombinerte Gemini, DeepMinds store språkmodell, med AlphaZero, som er en forsterkingslæringssmotor kjent for sin suksess i brettspill. I denne sammenhengen var Gemini’s rolle å oversette naturlige språkproblemer til Lean og forsøke å bevise logiske skritt. AlphaProof ble trent på millioner av eksempler på problemer som spenner over ulike matematiske disipliner og vanskelighetsgrader. Systemet forbedret seg selv ved å prøve å bevise stadig mer komplekse utsagn, likt hvordan AlphaZero lærte ved å spille spill mot seg selv.

AlphaGeometry 2 ble designet for å løse geometriproblemer. Her enablede Gemini’s språkforståelse AI-en å forutsi nyttige hjelpekonstruksjoner, mens en symbolisk resoneringssmotor håndterte logiske deduksjoner. Denne hybride tilnærmingen tillot AlphaGeometry å takle geometriske problemer langt utenfor rekkevidden av tradisjonell maskinresonnering.

Sammen løste disse systemene fire av seks IMO-problemer: to i algebra, ett i tallteori og ett i geometri, og oppnådde en poengsum på 28 av 42. Denne prestasjonen var et betydelig milepæl, da det var første gang en AI hadde nådd sølvmedaljenivået ved IMO. Imidlertid var denne suksessen sterkt avhengig av menneskelige eksperter for å oversette problemer til formelle matematiske språk. De krevde også massive beregningsressurser, som tok dager med prosesseringstid for hvert problem.

Tekniske innovasjoner bak gullmedaljen

DeepMinds overgang fra en sølv til en gullmedalje var drevet av flere betydelige tekniske forbedringer.

1. Naturlig språk som medium for bevis

Den mest betydelige endringen var å gå fra systemer som krevde ekspertoversettelser til formelle språk til å behandle naturlig språk som medium for bevis. Denne endringen ble oppnådd gjennom en forbedret versjon av Gemini utstyrt med Deep Think-kapasiteter. I stedet for å konvertere problemer til Lean, prosesserer modellen teksten direkte, genererer uformelle skisser, internt formaliserer kritiske skritt og produserer en raffinert engelsk bevis. Forsterkingslæring fra menneskelig tilbakemelding (RLHF) ble brukt til å belønne løsninger som var logisk konsistente, korte og presenterte.

Gemini Deep Think skiller seg fra den offentlige versjonen av Gemini på to måter. Først allokerer den lengre kontekstvinduer og flere beregningsToken per forespørsel, noe som muliggjør at modellen kan opprettholde multi-sidige tanker. For det andre bruker den parallell resonnering, der hundrevis av spekulative tråder genereres for ulike potensielle løsninger. En lett tilsynshaver rangerer og fremmer deretter de mest lovende stier, låner konsepter fra Monte Carlo-trærøkning, men anvendt på tekst. Denne tilnærmingen ligner hvordan menneskelige team brainstormer, forkaster uproduktive ideer og konvergerer mot elegante løsninger.

2. Trening og forsterkingslæring

Trening av Gemini Deep Think innebar finjustering av modellen for å forutsi neste skritt i stedet for endelige svar. For dette formålet ble en korpus på 100 000 høykvalitets IMO- og universitetskonkurranseløsninger samlet inn. Korpuset ble hovedsakelig samlet fra offentlige matematikkforum, arXiv-preprint og collegeproblemer. Menneskelige mentorer gjennomgikk trenings eksempler for å filtrere illogiske eller ufullstendige bevis. Forsterkingslæring hjalp til å finjustere modellen, som ble presset mot å produsere konsise og presise bevis. Tidlige versjoner produserte overordnet verbale bevis, men straffer på redundante fraser hjalp til å kutte uttaket.

I motsetning til konvensjonell finjustering, som ofte sliter med sparsomme belønninger hvor tilbakemelding er binær, enten er beviset riktig eller ikke. DeepMind implementerte et trinnvis belønningsystem, der hver verifisert underlemma bidro til den totale poengsummen. Denne belønningsmekanismen guider Gemini, selv når fullstendig bevis er sjeldent. Treningprosessen varte i tre måneder og brukte omtrent 25 millioner TPU-timer.

3. Massiv parallellisering

Parallellisering spilte også en kritisk rolle i DeepMinds fremgang fra sølv til gull. Hvert problem genererte flere resonanser i parallell, med ressurser som dynamisk skiftet til mer løftende veier når andre stanset. Denne dynamiske planleggingen var spesielt gunstig for kombinatoriske problemer, som har store løsningsrom. Tilnærmingen er lik hvordan mennesker tester hjelpeulikheter før de begynner en full induksjon. Selv om denne teknikken var beregningskrevende, var den håndterbar ved hjelp av DeepMinds TPU v5-kluster.

DeepMind ved IMO 2025

For å opprettholde integriteten til konkurransen, frøs DeepMind vekterne til modellen tre uker før IMO for å forhindre at offisielle problemer kom inn i treningssettet. De filtrerte også ut data som inneholdt løsninger på tidligere upubliserte olympiadeproblemer.

Under konkurransen fikk Gemini Deep Think de seks offisielle problemene i ren tekstformat, uten å gi tilgang til internettet. Systemet opererte på et kluster konfigurert for å simulere beregningskraften til en standard bærbar datamaskin per prosess. Hele problem-løsingsprosessen ble fullført på mindre enn tre timer, godt innenfor tidsbegrensningene. De genererte bevisene ble sendt til IMO-koordinatorerne uten endringer.

Gemini Deep Think oppnådde full poeng på de fem første problemene. Det siste spørsmålet, som var et utfordrende kombinatorisk puslespill, stumpet imidlertid både AI og 94% av menneskelige deltakere. Til tross for dette fullførte AI-en med en total poengsum på 35/42 og sikret en gullmedalje. Denne poengsummen var syv poeng høyere enn årets tidligere sølvprestasjon. Observatører beskrev senere AI-ens bevis som “flittige” og “fullstendige”, og noterte at de fulgte de strenge rettferdiggjøringene som forventes av menneskelige deltakere.

Implikasjoner for AI og matematikk

DeepMinds prestasjon er et betydelig milepæl for både AI og matematikk. For AI er å mestre IMO et skritt mot kunstig generell intelligens (AGI), der systemer kan utføre enhver intellektuell oppgave som et menneske kan. Å løse komplekse matematiske problemer krever resonnering og forståelse, som er grunnleggende komponenter i generell intelligens. Denne suksessen indikerer at AI gjør fremskritt mot mer menneskelignende kognitive evner.

For matematikk kan AI-systemer som Gemini Deep Think bli uvurderlige verktøy for matematikere. De kan assistere i å utforske nye områder, verifisere antagelser og sogar oppdage nye teorier. Ved å automatisere de mer kjedelige aspektene av beviskonstruksjon, frigjør AI menneskelige matematikere til å fokusere på høyere konseptuell arbeid. I tillegg kan teknikken som er utviklet for disse AI-systemene inspirere nye metoder i matematisk forskning som kanskje ikke er mulig gjennom menneskelig innsats alene.

Imidlertid setter AI-ens fremgang i matematikk også spørsmål om AI-ens rolle i utdanningsinstilling og konkurranser. Ettersom AI-ens evner fortsetter å vokse, vil det være debatter om hvordan AI-ens involvering kan endre naturen til matematisk utdanning og konkurranse.

Se fremover

Å vinne IMO-gull er et betydelig milepæl, men mange matematiske utfordringer ligger fortsatt utenfor rekkevidde for nåværende AI-systemer. Imidlertid understreker den raske fremgangen fra sølv til gull på bare ett år den akselererende takten i AI-innovasjoner og -utviklinger. Hvis denne takten fortsetter, kan AI-systemer snart takle noen av matematikkens mest berømte uløste problemer. Mens spørsmålet om hvorvidt AI vil erstatte eller forbedre menneskelig kreativitet fortsatt er uløst, er IMO 2025 et tydelig tegn på at kunstig intelligens har gjort betydelige fremskritt i logisk resonnering. ments. Hvis denne takten fortsetter, kan AI-systemer snart takle noen av matematikkens mest berømte uløste problemer. Mens spørsmålet om hvorvidt AI vil erstatte eller forbedre menneskelig kreativitet fortsatt er uløst, er IMO 2025 et tydelig tegn på at kunstig intelligens har gjort betydelige fremskritt i logisk resonnering.