AI ved Den Internationale Matematisk Olympiad: Hvordan AlphaProof og AlphaGeometry 2 opnåede sølvmedaljeniveau

Matematisk resonnering er en vital del af menneskets kognitive evner, der driver fremgang i videnskabelige opdagelser og teknologiske udviklinger. Da vi stræber efter at udvikle kunstig generel intelligens, der matcher menneskets kognition, er det essentiel at udstyre AI med avancerede matematiske resonneringsfærdigheder. Mens nuværende AI-systemer kan håndtere grundlæggende matematikproblemer, kæmper de med den komplekse resonnering, der er nødvendig for avancerede matematiske discipliner som algebra og geometri. Men dette kan være under forandring, da Google DeepMind har gjort væsentlige fremskridt i at fremme et AI-systems matematiske resonneringsfærdigheder. Dette gennembrud er opnået ved Den Internationale Matematisk Olympiad (IMO) 2024. Etableret i 1959 er IMO den ældste og mest prestigefyldte matematikkonkurrence, der udfordrer high school-studerende verden over med problemer i algebra, kombinatorik, geometri og talteori. Hvert år konkurrerer hold af unge matematikere for at løse seks meget udfordrende problemer. I år introducerede Google DeepMind to AI-systemer: AlphaProof, der fokuserer på formel matematisk resonnering, og AlphaGeometry 2, der specialiserer sig i at løse geometriske problemer. Disse AI-systemer formåede at løse fire af seks problemer, og opnåede dermed sølvmedaljeniveau. I denne artikel vil vi udforske, hvordan disse systemer fungerer til at løse matematiske problemer.

AlphaProof: Kombinerer AI og formel sprog til matematisk bevisføring

AlphaProof er et AI-system designet til at bevise matematiske udsagn ved hjælp af det formelle sprog Lean. Det integrerer Gemini, et forudtrænet sprogmodel, med AlphaZero, en forstærkningslæringsalgoritme, der er berømt for at mestre skak, shogi og Go.

Gemini-modellen oversætter naturligt sprogproblemer til formelle problemer, og opretter en bibliotek af problemer med varierende sværhedsgrader. Dette tjener to formål: omregning af upræcist naturligt sprog til præcist formelt sprog til verificering af matematiske beviser, og brug af Gemini’s prædiktive evner til at generere en liste over mulige løsninger med formelt sprogpræcision.

Når AlphaProof møder et problem, genererer det potentielle løsninger og søger efter bevistrin i Lean for at verificere eller afvise dem. Dette er i virkeligheden en neuro-symbolisk tilgang, hvor neuralt netværk, Gemini, oversætter naturligt sprog til symbolisk formelt sprog for at bevise eller afvise udsagnet. Ligesom AlphaZeros selvspilsmekanisme, hvor systemet lærer ved at spille spil mod sig selv, træner AlphaProof sig selv ved at forsøge at bevise matematiske udsagn. Hver bevisforsøg forfiner AlphaProofs sprogmodel, med succesfulde beviser, der forstærker modellens evne til at tackle mere udfordrende problemer.

Til Den Internationale Matematisk Olympiad (IMO) blev AlphaProof trænet ved at bevise eller afvise millioner af problemer, der dækkede forskellige sværhedsgrader og matematiske emner. Denne træning fortsatte under konkurrencen, hvor AlphaProof forfiner sine løsninger, indtil det fandt komplette svar på problemernes løsninger.

AlphaGeometry 2: Integrerer LLM’er og symbolisk AI til at løse geometriske problemer

AlphaGeometry 2 er den seneste iteration af AlphaGeometry-serien, designet til at tackle geometriske problemer med forbedret præcision og effektivitet. Bygget på fundamentet af sin forgænger, anvender AlphaGeometry 2 en neuro-symbolisk tilgang, der kombinerer neurale store sprogmodeller (LLM’er) med symbolisk AI. Denne integration kombinerer regelbaseret logik med neuralt netværks prædiktive evne til at identificere hjælpepunkter, der er essentielle for at løse geometriske problemer. LLM’en i AlphaGeometry forudser nye geometriske konstruktioner, mens den symboliske AI anvender formel logik til at generere beviser.

