KI genererer matematiske bevis: Forskere må kontrollere funn

Kunstig intelligens (KI) har nå beveget seg fra å generere tekst til å produsere matematiske bevis. Denne utviklingen reiser spørsmål om hvordan slike funn skal etterprøves, og understreker behovet for uavhengige fagmiljøer som kan validere påstandene fra teknologiselskaper som OpenAI. Et nylig eksempel involverer OpenAIs modell, Astra, som har generert et bevis på over 37 000 linjer med kode, et bevis som hevder å utfordre en over 40 år gammel antakelse fremsatt av den anerkjente matematikeren Alain Connes, en mottaker av Fields-medaljen.

Connes, kjent for sitt arbeid innen operatoralgebraer, stilte opprinnelig spørsmål ved om et bestemt matematisk «fingeravtrykk» alltid kunne identifisere objektet det stammer fra. OpenAI, gjennom Astra, hevder å ha funnet tilfeller der ulike objekter deler samme fingeravtrykk. Etter at disse funnene ble publisert, oppsto det påstander i sosiale medier om at KI-en hadde utført logikken korrekt, men angrepet feil problemstilling. Enkelte innvendinger synes å bygge på matematiske sammenblandinger, mens andre bidrag, som et moteksempel til Connes’ antakelse funnet av matematikeren Shuoxing Zhou ved hjelp av KI, også har blitt presentert. Disse hendelsene illustrerer hvor raskt både potensielle gjennombrudd og påstander om feil kan spre seg i den digitale tidsalderen.

KI som forskningsverktøy: Muligheter og utfordringer

Connes-arbeidet er ett av ti manuskripter OpenAI nylig offentliggjorde, med temaer som spenner fra kulepakking i høye dimensjoner til abstrakte matematiske objekter. Disse manuskriptene, som til sammen fyller 249 sider, ble funnet og bearbeidet ved hjelp av modellen Astra. Etter at menneskelige forskere bearbeidet materialet med modellen, ble argumentene formalisert i Lean, et system som verifiserer matematiske slutninger trinn for trinn. OpenAI anslår at det kostet rundt 2000 dollar å bruke modellen til å finne løsningene, et beløp som ikke inkluderer utviklings- og treningkostnader. Med ferdigutviklede modeller blir det dermed kostnadseffektivt å produsere nye beviskandidater.

Selv om hvert enkelt resultat ennå ikke er endelig bekreftet, anser forskere dette som et gjennombrudd på grunn av bredden i funnene. Mens ti resultater kan være mer enn tilfeldig flaks, er det viktig å huske at disse ikke er ti aksepterte teoremer. Lean-systemet kan bekrefte at en påstand følger av gitte definisjoner, men det kan ikke avgjøre om påstanden reflekterer det historiske problemet, om resultatet er nytt, eller hvilken reell betydning det har. Denne vurderingen krever fortsatt ekspertise fra fagfolk.

Teknologien bak dagens KI, opprinnelig utviklet for språkforståelse og -generering, finner nå anvendelse i problemer den ikke var ment for, som matematisk forskning. Matematikken er et tydelig eksempel på denne overgangen, da matematiske argumenter kan kontrolleres steg for steg. I mange andre felt er det betydelig vanskeligere å vurdere om et svar er korrekt. Professor Fabian Harang ved Handelshøyskolen BI og SURE-AI har erfart at språkmodeller kan identifisere svakheter i manuskripter og bidra til kodeutvikling, noe som reduserer tiden fra uker til dager, men som krever grundig menneskelig kontroll. KI-verktøy kan bistå med litteratursøk, kodehjelp og identifisering av potensielle svakheter, men de kan også feilaktig henvise til ikke-eksisterende artikler eller presentere feilaktige argumenter.

Førsteamanuensis Cris Salvi ved Logos Research og Imperial College London peker på en flaskehals: Det er blitt billig å produsere matematikk som virker overbevisende, men grundig kontroll kan ikke fremskyndes i samme tempo. Derfor må kravene til dokumentasjon og ansvar opprettholdes. Denne utviklingen påvirker også utdanningssektoren. Studenter kan allerede få overbevisende løsninger på mange oppgaver på sekunder. Hvis skriftlige svar er det eneste beviset på læring, risikerer man å teste tilgangen til KI-verktøy fremfor reell matematisk forståelse. Et generelt forbud mot KI i studier kan imidlertid frata studentene verdifull veiledet erfaring med teknologi de senere vil møte i arbeidslivet.

Universiteter må derfor tilpasse seg. Det kan innebære eksamener der studentene må muntlig forsvare løsninger, identifisere feil i KI-genererte argumenter, og sammenligne ulike forslag. Personer som skal kontrollere maskinens arbeid, vil fortsatt trenge et solid matematisk fundament. Dette gjør ikke matematikere overflødige, men vil endre deres arbeid. Mer tid kan brukes på å kontrollere forutsetninger, forstå implikasjoner og avgjøre hvilke spørsmål som er verdt å utforske, heller enn å bruke mye tid på å finne det første forslaget. Universitetene bør derfor bygge kompetanse innen KI-støttet matematikk og formelle metoder, og tidsskrifter samt institusjoner må tydeliggjøre retningslinjer for dokumentasjon av KI-bruk. Spesielt viktig er uavhengige fagmiljøer som kan etterprøve selskapenes påstander. OpenAI fortjener anerkjennelse for å ha publisert manuskripter og formelle sertifikater som muliggjør seriøs etterprøving. Samtidig må fagmiljøet unngå å bli passive tilskuere. Connes-episoden viser at man kan la seg rive med av en forenklet fortelling. Verken et Lean-sertifikat eller spredning i sosiale medier er tilstrekkelig alene for å fastslå om et problem er korrekt løst, om resultatet er nytt, eller hva dets betydning er. Det er allerede mulig å generere flere matematiske forslag enn fagmiljøet klarer å kontrollere. Derfor blir universitetenes oppgave konkret: å utdanne mennesker som kan skille genuine gjennombrudd fra blindspor, og som stiller det kritiske spørsmålet: Har vi faktisk bevist det vi tror vi har bevist? Når bevisene blir billige, blir dømmekraften verdifull.