DeepSeek-Prover-V1.5-Base

Mis on DeepSeek-Prover-V1.5-Base?

DeepSeek-Prover-V1.5-Base on DeepSeeki arendatud 7 miljardi parameetriga avatud kaaludega keelemudel, mis on loodud formaalsete teoreemide tõestamiseks. Selle peamine väljund on Lean 4 tõestuskood: Leani tõestusassistendi keeles kirjutatud tekst, mida saab kompileerida ja formaalse teoreemi väite suhtes kontrollida.

See eristab mudelit üldotstarbelisest vestlusmudelist, mis võib tõestust loomulikus keeles selgitada. Loomulikus keeles selgitus võib kõlada veenvalt, kuid sisaldada samal ajal mõnd raskesti märgatavat viga. Leanis kirjutatud tõestus peab enne kehtiva formaalse tõestusena heakskiitmist vastama Lean süsteemi ja imporditud matemaatikateekide, sealhulgas Mathlibi reeglitele.

Mudel on DeepSeek-Prover-V1.5 väljalaske baaskontrollpunkt. Sama projekt hõlmas ka juhendatud peenhäälestusega ja tugevõppega variante. DeepSeek-Prover-V1.5-Base eelneb neile täiendavatele treeninguetappidele, mistõttu tuleks seda käsitleda pigem teadustöö alusena kui selle väljalaske kõige paremini toimiva versioonina.

Eesmärk ja koht DeepSeek-Proveri mudelisarjas

DeepSeek-Prover-V1.5-Base eeltreeniti mudelist DeepSeekMath-Base 7B ning kohandati seejärel formaalsetele matemaatikakeeltele. Selle roll on pakkuda mudelit, mis suudab teoreemiväidete ja ümbritseva lähtekoodi põhjal genereerida täielikke või osalisi Lean 4 tõestusi.

Laiem DeepSeek-Prover-V1.5 süsteem lisas selliseid tehnikaid nagu tõestusassistendi tagasiside ja RMaxTS, Monte Carlo puuotsingu meetod alternatiivsete tõestusteede uurimiseks. Need tehnikad kuuluvad laiemasse teoreemitõestussüsteemi ja hilisematesse treeningujärgsetesse etappidesse; neid ei tohiks käsitleda üksnes Base-kontrollpunkti enda funktsioonidena.

Praeguses DeepSeek-Proveri mudeliperes on see kontrollpunkt varasema põlvkonna mudel. DeepSeeki kirjelduse järgi on DeepSeek-Prover-V2-7B ehitatud DeepSeek-Prover-V1.5-Base peale ning selle konteksti pikkust on suurendatud 32K märgini. Seetõttu on V1.5-Base eriti asjakohane siis, kui reprodutseeritavus, juurdepääs algsele teadustöö kontrollpunktile või kohandatud eksperimenteerimine on uuema tõestusmudeli kasutamisest tähtsamad.

Kuidas see genereerib kontrollitavaid tõestusi

Tüüpilises töövoos annab kasutaja mudelile formaalse Leani teoreemi, selle lokaalsed definitsioonid ja asjakohase ümbritseva koodi. Seejärel ennustab mudel Leani märgendeid, mis võivad tõestuse lõpetada. Genereeritud tulemus edastatakse Leanile, mis kontrollib, kas tõestus läbib tüübikontrolli. Ebaõnnestumise korral võib tõestuse otsingusüsteem edastada veateate või proovida mõnd muud kandidaati.

See genereerimise ja kontrollimise lahutamine on mudeli kasulikkuse keskmes. DeepSeek-Prover-V1.5-Base pakub välja tõestuskoodi, kuid Lean ja Mathlib määravad, kas see kood kehtib. Seetõttu töötab mudel kõige paremini ühe osana tsüklis, mis ühendab keelemudeli genereerimise, kompileerimise, vigade käsitlemise ja võimaliku mitme kandidaadi hulgast otsimise.

Algajate jaoks on oluline mõista, et mudel ei kirjelda üksnes matemaatikat. See on suunatud formaalsele keelele, millel on range süntaks ja semantika. Kesktaseme kasutajate jaoks tähendab see praktiliselt, et mudeli kvaliteet sõltub mitte ainult genereeritud tekstist, vaid ka täpsest Leani versioonist, imporditud teekidest, teoreemikeskkonnast ja tõestuse kontrollimise seadistusest.

Teatatud võrdlustulemused

DeepSeek-Prover-V1.5 projekti hindamises saavutas Base-mudel teatatud hindamisseadistuse korral miniF2F-i testi võrdlusalusel tulemuse 42,2% ja ProofNetis 13,2%. Base-kontrollpunkti miniF2F-i tulemus saadi kolme näitega juhendamise abil.

