DeepSeek-Prover-V2: Broer gapen mellom uformell og formell matematisk resonnering

Mens DeepSeek-R1 har fremmet AI sin evne til uformell resonnering betydelig, har formell matematisk resonnering forblitt en utfordring for AI. Dette skyldes hovedsakelig at produksjon av verifiserbar matematisk bevis krever både dyp konseptuell forståelse og evnen til å konstruere presise, steg-for-steg logiske argumenter. Nylig er imidlertid betydelig fremgang gjort i denne retningen, da forskere ved DeepSeek-AI har introdusert DeepSeek-Prover-V2, en åpen kildekode AI-modell som kan omforme matematisk intuisjon til strenge, verifiserbare bevis. Denne artikkelen vil dykke dyptere inn i detaljene om DeepSeek-Prover-V2 og vurdere dens potensielle innvirkning på fremtidig vitenskapelig oppdagelse.

Utfordringen med formell matematisk resonnering

Matematikere løser ofte problemer ved hjelp av intuisjon, heuristikk og høynivå-resonnering. Denne tilnærmingen tillater dem å hoppe over trinn som synes åpenbare eller å basere seg på approksimasjoner som er tilstrekkelige for deres behov. Formal teorembevisning krever imidlertid en annen tilnærming. Den krever full presisjon, med hver enkelt trinn uttrykt eksplisitt og logisk berettiget uten noen tvetydighet.

De siste fremgangene i store språkmodeller (LLM) har vist at de kan løse komplekse, konkurranse-nivå matematikkproblemer ved hjelp av naturlig språk-resonnering. Til tross for disse fremgangene, har LLM fortsatt vanskeligheter med å konvertere intuitiv resonnering til formelle bevis som maskiner kan verifisere. Dette skyldes hovedsakelig at uformell resonnering ofte inkluderer kortveier og utelatte trinn som formelle systemer ikke kan verifisere.

DeepSeek-Prover-V2 løser dette problemet ved å kombinere styrkene til uformell og formell resonnering. Den bryter ned komplekse problemer i mindre, håndterbare deler, samtidig som den opprettholder presisjonen som kreves av formell verifisering. Denne tilnærmingen gjør det lettere å broe gapet mellom menneskelig intuisjon og maskin-verifiserte bevis.

En ny tilnærming til teorembevisning

I essensen anvender DeepSeek-Prover-V2 en unik data-prosesseringspipeline som involverer både uformell og formell resonnering. Pipelinen begynner med DeepSeek-V3, en generell LLM, som analyserer matematikkproblemer i naturlig språk, dekomponerer dem i mindre trinn og oversetter disse trinnene til formelt språk som maskiner kan forstå.

I stedet for å forsøke å løse hele problemet på en gang, bryter systemet det ned i en rekke “sub-mål” – mellomlemmer som tjener som støttestener mot det endelige beviset. Denne tilnærmingen repliserer hvordan menneskelige matematikere løser vanskelige problemer, ved å arbeide gjennom håndterbare deler i stedet for å forsøke å løse alt på en gang.

Hva gjør denne tilnærmingen spesielt innovativ er hvordan den syntetiserer treningsdata. Når alle sub-mål i et komplekst problem er løst, kombinerer systemet disse løsningene til et fullstendig formelt bevis. Dette beviset er deretter parret med DeepSeek-V3s opprinnelige tanke-prosess resonnering for å skape høykvalitets “kald-start” treningsdata for modell-treningsdata.

Forsterket læring for matematisk resonnering

Etter initialt treningsdata på syntetisk data, anvender DeepSeek-Prover-V2 forsterket læring for å ytterligere forbedre sine evner. Modellen får tilbakemelding på om dens løsninger er korrekte eller ikke, og den bruker denne tilbakemeldingen til å lære hvilke tilnærminger som fungerer best.

En av utfordringene her er at strukturen på de genererte bevisene ikke alltid stemmer overens med lemmadekomposisjonen foreslått av tanke-prosess. For å løse dette, inkluderte forskerne en konsistens-belønning i treningsfasene for å redusere struktur-misalignering og påtvinge inklusjon av alle dekomponerte lemmata i endelige bevis. Denne tilnærmingen har vist seg å være spesielt effektiv for komplekse teorier som krever multi-trinn resonnering.

