Mis on DeepSeek-Prover-V1?
DeepSeek-Prover-V1 on 7 miljardi parameetriga avatud kaaludega keelemudel, mis on loodud spetsiaalselt matemaatiliste teoreemide formaalseks tõestamiseks. Selle asemel et anda mitteametlik selgitus, näiteks „see järeldub Pythagorase teoreemist“, püüab mudel genereerida masinaga kontrollitava tõestuse, mis on kirjutatud keeles Lean 4. Lean 4 on programmeerimiskeel ja tõestusassistent, mida kasutatakse matemaatiliste definitsioonide, teoreemide ja tõestuste väljendamiseks.
DeepSeek avaldas mudeli 23. mail 2024. See lähtestati mudelist DeepSeekMath-Base 7B ja häälestati formaalseks arutlemiseks. Mudeli väljund on tekstipõhine Leani kood, mitte visuaalne tõestus, heliselgitus ega üldine vestlusvastus. Ettenähtud töövoog on genereerimine, kompileerimine, kontrollimine ja parandamine: DeepSeek-Prover-V1 pakub välja tõestuse ning Lean kontrollib seda sõltumatult teoreemi väite, imporditud teekide ja aktiivse Leani keskkonna alusel.
DeepSeek-Proveri perekonnas on see varasem teaduslik väljalase. Esitatud mudeliteave määratleb selle mudelite DeepSeek-Prover-V1.5 ja DeepSeek-Prover-V2 eelkäijana. See on uute projektide jaoks oluline: DeepSeek-Prover-V1 on endiselt kasulik algse uurimistöö kordamiseks või avatud kaaludega tõestusgeneraatori katsetamiseks, kuid uuemat väljalaset vajavate projektide puhul võivad hilisemad sama perekonna mudelid olla sobivamad. Esitatud uurimismaterjal ei anna nende järeltulijatega üksikasjalikku ja kontrollitud võrdlust.
Kuidas mudelit treeniti
DeepSeek-Prover-V1 treenimiseks kasutati ligikaudu kaheksat miljonit sünteetilist formaalset väidet koos tõestustega. Andmete genereerimine algas matemaatikaülesannetest, mida püüti väljendada Leani 4 teoreemiväidetena. Seda protsessi nimetatakse sageli autoformaliseerimiseks. Seejärel genereeriti ja filtreeriti kandidaat-tõestusi ning Lean kontrollis edukad kandidaadid üle.
See kontrollietapp on mudeli peamine kvaliteedikontrolli mehhanism. Keelemudel võib genereerida matemaatiliselt usutavana näivat koodi, mis sisaldab siiski kehtetut järeldust või kasutab kättesaamatut teoreemi. Lean lükkab sellise väljundi tagasi, kui seda ei saa kompileerida või kui see ei tõesta esitatud eesmärki. Seetõttu tuleks DeepSeek-Prover-V1 käsitleda närvivõrgupõhise generaatorina, mida kasutatakse tõestuse otsingu töövoos, mitte autoriteedina, kelle esimest vastust võiks kontrollimata vastu võtta.
Peamised võimalused
- Leani 4 tõestuste genereerimine: see genereerib Lean 4 jaoks formaalseid teoreemiväiteid ja kandidaat-tõestusi.
- Matemaatiline arutlemine: selle treening ja hindamine keskenduvad formaalsele matemaatikale, sealhulgas gümnaasiumi- ja ülikoolitaseme matemaatikavõistlustega seotud ülesannetele.
- Terviktõestuste genereerimine: mudel võib proovida koostada täieliku tõestuse, mitte ainult soovitada mitteametlikku järgmist sammu.
- Avatud kaaludega kasutuselevõtt: kaalud saab alla laadida, et katsetada mudelit lokaalselt ühilduvate masinõppevahenditega.
- Kontrollimine tõestusassistendiga: genereeritud koodi saab Leaniga sõltumatult kontrollida, mis annab valitud teoreemi ja keskkonna jaoks deterministliku õigsuskontrolli.
Mudeli võimalusi ei tohiks segi ajada üldotstarbelise programmeerimis- või vestlusoskusega. See võib genereerida koodi Leani tõestuste arendamise konkreetses kontekstis, kuid esitatud uurimismaterjal ei tõesta selle laialdast võimekust tarkvaraarenduses. Toimetuslik hinnang annab selle arutlusvõimele 8 punkti 10-st ja programmeerimisvõimele 3 punkti 10-st; need on võrdlevad toimetuslikud hinded, mitte teenusepakkuja avaldatud võrdlustesti tulemused.
Tulemused võrdlustestides
Mudeli väljalaske hindamise kohaselt saavutas see esitatud hindamisseadistuses Lean 4 miniF2F-i testvõrdlustestis tulemuse 50,0%. Seotud uurimistöös teatatakse ka 46,3% täpsusest terviktõestuste genereerimisel 64 näidisega ning miniF2F-i testi kumulatiivsest tulemusest 52,0%, kui kasutati suurt hulka genereerimisi.
Uurimustöö kohaselt tõestas mudel suure arvu katsete korral Formalized International Mathematical Olympiad võrdlustestis 148 ülesandest viis. Need näitajad mõõdavad formaalsete tõestuste genereerimist kindlate valimi moodustamise ja kontrollimise protseduuride korral. Neid ei tohiks tõlgendada garantiina, et üks viip genereerib toimiva tõestuse, ega piiramatu matemaatilise intelligentsuse mõõdikuna.
Praktilises kasutuses võib jõudlus oluliselt muutuda sõltuvalt teoreemivaldkonnast, viiba vormingust, saadaolevatest Leani teekidest, imporditud moodulitest, Leani versioonist, ajapiirangutest ja valimisse võetud kandidaatide arvust. Süsteem, mis genereerib mitu tõestust ja edastab iga kandidaadi Leanile, võib saavutada parema lõpliku õnnestumismäära kui ühe genereerimisega töövoog, kuid see nõuab ka rohkem arvutusressursse.
Kasutuselevõtt ja tehnilised piirangud
DeepSeek-Prover-V1 levitatakse allalaaditavate BF16-mudeli kaaludena ning selle suuruseks on märgitud 7 miljardit parameetrit. Esitatud dokumentatsioon ei avalda mudelipõhist kontekstiakna piirangut ega väljundi maksimaalset märgilimiiti, mistõttu tuleks neid väärtusi käsitleda teadmata väärtustena, mitte eeldada neid mudeli parameetrite arvu või mõne teise DeepSeeki väljalaske põhjal.
Lokaalne kasutuselevõtt nõuab sobivat riistvara, ühilduvaid mudeliteeke ja toimivat Leani 4 keskkonda kontrollimiseks. Mudelikaardil ei ole selle väljalaske jaoks loetletud ametlikku DeepSeeki hallatavat järelduspunkti. Samuti ei ole dokumenteeritud teenusepakkuja hallatavat tööriistakutsungit, voogedastust, peenhäälestust, vahemällu salvestamist, pakktöötlust, garanteeritud struktureeritud JSON-väljundit ega veebiotsingut. Neid võimalusi ei tohiks eeldada lihtsalt seetõttu, et mõni lokaalse kasutuselevõtu raamistik võib neid pakkuda.
Dokumenteeritud kasutusjuhus on nii sisend kui ka väljund tekstipõhine. Tekstisisend võib teoreemi kirjeldada või kodeerida ning tekstiväljund sisaldab Leani väiteid või tõestuskoodi. Dokumenteeritud ei ole pildi-, heli-, video-, muusika- ega muu otsese mittetekstilise väljundi võimalust. Ka mudeli väljund ise ei tõenda õigsust: Lean peab vastavas keskkonnas edukalt käivituma.
Hind ja juurdepääs
DeepSeek-Prover-V1 jaoks ei ole ametlikku majutatud API hinda avaldatud. Peamine juurdepääsuviis on avatud kaaludega mudeli allalaadimine DeepSeek AI Hugging Face'i organisatsioonist. Seetõttu ei ole võrdlemiseks kontrollitud sisend- ega väljundmärgi hinda, tellimustasu ega hallatud järeldusteenuse hinda.
Mudeli lokaalne kasutamine võib aidata vältida majutatud API tasusid, kuid see ei ole tasuta. Kasutajad vajavad riistvara või renditud arvutusressursse, salvestusruumi, mudeli teenindamise tarkvara ning ressursse Leani kontrollimiseks ja korduvateks tõestuskatseteks. Kulueelis sõltub seega kasutuselevõtu keskkonnast ja töökoormusest. Toimetuslik kuluhinne 8 punkti 10-st peegeldab allalaaditavate kaalude kättesaadavust ja dokumenteeritud API-arve puudumist; see ei ole DeepSeeki avaldatud hinnakujundusväide.
Tugevused ja piirangud
Tugevused
- See on kitsalt optimeeritud keeruka ja selgelt määratletud ülesande jaoks: formaalse Lean 4 matemaatika genereerimiseks.
- Avatud kaaludega levitamine toetab kohalikku uurimistööd, reprodutseeritavust ja katsetamist väljaspool hallatud vestlusliidest.
- Leani kontroll pakub tugevamat õigsusfiltrit kui üksnes mitteametliku teksti hindamine.
- Sünteetiline treeninguprotsess on üles ehitatud suure hulga formaalsete väidete ja kontrollitud tõestuste, mitte ainult loomulikus keeles esitatud matemaatika põhjal.
- Võrdlustestide tulemused näitavad automatiseeritud tõestuseotsingu praktilist kasulikkust, eriti mitme kandidaadi genereerimisel ja kontrollimisel.
Piirangud
- See on spetsialiseeritud mudel ega ole dokumenteeritult üldotstarbelise vestlusmudeli asendus.
- Genereeritud tõestus võib ebaõnnestuda vale taktika, sobimatu teoreemiväite, puuduva impordi, teegiversioonide erinevuse või ühildumatu Leani keskkonna tõttu.
- Vaja võib minna mitut katset, mis suurendab viivitust ja kohalikku arvutuskasutust.
- Selle väljalaske jaoks ei ole dokumenteeritud ametlikku majutatud API-t, standardset kommertshinda, konteksti piirangut ega väljundi maksimaalset limiiti.
- Kättesaadava toimetusliku hinnangu kohaselt on selle kasulikkus väljaspool Leani teoreemide tõestamist programmeerimisel piiratud.
- See mudel on DeepSeek-Proveri perekonna vanem väljalase, mistõttu võivad uusima perekonna võimekust otsivad kasutajad eelistada uuemat toetatud mudelit, kui see on saadaval.
Millal valida DeepSeek-Prover-V1?
Vali DeepSeek-Prover-V1 siis, kui peamine vajadus on Leani 4 tõestuste lokaalne või teadustööle suunatud genereerimine ning oled valmis kontrollimise töövoogu ise haldama. See sobib hästi närvivõrgupõhise teoreemitõestamise katsetamiseks, 2024. aasta DeepSeek-Proveri uurimistöö kordamiseks, matemaatikavõistluste ülesannete formaliseerimiseks kandidaat-tõestuste genereerimisel või selle uurimiseks, kuidas sünteetilised tõestusandmed mõjutavad keelemudelite treenimist.
See sobib vähem olukordadesse, kus vajad kohe kasutusvalmis majutatud teenust, prognoositavat API-arveldamist, garanteeritud vastuseskeeme, teenusepakkuja hallatavaid tööriistu, veebiotsingut või tavapärast rakenduste programmeerimist. Selgituste, väljaspool Leani toimiva koodi ja vestluspõhiste töövoogude jaoks võib sobivam olla üldotstarbeline keelemudel. Uuem teoreemitõestusmudel võib olla eelistatum juhul, kui olulisemad on perekonna tänapäevane jõudlus või uuendatud tööriistad, mitte selle konkreetse väljalaske reprodutseerimine.
Tõsise kasutuselevõtu korral käsitle DeepSeek-Prover-V1 kandidaatide generaatorina. Määra teoreem sihtkeskkonnas, genereeri üks või mitu tõestust, käivita Lean iga kandidaadi puhul, säilita ainult kontrollitud tulemused ning vaata saadud kood üle hooldatavuse ja sõltuvuseelduste seisukohast. Nii muutuvad mudeli tõenäosuslikud soovitused formaalselt kontrollitud matemaatilisteks artefaktideks.