Mis on DeepSeek-Prover-V1.5-RL?
DeepSeek-Prover-V1.5-RL on 7 miljardi parameetriga keelemudel automaatseks teoreemide tõestamiseks Lean 4-s. Lean on tõestusassistent ehk tarkvara, mis kontrollib, kas matemaatiline argument on formaalselt korrektne. Ainult mitteametliku selgituse tagastamise asemel genereerib mudel Leani lähtekoodi, mille saab esitada Leanile ja Mathlibile kontrollimiseks.
DeepSeek avaldas mudeli 15. augustil 2024 ning allalaaditavad kaalud on saadaval Hugging Face'is. See kuulub DeepSeek-Prover-V1.5 mudeliperesse ja on konkreetselt selle tugevdusõppe variant. Väljaannet tuleks käsitleda formaalse matemaatika, tõestuste genereerimise ja verifitseerijast juhitud keelemudelite katsete jaoks mõeldud teadusmudelina, mitte üldise vestlusassistendina.
DeepSeeki hilisemad mudeliväljaanded võivad uute projektide jaoks paremini sobida ning kaasasolevas uurimistöös kirjeldatakse seda mudelit vanema teadusväljaandena, mille on asendanud uuemad DeepSeek-Proveri mudelid. Sellest hoolimata on DeepSeek-Prover-V1.5-RL endiselt asjakohane, kui projekt nõuab just V1.5-RL kontrollpunkti või kui reprodutseeritav uurimistöö sõltub avaldatud treeningu- ja hindamisseadistusest.
Kuidas mudelit treenitakse
DeepSeek-Prover-V1.5-RL lähtestati mudelilt DeepSeek-Prover-V1.5-SFT, mis on sama seeria juhendatud peenhäälestusega versioon. Tugevdusõppe etapp kasutab Lean 4 tagasisidet: genereeritud tõestus saab kasulikku tagasisidet, kui tõestusassistent selle heaks kiidab, ning ebaõnnestunud tõestuskatseid saab tagasi lükata või kasutada edasise täiustamise suunamiseks.
Avaldatud treeningumeetod kasutab GRPO-laadset veebipõhist tugevdusõpet. Praktiliselt tähendab see, et mudel õpib kandidaat-tõestusi genereerides ja verifitseerijalt signaale saades, mitte ainult lõpetatud tõestuste näidetele tuginedes. See sobib Leaniga eriti hästi, sest korrektsust saab mehaaniliselt kontrollida. Tõestus, mis võib inimesele veenev tunduda, kuid ei kompileeru, ei ole formaalselt korrektne tõestus.
Laiem DeepSeek-Prover-V1.5 süsteem sisaldab ka RMaxTS-i, Monte Carlo puuotsingu meetodit mitme tõestustee uurimiseks. RMaxTS ei ole eraldi väljundviis ega mudeli eraldi versioon. See on järeldamise ajal kasutatav otsinguprotseduur, mis võib tõestusassistendi tagasiside ja sisemiste tasude abil alternatiivseid teid genereerida ja hinnata.
Mida mudel suudab teha
- Genereerida formaalsete matemaatiliste väidete põhjal Lean 4 teoreemitõestusi.
- Lõpetada Leani koodi ja töötada vahepealse taktikaseisu teabega.
- Genereerida tõestuskandidaate, mida saab kontrollida Lean 4 ja Mathlibiga.
- Toetada valimitamist, tõestuste kontrollimist, ekspertide iteratsiooni ja verifitseerijast juhitud keelemudelite uurimist.
- Käivituda kohapeal selliste tööriistade kaudu nagu Hugging Face Transformers või vLLM, sõltuvalt nõutavast keskkonnast ja riistvarast.
Selle väljund on tekst, peamiselt Leani kood ja sellega seotud tekstiline arutluskäik. Mudel ei genereeri algupäraselt pilte, heli, videot, manuseid ega käivitatavaid tegevusi. Kaasasolevate spetsifikatsioonide kohaselt ei paku see ka sisseehitatud veebiotsingu ega üldist tööriistade kasutamise süsteemi.
Avaldatud jõudlus
Autorite avaldatud hindamise kohaselt saavutas DeepSeek-Prover-V1.5-RL miniF2F-test'i võrdlusandmestikul 60,2% läbimismäära ja ProofNetis 22,6% läbimismäära kirjeldatud ühe läbimisega kogu tõestuse genereerimise seadistuses. Need tulemused näitavad, kas genereeritud formaalsed tõestused läbivad asjakohased võrdlusandmestiku kontrollid; need ei ole üldise matemaatilise võimekuse ega tarkvaraarenduse tulemused.
Kui laiem DeepSeek-Prover-V1.5 süsteem kombineeriti RMaxTS-i otsinguprotseduuriga, ulatusid avaldatud tulemused miniF2F-testis 63,5%-ni ja ProofNetis 25,3%-ni. Neid näitajaid ei tohiks omistada DeepSeek-Prover-V1.5-RL-i muutmata üksikule genereerimisele. Need kajastavad teistsugust järeldamise seadistust, mis kasutab täiendavat otsingut.
Võrdlustulemused sõltuvad viiba vormingust, valimieelarvest, tõestusotsingu seadistusest, verifitseerija konfiguratsioonist ja võrdlusandmestiku versioonist. Seetõttu on need uurimisväljaande mõistmiseks kasulikud, kuid ei taga, et konkreetne teoreem edukalt lahendatakse.
Kontekst, väljund ja juurutamine
Kaasasoleva mudeliteabe kohaselt on konteksti pikkus 4096 tokenit ja maksimaalne väljundi suurus 2048 tokenit. Konteksti väärtus põhineb ametliku hoidla vLLM-i konfiguratsioonil ja sellega seotud probleemi kontekstil. 2048 tokeni väärtus kajastab dokumenteeritud uurimistöö valimisseadistust, mitte eraldi avaldatud arhitektuurilist ranget maksimumi, mistõttu peaksid kasutajad kontrollima tegelikku piirangut enda valitud järeldamisseadistuses.
Juurutamine toimub kasutaja hallatavas keskkonnas. Ametlikud materjalid pakuvad allalaaditavaid kaale, uurimiskoodi ja kohaliku järeldamise juhiseid, mitte mudelipõhist majutatud API-t. Praktiline seadistus eeldab ühilduvat Linuxi keskkonda, Python 3.10-t, Lean 4-ja, MathLibi, asjakohaseid järeldamissõltuvusi ja piisavaid GPU-ressursse. Tegelik genereerimiskiirus sõltub riistvarast, kvantimisest või käituskeskkonna konfiguratsioonist, tõestuse pikkusest ja sellest, kas täiendav tõestusotsing on lubatud.
Kuna iga kandidaat-tõestus tuleb tavaliselt Leaniga üle kontrollida, ei võrdu kogu lahendamiskiirus lihtsalt keelemudeli tokenite genereerimise kiirusega. RMaxTS ja muud mahukat valimist kasutavad töövood võivad suurendada kehtiva tõestuse leidmise tõenäosust, kuid nõuavad ka rohkem genereerimisi ja kontrolltööd. See loob otsese kompromissi otsingueelarve, latentsuse ja arvutuskulu vahel.
Hind ja kättesaadavus
DeepSeek-Prover-V1.5-RL-i levitatakse avatud kaaludega mudelina, mille saab alla laadida ametlikust Hugging Face'i hoidlast. Kaasasolevas uurimismaterjalis ei ole dokumenteeritud mudelipõhist majutatud API hinnastust ega hallatud järeldamisplaani. Seetõttu ei ole kinnitatud sisend- ega väljundtokeni hinda, mida esitada.
Kohalik kasutus ei ole tegevuskulude mõttes tasuta: kasutajad peavad tagama ühilduva riistvara, salvestusruumi, seadistamisele kuluva aja ning elektri- või pilvearvutusressursid. Avatud kaaludega levitamine võib siiski olla teadlastele kasulik, kui nad vajavad kontrolli järeldamise, tõestuskontrolli integreerimise või reprodutseeritavate katsete üle, mitte hallatud lõpp-punkti.
Tugevused ja piirangud
Peamised tugevused
- Spetsialiseeritus: Mudel on treenitud Lean 4 formaalsete tõestuste genereerimiseks, mitte laiapõhjaliste keeleülesannete täitmiseks.
- Verifitseerijast juhitud arendus: Lean pakub objektiivse viisi kontrollimaks, kas genereeritud tõestuskood aktsepteeritakse.
- Ligipääsetavus teadustööks: Allalaaditavad kaalud ja kohaliku juurutamise tugi võimaldavad katseid ilma mudelipõhisest majutatud API-st sõltumata.
- Ühilduvus otsinguga: Mudelit saab kombineerida RMaxTS-i meetodiga, et uurida mitut tõestuskandidaati.
- Kasulik väljundvorming: Edukad tulemused on masinaga kontrollitav Leani kood, mida saab formaaliseerimise töövoogudesse integreerida.
Olulised piirangud
- Kitsas ülesandefookus: See ei ole loodud tavavestluseks, üldotstarbeliseks programmeerimiseks, laiapõhjaliseks tarkvaraarenduseks ega multimodaalseks analüüsiks.
- Kohaliku taristu koormus: Kasutajad peavad Lean 4, MathLibi ja järeldamisvirna ise paigaldama ning omavahel ühendama.
- Dokumenteeritud hallatud API puudub: Kaasasolevates materjalides ei ole majutatud lõpp-punkti, teenusetaseme kohustust ega mudelipõhist tokenihinnastust.
- Piiratud genereerimiseelarve: Loetletud konteksti- ja väljundiväärtused võivad piirata pikki teoreemiväiteid, tõestuskonteksti või mitmeastmelisi tõestusi.
- Otsing võib suurendada kulu ja latentsust: Mitu näidist ja verifitseerija kontrolli võivad tulemusi parandada, kuid nõuavad täiendavat arvutusvõimsust.
- Teadusväljaande staatus: Uuemad DeepSeek-Proveri väljaanded võivad olla värske töö jaoks eelistatavamad, kui oluline on uusim mudel või hooldatud tööriistakomplekt.
Millal valida DeepSeek-Prover-V1.5-RL?
Vali DeepSeek-Prover-V1.5-RL, kui peamine vajadus on Lean 4 tõestuskoodi kohapealne genereerimine ja projekt saab kasu konkreetsest DeepSeek-Prover-V1.5-RL-i kontrollpunktist. See sobib mõistlikult katseteks, mis hõlmavad formaalset matemaatikat, tõestuste lõpetamist, verifitseerija tagasisidet, tõestusotsingut ning juhendatud peenhäälestuse ja tugevdusõppe võrdlemist.
See sobib paremini kui üldotstarbeline keelemudel ka siis, kui formaalne verifitseerimine on töövoo keskmes. Üldmudel võib genereerida loetavaid matemaatilisi selgitusi või tavalist programmikoodi, kuid DeepSeek-Prover-V1.5-RL on treenitud konkreetsemale eesmärgile: genereerida tõestustermineid ja taktikaid, mida Lean saab kontrollida.
Muu võimalus võib olla sobivam, kui projekt vajab hallatud API-t, ajakohast tootetuge, suure läbilaskevõimega üldotstarbelist programmeerimist, veebipääsu, pildi- või helitöötlust või vestlusassistenti. Uuem teoreemitõestusmudel võib samuti olla eelistatavam, kui eesmärk on kasutada uusimaid võimalusi, mitte reprodutseerida V1.5 teadusväljaannet. Selle mudeli enda töövoos võib RMaxTS-i või mõne muu otsinguprotseduuri kasutamine olla otstarbekas, kui tõestuse õnnestumine on tähtsam kui minimaalne latentsus ja arvutuskulu.
Litsents ja lõpphinnang
Kaasasoleva hoidla kood on avaldatud MIT-litsentsi alusel. Mudeli kaalud kasutavad DeepSeeki mudelilitsentsi, mistõttu peaksid kasutajad enne ärilist juurutamist, levitamist või muutmist tutvuma mudelihoidlas oleva litsentsiga.
DeepSeek-Prover-V1.5-RL-i tuleks käsitleda keskendunud, avatud kaaludega uurimistööriistana Lean 4 teoreemide tõestamiseks. Selle peamine eelis on keelemudeli genereerimise ühendamine objektiivse tõestusverifitseerijaga. Peamised kulud on spetsialiseeritus, kohapealse juurutamise töö, piiratud üldotstarbeline kasutatavus ja tõestusotsinguks vajalik täiendav arvutusvõimsus. Teadlaste jaoks, kes vajavad selliseid formaalsete tõestuste võimalusi, võivad need kompromissid olla vastuvõetavad; üldiste tehisintellekti töökoormuste puhul on tõenäoliselt parem valik teistsugune mudelitüüp.