Need on projekti teatatud võrdlustulemused, mitte iga teoreemi või juurutuse kohta kehtivad garantiid. Tulemuslikkus võib varieeruda sõltuvalt juhistest, teoreemi vormindusest, saadaolevast kontekstist, Leani ja Mathlibi versioonidest, kandidaatide valimist ning sellest, kas kasutatakse välist otsingu- või kontrollimisajastit.

Base-kontrollpunkti tulemus oli sama väljalaske juhendatud peenhäälestusega ja tugevõppega variantide omast teatatud hindamistes madalam. See erinevus on mudeli valimisel oluline: V1.5-Base pakub kasulikku avatud lähtekohta, kuid esitatud projektitulemuste põhjal ei ole see oma mudeliperes kõige tugevam otsene teoreemitõestuslahendus.

Tehnilised näitajad ja kättesaadavus

4 096 märgi pikkune kontekst on selle mudeli kohta esitatud teadustöös määratletud kontekstipikkus. See piirab seda, kui palju teoreemi koodi, definitsioone, importe, varasemat tõestusseisu ja juhiseid saab ühe päringuga esitada. Teadustöös ei määratleta eraldi maksimaalset väljundmärgendite arvu, mistõttu ei tohiks eeldada muud sõltumatut väljundpiiri peale teeninduskonfiguratsiooni ja kontekstiakna praktiliste piirangute.

Modelit saab alla laadida selle ametlikust Hugging Face'i repositooriumist ja käitada Transformeritel põhinevate tööriistadega. Projekti dokumentatsioon on suunatud Linuxile ja Python 3.10-le ning kirjeldab Lean 4, valmis Mathlibi keskkonda, vLLM-i näiteid ja Leani kontrollimise ajastit. Täpsed riistvaranõuded sõltuvad juurutusest ning esitatud materjalis neid ei määratleta.

Modaalsused, tööriistad ja API tugi

DeepSeek-Prover-V1.5-Base on tekstisisendi ja tekstiväljundiga mudel. Selle väljund on Leani koodi esindav tekst; esitatud mudeliandmete kohaselt ei paku see natiivset pildi-, heli-, video-, muusika-, kõne- ega embedding-väljundit. Seda ei ole dokumenteeritud multimodaalse mudelina.

Mudeli enda kohta ei ole dokumenteeritud sisseehitatud veebiotsingut, funktsioonikutsungeid ega hallatud tööriistakasutuse tuge. Kohalik rakendus võib ühendada mudeli väljundi Leani, Mathlibi, kompilaatori või tõestusotsingu ajastiga, kuid need on ümbritseva töövoo välised komponendid, mitte hostitud mudeli natiivsed tööriistad.

Esitatud teadustöös ei ole voogedastuse, esimese osapoole vahemälu ega peenhäälestuse tuge kontrollitud. Teadlased saavad töötada avatud kaaludega ning luua kohandatud järeldus- või treeningutorustikke, kuid see erineb pakkuja hallatava peenhäälestustoote või API-funktsiooni kasutamisest.

Peamised tugevused

• Suunitletud spetsialiseerumine: Mudel on treenitud formaalse matemaatikakeele ja Lean 4 tõestuste genereerimise jaoks, mitte laiaulatuslikeks vestlusülesanneteks.
• Mehaaniline kontrollimine: Lean ja Mathlib saavad kandidaat-tõestusi kontrollida, pakkudes objektiivset kehtivustesti selle asemel, et tugineda üksnes loomulikus keeles esitatud selgituse veenvusele.
• Juurdepääs avatud kaaludele: Allalaaditavad kaalud toetavad kohalikku eksperimenteerimist, reprodutseeritavat teadustööd, kohandatud teenindust ja edasist mudeliarendust.
• Kasulik teadustöö lähtekoht: Baaskontrollpunktina saab seda kasutada juhendamise, tõestusotsingu, peenhäälestuse ja kontrollimisest teadliku genereerimise uurimiseks.
• Selge integratsioonieesmärk: Selle kavandatud keskkond on konkreetne: Lean 4, Mathlib ja ümbritsev tõestuse kontrollimise töövoog.

Piirangud ja kompromissid

• Ei ole üldotstarbeline assistent: See ei ole mõeldud tavavestlusteks, laiapõhjaliseks teadmiste tööks, veebiotsinguks ega üldiseks programmeerimisabiks.
• Varasema põlvkonna kontrollpunkt: DeepSeek-Proveri mudelisarjas on selle välja vahetanud uuemad väljalasked, sealhulgas DeepSeek-Prover-V2.
• Hilisematest variantidest madalam teatatud tulemuslikkus: Base-mudeli tulemus oli projekti teatatud hindamistes DeepSeek-Prover-V1.5 SFT- ja RL-versioonide omast madalam.
• Uuemate seotud teadustöödega võrreldes lühem kontekst: Selle dokumenteeritud kontekstipikkus on 4 096 märki, samas kui esitatud DeepSeek-Prover-V2 teabes kirjeldatakse 32K märgi pikkust konteksti.
• Käitamise keerukus: Kasulik juurutus nõuab mudeli teenindamise taristut, Lean 4, Mathlibi ning mehhanismi genereeritud tõestuste kontrollimiseks ja vajaduse korral uuesti proovimiseks.
• Tuvastatud hostitud hinnastus puudub: Kasutajad peavad arvestama enda arvutus- või hostimiskuludega, sest ametlikku esimese osapoole märgipõhist hinnastust ei tuvastatud.

