Mis on DeepSeek-Prover-V2-671B?
DeepSeek-Prover-V2-671B on DeepSeeki avatud kaaludega keelemudel, mis on loodud spetsiaalselt formaalsete matemaatiliste teoreemide tõestamiseks. Selle peamine väljund on Lean 4 kood: deklaratsioonid, taktikad ja tõestusliikmed, mida saab kontrollida Leani ning asjakohaste matemaatikateekide abil. See eristab mudelit üldotstarbelisest keelemudelist, mis selgitab lahendusi tavalises proosas. Veenvana näivast vastusest siin ei piisa – tõestus on kasulik ainult siis, kui Leani tööriistaahel selle aktsepteerib.
DeepSeek avaldas mudeli 30. aprillil 2025 koos väiksema mudeliga DeepSeek-Prover-V2-7B. 671B versioon on selle mudeliperekonna suurem liige ning mõeldud nõudlikeks teadus- ja inseneritöödeks. See on allalaaditavate kaaludena saadaval DeepSeeki ametlikus mudelirepositooriumis, mitte selgelt dokumenteeritud esimese osapoole majutatud API-tootena.
Mudelit tasub käsitleda tõestuste genereerimise komponendina. Tüüpilise töövoo puhul antakse mudelile formaalne teoreemiväide või sobivas Leani keskkonnas esitatud matemaatikaülesanne, palutakse tal pakkuda tõestust ning saadetakse tulemus seejärel kontrollimiseks Leanile. Ebaõnnestunud tõestusi saab mudeli ümber tehtava täiendava otsingu, viipade või orkestreerimise abil parandada.
Koht DeepSeek-Proveri mudeliperekonnas
DeepSeek-Prover-V2-671B kuulub DeepSeeki DeepSeek-Proveri perekonda, mis keskendub formaalsele matemaatilisele arutlusele, mitte üldisele vestlusele, piltide mõistmisele või meedia genereerimisele. Mudel on treenitud DeepSeek-V3-Base'i põhjal ja kasutab DeepSeek-V3 arhitektuuri. Selle ekspertide segu arhitektuuris on kokku ligikaudu 671 miljardit parameetrit.
Seotud 7B versioon on praktilisem valik juhul, kui riistvara, teenindamise kulu või latentsus on tähtsam kui suurima kontrollpunkti mahutavus. Esitatud uurimus ei tõesta, et väiksem mudel saavutaks 671B mudeliga võrreldavaid tulemusi. Seetõttu tuleks valikut käsitleda juurutuse ja võimekuse kompromissina, mitte eeldada, et mõlemad kontrollpunktid on omavahel asendatavad.
Kuidas mudelit treenitakse
DeepSeek kirjeldab treeninguprotsessi, mis põhineb rekursiivsel teoreemide tõestamisel. Lihtsustatult võib keerulise teoreemi jagada väiksemateks alamülesanneteks ning saadud alamprobleeme kasutada formaalsete treeningnäidete koostamiseks. DeepSeek-V3 aitab keerukaid matemaatikaülesandeid osadeks jagada ja tõestusandmeid sünteesida. Seejärel kohandatakse tõestusmudelit selle algmaterjali põhjal.
Treeninguprotsessis kasutatakse ka formaalsest kontrollist saadud binaarse tagasisidega tugevdusõpet. Genereeritud tõestus kas läbib hindamisseadistuse korral formaalse kontrollija või ei läbi seda. Selline tagasiside on konkreetsem kui subjektiivne hinnang sellele, kas selgitus kõlab usutavalt, sest Lean saab kehtetud tõestusliikmed ja taktikad tagasi lükata.
Need meetodid selgitavad mudeli spetsialiseerumist. Mudelit ei ole lihtsalt suunatud matemaatikast rääkima, vaid optimeeritud keeruliseks teisenduseks, mille käigus muudetakse informaalne või poolformaalne matemaatiline idee Lean 4 süntaksile, teekidele ja tuuma kontrollile vastavaks koodiks.
Formaalse tõestamise võimekus ja avaldatud tulemused
DeepSeek-Prover-V2-671B on loodud Lean 4 tõestuste genereerimiseks ja tõestuste otsingu töövoogude toetamiseks, kus kandidaatväljundeid korduvalt kontrollitakse. Avaldatud võimekuste hulka kuuluvad:
- Lean 4 tõestuskoodi, sealhulgas tõestusliikmete ja taktikate genereerimine.
- Keerukate probleemide lahendamine rekursiivse alamülesanneteks jagamise abil.
- Kandidaatide loomine automaatseks teoreemide tõestamiseks ja matemaatika formaliseerimiseks.
- Pikkade deklaratsioonide, tõestuskontekstide ja teegimaterjaliga töötamine seadistatud positsioonipiiri ulatuses.
- Allalaaditavate mudelikaalude kaudu enda hallatava eksperimenteerimise toetamine.
DeepSeek teatab MiniF2F-test'i võrdlustestis 88,9% läbimismäärast ning PutnamBenchi hindamisseadistuse puhul lahendustest 49 ülesandele 658-st, nagu on kirjeldatud tehnilises aruandes. Need on teenusepakkuja teatatud võrdlustulemused, mitte ühe konkreetse projekti garantiid. Tulemused võivad sõltuda viipamisest, teoreemi esitusest, teekide versioonidest, otsingustrateegiast, kontrollitsüklitest ja kasutada olevast arvutusvõimsusest. Eelkõige ei tohi genereeritud tõestust pidada matemaatiliselt kontrollituks enne, kui Lean selle kompileerib ja kontrollib.
Kontekst, väljund ja toetatud modaalsused
Ametlik kontrollpunkti konfiguratsioon määrab maksimaalseks positsioonimanuse pikkuseks 163 840 tokenit. See on allalaaditava mudeli puhul avaldatud asjakohane kontekstiga seotud piirang. See näitab, et kontrollpunkt on seadistatud väga pikkade järjestuste jaoks, mis võib olla kasulik juhul, kui teoreem sõltub ulatuslikest deklaratsioonidest, imporditud teegi kontekstist või vahepealsest tõestusmaterjalist. Tegelik kasutatav maht võib sõltuda ka järeldusraamistikust, mälust, paralleeltöötlusest ja viiba koostamisest.
Selle kontrollpunkti täpset genereeritavate tokenite maksimaalset arvu esitatud uurimuses ei tuvastatud. Mudel võib toota tekstilist väljundit, eelkõige Lean 4 koodi ja sellega seotud arutluskäike, kuid seda väljundit ei tohi segi ajada otsese käivitamise või kontrollimisega. Tulemuse kontrollimiseks on endiselt vaja eraldi Leani keskkonda.
Kontrollpunkti sisend ja väljund on tekstipõhised. Esitatud materjalis ei ole dokumenteeritud toetatud pildi-, heli- ega videosisendit või -väljundit. Seetõttu ei sobi see multimodaalseteks genereerimistöövoogudeks. Selle väljund ei ole olemuslikult struktureeritud API-vastus ning baaskontrollpunkti dokumentatsiooni põhjal ei tohiks eeldada struktureeritud väljundi ega JSON-režiimi tuge.
Arhitektuur ja juurutusnõuded
Ligikaudu 671 miljardi parameetriga DeepSeek-Prover-V2-671B vajab käitamiseks märksa rohkem ressursse kui väike lokaalne mudel. Parameetrite arv mõjutab mälu-, salvestus- ja ribalaiusevajadust, laadimisaega ning praktiliseks järeldamiseks vajalikku riistvara hulka. Täielik juurutus vajab ka kontrollpunkti toetavat järelduspakki ja toimivat Leani keskkonda tõestuste kontrollimiseks.
DeepSeek pakub näiteid, mis ühilduvad Transformers'i, vLLM-i ja SGLangiga. Kvantimine ja hajutatud järeldamine võivad vähendada praktilisi ressursinõudeid, kuid ei muuda mudelit kergeks töölauatööriistaks. Esitatud uurimus ei anna lõplikku minimaalset GPU-konfiguratsiooni, seega tuleks riistvaranõudeid hinnata valitud täpsuse, kvantimismeetodi, järeldusraamistiku, pakisuuruse ja sihtlatentsuse põhjal, mitte tuletada neid üksnes parameetrite arvust.
Tootmiskõlbliku tõestuste otsingu süsteemi puhul on mudeli teenindamine vaid üks arhitektuuri osa. Ümbritsev süsteem võib vajada teoreemide otsingut, viipade koostamist, kandidaatide järjestamist, korduvat genereerimist, ajalõppude käsitlemist ja Leani kompileerimist. 671B kontrollpunkt sobib kõige paremini siis, kui keerukate tõestuste genereerimisel saavutatav eeldatav paranemine õigustab seda käitamise keerukust.
Hinnastus ja API kättesaadavus
DeepSeek-Prover-V2-671B sisend- ega väljundtokeni ametlikku hinda ei tuvastatud. Esitatud uurimuses ei tuvastatud ka esimese osapoole hallatavat DeepSeeki API-t selle konkreetse allalaaditava kontrollpunkti jaoks. Seetõttu ei ole teatamiseks kontrollitud majutatud kuuhinda, arveldusperioodi ega tavapärast API-kulu.
Selle tegelik kulu sõltub hoopis mudeli allalaadimiseks, teenindamiseks ja kontrollimiseks kasutatavast taristust. Enda hallatav juurutus võib anda kontrolli andmete ja mudeli käitamise üle, kuid arvesse tuleb võtta riistvara, elektri, inseneritöö, salvestusruumi ja hoolduse kulusid. Majutatud taristu võib eksperimenteerimise lihtsamaks muuta, kuid teenusepakkuja hind käiks sellisel juhul selle majutuslahenduse, mitte mudeli enda ametliku hinna kohta.
Oluline kompromiss on ka kiirus. 671B suurusjärk ja formaalse kontrolli tsükkel muudavad mudeli väikese latentsusega interaktiivsete rakenduste jaoks halvasti sobivaks, välja arvatud juhul, kui juurutusel on märkimisväärne paralleelne riistvara ja tõhus otsingukujundus. Mudeli väärtus seisneb eelkõige keerukates arutlusülesannetes, kus tõestuse kvaliteet on kiiretest vestlusvastustest tähtsam.
Tugevused ja piirangud
Tugevused
- Tugev spetsialiseerumine: Mudel on treenitud Lean 4 formaalsete tõestuste genereerimiseks, mitte laiapõhjaliseks vestlusabiliseks.
- Kontrollile suunatud treening: Formaalse kontrolli tagasisidega tugevdusõpe suunab mudelit looma väljundeid, mida saab tõestusassistendiga testida.
- Suur mudelivõimekus: 671B ekspertide segu arhitektuur on mõeldud keerukaks matemaatiliseks arutluseks ja tõestuste otsingu probleemideks.
- Avatud kaaludega juurdepääs: Teadlased saavad kontrollpunkti ühilduvate järeldustööriistade abil uurida ja juurutada, sõltumata dokumenteeritud suletud lähtekoodiga lõpp-punktist.
- Pikk seadistatud positsioonipikkus: 163 840 tokeni seadistus võimaldab mahutada ulatuslikku teoreemi- ja teegikonteksti.
Piirangud
- Suur juurutuskoormus: Kontrollpunkt vajab märksa rohkem mälu, riistvara ja süsteemiarendust kui väiksemad tõestusmudelid.
- Kontrollimine on kohustuslik: Ladus Lean-kood on ainult kandidaat, kuni Leani tuum ja asjakohased teegid selle aktsepteerivad.
- Piiratud tootetugi: Selle kontrollpunkti täpset väljundtokenite piiri, majutatud hinda ega esimese osapoole API-t ei ole tuvastatud.
- Piiratud modaalsuste tugi: Mudel on mõeldud teksti ja Lean-koodi jaoks, mitte piltide, heli, video või üldiste multimodaalsete ülesannete jaoks.
- Ei ole üldotstarbeline assistent: See ei ole loomulik valik tavavestluseks, veeb otsinguks, laiapõhjaliseks teadmistepõhiseks tööks ega väikese latentsusega kliendirakendusteks.
- Vajab süsteemiintegratsiooni: Kasulikud juurutused vajavad ühilduvat järeldusraamistikku ja eraldi Leani kontrollitsüklit.
Millal valida DeepSeek-Prover-V2-671B?
Vali see mudel siis, kui keskne probleem on keerukas formaalne matemaatika ja sul on võimalik käitada suurt avatud kaaludega kontrollpunkti. See sobib hästi automaatse teoreemide tõestamise, Lean 4 tõestuste sünteesi, võistlusmatemaatika formaliseerimise, kontrollijaga suunatud genereerimise ning süsteemide uurimiseks, mis võrdlevad või otsivad mitme tõestuskandidaadi seast.
See on eriti atraktiivne juhul, kui oluline on enda hallatav juurutus, mudeli uuritavus või kontroll tõestusandmete üle. Avatud kaaludega formaat võib olla kasulik ka eksperimentides, mis vajavad kohandatud järeldusorkestreerimist, mitte fikseeritud majutatud API-t. Avaldatud MiniF2F-i ja PutnamBenchi tulemused annavad tõendeid asjakohase võimekuse kohta, kuid neid tuleks käsitleda konkreetsete võrdlustestide tulemustena, mitte universaalsete jõudlusgarantiidena.
Kaalu väiksemat DeepSeek-Prover-V2-7B mudelit, kui ülesanne on sarnane, kuid olemasolev riistvara, reageerimisaeg või käituskulu on tähtsam. Üldotstarbeline arutlusmudel võib olla sobivam informaalsete matemaatiliste selgituste, tavalise tarkvaraarenduse või vestluskasutuse jaoks, kui formaalne Leani kontrollimine ei ole peamine nõue. Majutatud teenus võib olla eelistatav ka siis, kui meeskond soovib prognoositavat juurutust ilma 671B kontrollpunkti haldamata, kuigi esitatud uurimuses ei tuvastatud selle täpse mudeli ametlikku majutatud teenust.
Praktilise hindamise kontrollnimekiri
Enne DeepSeek-Prover-V2-671B kasutuselevõttu testi seda tüüpiliste Lean-projektidega, mitte ära tugine ainult võrdlustestide pealkirjades toodud näitajatele. Mõõda kompileeruvate genereeritud kandidaatide osakaalu, iga teoreemi jaoks vajalike katsete arvu, otsast lõpuni latentsust, mälukasutust ja korduva tõestuste otsingu kulu. Kontrolli katses kasutatud täpset Leani versiooni, imporditud teeke, järeldusraamistikku, täpsust ja kvantimise seadistusi.
Eralda süsteemi kujunduses ka tõestuse genereerimine selle valideerimisest. Salvesta algne teoreem, genereeritud kandidaat, kontrollija väljund ja keskkonna andmed, et edukad tulemused oleksid korratavad. See on eriti oluline, sest ühes teegi- või tööriistaahela konfiguratsioonis töötav tõestus võib teises vajada muudatusi.
DeepSeek-Prover-V2-671B-d tasub seega käsitleda suure võimekusega avatud kaaludega mootorina formaalsete tõestuste uurimiseks, mitte valmiskujul teoreemide tõestamise teenusena. Selle spetsialiseeritud treeningu, pika seadistatud konteksti ja avaldatud võrdlustestide tulemuste kombinatsioon on õige töökoormuse puhul veenev, kuid mudeli suurus, teadmata majutatud hind ja välise kontrollimise vajadus muudavad hoolika taristuplaneerimise hädavajalikuks.