AI ved Den internasjonale matematikkolympiaden: Hvordan AlphaProof og AlphaGeometry 2 oppnådde sølvmedaljenivå

Matematisk resonnering er en vital del av menneskelige kognitive evner, og driver fremgang i vitenskapelige oppdagelser og teknologiske utviklinger. Mens vi streber etter å utvikle kunstig generell intelligens som matcher menneskelig kognisjon, er det essensielt å utstyre AI med avanserte matematiske resonneringsevner. Mens nåværende AI-systemer kan håndtere grunnleggende matematikkproblemer, sliter de med den komplekse resonneringen som er nødvendig for avanserte matematiske disipliner som algebra og geometri. Imidlertid kan dette være i ferd med å endre seg, ettersom Google DeepMind har gjort betydelige fremskritt i å fremme en AI-systems matematiske resonneringsevner. Dette gjennombruddet ble gjort ved Den internasjonale matematikkolympiaden (IMO) 2024. Etter å ha blitt etablert i 1959, er IMO den eldste og mest prestisjefylte matematikkonkurransen, og utfordrer high school-studenter verden over med problemer i algebra, kombinatorikk, geometri og tallteori. Hvert år konkurrerer lag av unge matematikere for å løse seks svært utfordrende problemer. I år introduserte Google DeepMind to AI-systemer: AlphaProof, som fokuserer på formell matematisk resonnering, og AlphaGeometry 2, som spesialiserer seg i å løse geometriske problemer. Disse AI-systemene klarte å løse fire av seks problemer, og presterte på samme nivå som en sølvmedaljør.

AlphaProof: Kombinerer AI og formell språk for matematisk bevis

AlphaProof er et AI-system designet for å bevise matematiske utsagn ved hjelp av det formelle språket Lean. Det integrerer Gemini, et forhåndsrent language model, med AlphaZero, en forsterkingslæringsalgoritme som er kjent for å mestre sjakk, shogi og Go.

Gemini-modellen oversetter naturlig språkproblemer til formelle problemer, og skaper en bibliotek av problemer med varierende vanskelighetsgrad. Dette tjener to formål: å konvertere upresise naturlige språk til presise formelle språk for å verifisere matematiske bevis, og å bruke de prediktive evnene til Gemini til å generere en liste over mulige løsninger med formell språkpresisjon.

Når AlphaProof møter et problem, genererer det potensielle løsninger og søker etter bevissteg i Lean for å verifisere eller motbevise dem. Dette er i hovedsak en neuro-symbolisk tilnærming, der neurale nettverk, Gemini, oversetter naturlige språkinstruksjoner til det symboliske formelle språket Lean for å bevise eller motbevise utsagnet. Liksom AlphaZeros selvspillmekanisme, hvor systemet lærer ved å spille spill mot seg selv, trener AlphaProof seg selv ved å forsøke å bevise matematiske utsagn. Hvert bevisforsøk forbedrer AlphaProofs språkmodell, med suksessfulle bevis som forsterker modellens evne til å takle mer utfordrende problemer.

For Den internasjonale matematikkolympiaden (IMO) ble AlphaProof trent ved å bevise eller motbevise millioner av problemer som dekket ulike vanskelighetsgrader og matematiske emner. Denne treningen fortsatte under konkurransen, hvor AlphaProof forbedret sine løsninger til den fant komplette svar på problemene.

AlphaGeometry 2: Integrerer LLM og symbolisk AI for å løse geometriske problemer

AlphaGeometry 2 er den nyeste iterasjonen av AlphaGeometry-serien, designet for å takle geometriske problemer med forbedret presisjon og effektivitet. Bygget på grunnlag av sin forgjenger, bruker AlphaGeometry 2 en neuro-symbolisk tilnærming som kombinerer neurale store språkmodeller (LLM) med symbolisk AI. Denne integreringen kombinerer regelbasert logikk med den prediktive evnen til neurale nettverk for å identifisere hjelpepunkter, som er essensielle for å løse geometriske problemer. LLM i AlphaGeometry forutsier nye geometriske konstruksjoner, mens den symboliske AI anvender formell logikk for å generere bevis.