Need piirangud tekitavad otsese võimekuse ja mugavuse vahelise kompromissi. Kohalikult juurutatud avatud kontrollpunkt pakub kontrolli ja kohandamisvõimalusi, kuid nõuab rohkem arendustööd kui hallatud API. Mudeli kitsas spetsialiseerumine võib olla eelis Leani uurimistöös, kuid halb sobivus rakendustele, mis vajavad laia keele-, tööriista- või multimodaalset võimekust.

Kiiruse ja kulude kaalutlused

Esitatud teadustöös ei ole selle kontrollpunkti kohta pakkuja avaldatud kiirust ega märgipõhist hinda. Praktiline kiirus sõltub riistvarast, kvantimisest või teeninduskonfiguratsioonist, pakisuurusest, kandidaatide genereerimise strateegiast ja Leani kontrollimiseks kuluvast ajast.

7 miljardi parameetriga mudel on paljudest suurtest üldotstarbelistest mudelitest märgatavalt väiksem, mis võib muuta kohaliku eksperimenteerimise kättesaadavamaks, kuid teadustöö ei määra kindlat latentsusaega ega riistvaranõuet. Tõestusotsing võib suurendada ka järeldustöö mahtu, sest süsteem võib enne kehtiva tõestuse leidmist genereerida ja kontrollida mitut alternatiivset kandidaati.

Kulusid tuleks seega hinnata töövoo, mitte üksnes mudeli suuruse alusel. Järelduste tegemiseks kulub arvutusressurssi, kuid lisavahendeid võivad nõuda ka Leani kompileerimine, Mathlib, otsing, logimine ja korduvad ebaõnnestunud katsed. Avatud kaaludega juurutus võib pikaajalise teadustöö korral siiski olla kulutõhus, kuid väikeste või harvade töökoormuste puhul ei ole see automaatselt odavam.

Parimad kasutusjuhud

DeepSeek-Prover-V1.5-Base sobib eriti hästi järgmisteks kasutusjuhtudeks:

• Automaatse teoreemitõestamise ja formaalse matemaatika uurimine.
• Lean 4 tõestuste lõpetamine ja kandidaatide genereerimine.
• Eksperimendid tõestusotsingu, kontrollimisest saadava tagasiside ja puuotsingu meetoditega.
• Leani ja Mathlibi ümber kohalike teoreemitõestusagentide loomine.
• Avatud mudeli peenhäälestamine või kohandamine spetsialiseeritud formaalse matemaatika andmestiku jaoks.
• Uurimine, kuidas keelemudelid kompilaatorite ja formaalsete tõestusassistentidega suhtlevad.

See sobib halvemini üldotstarbeliseks vestluseks, tootmisrakendusteks, mis vajavad hallatud kommerts-API-t, multimodaalseteks töökoormusteks, veebiühendusega assistentideks või formaalsete tõestuste genereerimisega mitteseotud tarkvaraarendusülesanneteks.

Millal valida DeepSeek-Prover-V1.5-Base?

Vali see mudel siis, kui vajad spetsiaalselt avatud kaaludega Lean 4 tõestusmudelit ning soovid järelduste tegemise, kontrollimise või edasise treenimise üle otsest kontrolli. See sobib eriti hästi juhul, kui teadustöö eesmärk on DeepSeek-Prover-V1.5 töö reprodutseerimine või edasiarendamine, kohandatud tõestusotsingumeetodite katsetamine või genereerimise integreerimine kohalikku Leani torustikku.

Vali selle asemel hilisem DeepSeek-Proveri väljalase, kui uuem kontrollpunkt, pikem kontekst või tugevam teatatud teoreemitõestuse tulemuslikkus on algse Base-mudeli kasutamisest tähtsam. Esitatud teadustöös nimetatakse DeepSeek-Prover-V2-7B-d selle kontrollpunkti järeltulijaks, mis on ehitatud selle peale ja mille kontekst on 32K; selle mudeli üksikasjalikke võrdlusandmeid siin siiski ei esitata.

Vali selle asemel üldotstarbeline keelemudel, kui peamine vajadus on vestlus, lai programmeerimistugi, multimodaalne sisend või väljund, veebiotsing või hallatud API-toimingud. DeepSeek-Prover-V1.5-Base'i väärtus tuleneb selle spetsialiseerumisest formaalsetele tõestustele, mitte rakendusvaldkondade laiusest.