Ytelse og virkelige evner

DeepSeek-Prover-V2s ytelse på etablerte benchmark-tester demonstrerer dens usedvanlige evner. Modellen oppnår imponerende resultater på MiniF2F-test benchmark og løser 49 av 658 problemer fra PutnamBench – en samling av problemer fra den prestisjefylte William Lowell Putnam matematikkonkurransen.

Kanskje enda mer imponerende er at, når den vurderes på 15 utvalgte problemer fra nylige American Invitational Mathematics Examination (AIME) konkurranser, løser modellen 6 problemer. Det er også interessant å notere at, i sammenligning med DeepSeek-Prover-V2, løser DeepSeek-V3 8 av disse problemene ved hjelp av flertallsavstemning. Dette antyder at gapet mellom formell og uformell matematisk resonnering er raskt smalner i LLM. Imidlertid krever modellens ytelse på kombinatoriske problemer fortsatt forbedring, og høylysere et område hvor fremtidig forskning kunne fokusere.

ProverBench: En ny benchmark for AI i matematikk

DeepSeek-forskerne har også introdusert en ny benchmark-datasett for å evaluere den matematisk problemløsningsevnen til LLM. Denne benchmarken, kalt ProverBench, består av 325 formaliserte matematikkproblemer, inkludert 15 problemer fra nylige AIME-konkurranser, samt problemer fra lærebøker og utdannings-tutorials. Disse problemene dekker fag som tallteori, algebra, kalkulus, reell analyse og mer. Innføringen av AIME-problemer er spesielt vital, da den vurderer modellen på problemer som krever ikke bare kunnskaps-henting, men også kreativ problemløsning.

Åpen kildekode-tilgang og fremtidige implikasjoner

DeepSeek-Prover-V2 tilbyr en spennende mulighet med sin åpen kildekode-tilgjengelighet. Vertet på plattformer som Hugging Face, er modellen tilgjengelig for en bred rekke av brukere, inkludert forskere, utdannere og utviklere. Med både en mer lettvekts 7-milliarder parameter-versjon og en kraftig 671-milliarder parameter-versjon, sikrer DeepSeek-forskerne at brukere med varierende beregningsressurser likevel kan dra nytte av den. Denne åpen tilgangen oppmuntrer til eksperimentering og muliggjør at utviklere kan skape avanserte AI-verktøy for matematisk problemløsning. Som et resultat har denne modellen potensialet til å drive innovasjon i matematisk forskning, og å muliggjøre at forskere løser komplekse problemer og avdekker nye innsikter i feltet.

Implikasjoner for AI og matematisk forskning

Utviklingen av DeepSeek-Prover-V2 har betydelige implikasjoner ikke bare for matematisk forskning, men også for AI. Modellens evne til å generere formelle bevis kan assistere matematikere i å løse vanskelige teorier, automatisere verifiseringsprosesser og til og med foreslå nye hypoteser. I tillegg kan teknikken som ble brukt til å skape DeepSeek-Prover-V2 påvirke utviklingen av fremtidige AI-modeller i andre fag som avhenger av streng logisk resonnering, som programvare- og maskin-ingeniørvitenskap.

Forskerne har som mål å skalerer modellen for å løse enda mer komplekse problemer, som de som er på International Mathematical Olympiad (IMO) nivå. Dette kan ytterligere fremme AI sin evne til å bevise matematisk teorier. Ettersom modeller som DeepSeek-Prover-V2 fortsetter å utvikle seg, kan de omdefinere fremtiden for både matematikk og AI, og drive fremgang i områder som spenner fra teoretisk forskning til praktiske anvendelser i teknologi.

Bunnen av saken

DeepSeek-Prover-V2 er en betydelig utvikling i AI-drevet matematisk resonnering. Den kombinerer uformell intuisjon med formell logikk for å bryte ned komplekse problemer og generere verifiserbare bevis. Den imponerende ytelsen på benchmark-tester viser dens potensiale til å støtte matematikere, automatisere bevis-verifisering og til og med drive nye oppdagelser i feltet. Som en åpen kildekode-modell er den tilgjengelig for alle, og tilbyr spennende muligheter for innovasjon og nye anvendelser i både AI og matematikk.