Når AlphaGeometry konfronteres med et geometrisk problem, evaluerer LLM’en talrige muligheder og forudser konstruktioner, der er afgørende for problem-løsning. Disse forudsigelser tjener som værdifulde hints, der leder den symboliske motor mod præcise deduktioner og bringer den tættere på en løsning. Denne innovative tilgang giver AlphaGeometry mulighed for at tackle komplekse geometriske udfordringer, der strækker sig ud over konventionelle scenarier.

En vigtig forbedring i AlphaGeometry 2 er integrationen af Gemini LLM. Denne model er trænet fra scratch på betydeligt mere syntetisk data end sin forgænger. Denne omfattende træning udstyrer den til at håndtere mere vanskelige geometriske problemer, herunder dem, der involverer objekter i bevægelse og ligninger om vinkler, forhold eller afstande. Desuden har AlphaGeometry 2 en symbolisk motor, der fungerer to størrelsesordener hurtigere, hvilket giver den mulighed for at udforske alternative løsninger med hidtil uset hast. Disse fremskridt gør AlphaGeometry 2 til et kraftfuldt værktøj til at løse komplekse geometriske problemer og sætter en ny standard i feltet.

AlphaProof og AlphaGeometry 2 ved IMO

I år ved Den Internationale Matematisk Olympiad (IMO) blev deltagerne testet med seks forskellige problemer: to i algebra, en i talteori, en i geometri og to i kombinatorik. Google-forskere oversatte disse problemer til formel matematisk sprog til AlphaProof og AlphaGeometry 2. AlphaProof løste to algebra-problemer og ét talteori-problem, herunder det mest vanskelige problem i konkurrencen, som kun fem menneskelige deltagere løste i år. Imens løste AlphaGeometry 2 med succes det geometriske problem, men kunne ikke løse de to kombinatoriske udfordringer.

Hvert problem ved IMO er værd 7 point, og opgør sig til en maksimum på 42 point. AlphaProof og AlphaGeometry 2 opnåede 28 point og opnåede dermed perfekte score på de problemer, de løste. Dette placerede dem i den øvre del af sølvmedalje-kategorien. Guldmedalje-grænsen i år var 29 point, som 58 af de 609 deltagere opnåede.

Næste skridt: Naturligt sprog til matematiske udfordringer

AlphaProof og AlphaGeometry 2 har vist imponerende fremskridt i AI’s evne til at løse matematiske problemer. Men disse systemer afhænger stadig af menneskelige eksperter til at oversætte matematiske problemer til formelt sprog til behandling. Desuden er det uklart, hvordan disse specialiserede matematiske færdigheder kan integreres i andre AI-systemer, såsom til at udforske hypoteser, teste innovative løsninger til langvarige problemer og effektivt håndtere tidskrævende aspekter af beviser.

For at overvinde disse begrænsninger udvikler Google-forskere et naturligt sprog-resoneringssystem baseret på Gemini og deres seneste forskning. Dette nye system sigter mod at fremme problem-løsningsevner uden at kræve formelt sprog-oversættelse og er designet til at integrere smidigt med andre AI-systemer.

Bottom Line

Præstationen af AlphaProof og AlphaGeometry 2 ved Den Internationale Matematisk Olympiad er et bemærkelsesværdigt skridt fremad i AI’s evne til at tackle komplekse matematiske resonneringer. Begge systemer demonstrerede sølvmedalje-niveau ved at løse fire af seks udfordrende problemer, og demonstrerede betydelige fremskridt i formel bevis og geometrisk problem-løsning. Trods deres præstationer afhænger disse AI-systemer stadig af menneskelig input til at oversætte problemer til formelt sprog og står over for udfordringer med hensyn til integration med andre AI-systemer. Fremtidig forskning sigter mod at forbedre disse systemer yderligere, muligvis ved at integrere naturligt sprog-resonering for at udvide deres evner på tværs af et bredere spektrum af matematiske udfordringer.