Når AlphaGeometry møter et geometrisk problem, vurderer LLM flere muligheter, og forutsier konstruksjoner som er kritiske for å løse problemet. Disse forutsigelsene tjener som verdifulle ledetråder, og guider den symboliske motoren mot nøyaktige deduksjoner og fremover mot en løsning. Denne innovative tilnærmingen muliggjør at AlphaGeometry kan takle komplekse geometriske utfordringer som går utenfor konvensjonelle scenarioer.

En nøkkelforbedring i AlphaGeometry 2 er integreringen av Gemini LLM. Denne modellen er trent fra scratch på betydelig mer syntetisk data enn sin forgjenger. Denne omfattende treningen utstyrer den til å håndtere mer vanskelige geometriske problemer, inkludert de som involverer objektflytting og ligninger for vinkler, forhold eller avstander. I tillegg har AlphaGeometry 2 en symbolisk motor som opererer to størrelsesordener raskere, og muliggjør at den kan utforske alternative løsninger med utenforliggende hastighet. Disse fremskrittene gjør AlphaGeometry 2 til et kraftfullt verktøy for å løse intrikate geometriske problemer, og setter en ny standard i feltet.

AlphaProof og AlphaGeometry 2 ved IMO

I år ved Den internasjonale matematikkolympiaden (IMO) ble deltakerne testet med seks ulike problemer: to i algebra, ett i tallteori, ett i geometri og to i kombinatorikk. Google-forskere oversatte disse problemene til formell matematisk språk for AlphaProof og AlphaGeometry 2. AlphaProof løste to algebra-problemer og ett tallteoriproblem, inkludert det mest vanskelige problemet i konkurransen, som bare ble løst av fem menneskelige deltakere i år. I mellomtiden løste AlphaGeometry 2 det geometriske problemet, men klarte ikke å løse de to kombinatoriske utfordringene.

Hvert problem ved IMO er verdt syv poeng, og adderer opp til en maksimum på 42. AlphaProof og AlphaGeometry 2 tjente 28 poeng, og oppnådde perfekte poeng på problemene de løste. Dette plasserte dem på høyt nivå i sølvmedalje-kategorien. Gullmedalje-grensen i år var 29 poeng, som ble nådd av 58 av de 609 deltakerne.

Neste skritt: Naturlig språk for matematisk utfordring

AlphaProof og AlphaGeometry 2 har vist imponerende fremskritt i AI-systemers evne til å løse matematiske problemer. Likevel avhenger disse systemene fortsatt av menneskelige eksperter for å oversette matematiske problemer til formell språk for prosessering. I tillegg er det uklart hvordan disse spesialiserte matematiske ferdighetene kan inkorporeres i andre AI-systemer, som for å utforske hypoteser, teste innovative løsninger på langvarige problemer og effektivt håndtere tidskrevende aspekter av bevis.

For å overvinne disse begrensningene, utvikler Google-forskere et naturlig språk-resoneringssystem basert på Gemini og deres siste forskning. Dette nye systemet har som mål å fremme problem-løsningsevner uten å kreve formell språk-oversettelse, og er designet for å integrere smidig med andre AI-systemer.

Bunnen av saken

Ytelsen til AlphaProof og AlphaGeometry 2 ved Den internasjonale matematikkolympiaden er et betydelig skritt fremover i AI-systemers evne til å takle kompleks matematisk resonnering. Begge systemene viste sølvmedalje-nivå ved å løse fire av seks utfordrende problemer, og demonstrerte betydelige fremskritt i formell bevis og geometrisk problem-løsning. Til tross for deres prestasjoner, avhenger disse AI-systemene fortsatt av menneskelig innsats for å oversette problemer til formell språk, og møter utfordringer i å integrere med andre AI-systemer. Fremtidig forskning har som mål å forbedre disse systemene videre, potensielt ved å inkorporere naturlig språk-resonering for å utvide deres evner over en bredere rekke av matematiske utfordringer.