DeepSeek-Prover-V1.5-SFT

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

DeepSeek-Prover-V1.5-SFT on 7 miljardi parameetriga põhjuslik keelemudel, mis on treenitud spetsiaalselt automaatseks teoreemide tõestamiseks. Selle eesmärk on genereerida või täiendada formaalseid matemaatilisi tõestusi, mis on kirjutatud keeles Lean 4 — programmeerimiskeeles ja tõestusabilis, mida kasutatakse matemaatiliste väidete väljendamiseks ning kavandatud tõestuste loogilise kehtivuse kontrollimiseks.

Erinevalt üldotstarbelisest vestlusmudelist ei ole see eelkõige loodud loomulikus keeles küsimustele vastamiseks. Selle peamine väljund on Lean 4 koodi sisaldav tekst. See kood on kasulik ainult juhul, kui see läbib Leani kontrolli, mistõttu on mudeli näiline ladusus vähem oluline kui see, kas genereeritud tõestus kompileerub vastava teoreemi, definitsioonide ja imporditud Mathlibi teekide kontekstis.

Nimetus SFT viitab juhendatud peenhäälestusele (supervised fine-tuning). DeepSeek-Prover-V1.5 treeningprotsessis tähistab see kontrollpunkt juhendatud õppimise etappi ning paikneb Base'i ja tugevdusõppe variantide kõrval. Kaasasolevas uurimuses kirjeldatakse seda pigem vana, pärand- või asendatud kontrollpunktina kui praeguse üldotstarbelise DeepSeek pakkumisena.

Eesmärk ja positsioon

DeepSeek-Prover-V1.5-SFT lähtestati DeepSeekMath-Base'ist tuletatud 7B baasmudeliga ning kohandati seejärel formaalse matemaatika keele jaoks. Selle juhendatud peenhäälestuses kasutati täiustatud Lean 4 teoreemitõestuse andmestikku, mis sisaldas tõestusjärjendeid ja kontrollimisega seotud teavet. Treeningprotsess toetas nii mõttekäigu (chain-of-thought) kui ka mõttekäiguta tõestuste genereerimise režiime.

Praktilises mõttes on mudel formaalsete tõestussüsteemide jaoks kandidaatide genereerija. Tüüpilises töövoos palutakse sellel teoreem lõpule viia või tõestuskatse luua ning tulemus saadetakse kontrollimiseks Leanile. Kui katse ebaõnnestub, võib rakendus küsida täiendavaid näidiseid, koodi parandada või uurida eraldi otsinguprotsessi kaudu mitut alternatiivi.

See positsioon on oluline, kui võrrelda mudelit tavaliste kodeerimis- või vestlusmudelitega. DeepSeek-Prover-V1.5-SFT on kitsama kasutusalaga, kuid selle väljund on sobitatud formaalse kontrollijaga. Seetõttu on see kõige asjakohasem teoreemitõestussüsteeme loovatele teadlastele ja arendajatele, mitte kasutajatele, kes otsivad vestlusabilist või laia kasutusotstarbega tarkvaraarendustööriista.

Kontrollitud tehnilised andmed

4096 tokeni suurune kontekstiaken piirab seda, kui palju teoreemi konteksti, imporditud materjali, varasemat tõestusseisundit ja soovitud lõpuleviimist saab ühe genereerimise käigus esitada. Kaasasolevas uurimuses ei tuvastata eraldi maksimaalse väljundi tokenite seadistust, mistõttu ei tohiks eeldada kindlat väljundipiiri, mis ületaks mudeli konfiguratsiooni ja saadaoleva konteksti seatud piiranguid.

Jõudlus võrdlustestides

Esitatud DeepSeek-Prover-V1.5 hindamises saavutas SFT kontrollpunkt miniF2F-i testikomplektil kirjeldatud suure näidiste arvuga hindamise korral 57,4% läbimismäära ning võrdlustabeli järgi ProofNetis 22,9%. Sama uurimus teatab ProofNetis ühe läbimise seadistuses 128 näidise eelarvega üldiseks tulemuseks 17,9%.

Need näitajad pärinevad konkreetsest hindamisseadistusest ega garanteeri tulemust iga teoreemi või juurutuse puhul. Formaalse tõestamise jõudlus võib muutuda sõltuvalt viipamisest, genereeritavate kandidaatide arvust, teoreemi eeltöötlusest, saadaolevatest importidest, kontrollija konfiguratsioonist ja otsingustrateegiast. Neid tulemusi ei tohiks samuti segi ajada üldise arutlusoskuse skooriga.

Esitatud SFT tulemused jäävad mitmes seadistuses hilisema DeepSeek-Prover-V1.5-RL-i tulemustele alla. Sellest hoolimata on SFT kontrollpunkt kasulik, kui teadlased soovivad juhendatud etappi iseseisva mudelina kasutada, vajavad reprodutseeritavateks katseteks avatud kaalusid või tahavad lisada oma kontrollijapõhise otsingu ja täpsustamise meetodeid.

Kuidas tõestamise töövoog toimib

Kasutaja esitab tavaliselt teoreemi väite, seda ümbritseva Leani konteksti ja võimaliku osalise tõestuse. Seejärel genereerib mudel Lean 4 süntaksis kandidaatlõpetuse. Kandidaat edastatakse Leanile ja Mathlib4-le, kus tõestusabiline kontrollib tüüpe, taktikaid, viidatud definitsioone ja loogilist kehtivust.

Ebaõnnestunud kandidaat ei tähenda tingimata, et teoreem käib mudelile üle jõu. See võib sisaldada süntaksiviga, kasutada kättesaamatut lemmat, mõista kohalikku tõestusseisundit valesti või valida matemaatiliselt usutava, kuid formaalselt sobimatu taktika. Seetõttu genereerivad praktilised süsteemid sageli mitu kandidaati ning suunavad kontrollija vead parandamis- või otsingutsüklisse tagasi.

Ametlik repositoorium näitab järeldamist Hugging Face Transformersiga ning pakub eraldi tõestuse kontrollimise töövoogu, mis hõlmab Lean 4 ja Mathlibi. Enne kvantimist või muid juurutamise optimeerimisi on kontrollpunkti suurus Hugging Face'i repositooriumis ligikaudu 13,8 GB. Dokumenteeritud seadistus on mõeldud Linuxile ja Python 3.10-le.

Võimekus ja piirangud

Arutlus- ja kodeerimisvõimekus

Mudeli arutlusvõime on pigem spetsialiseeritud kui lai. See on treenitud siduma formaalsed matemaatilised eesmärgid Leani tõestusterminite või taktikajärjenditega, mistõttu on see asjakohane teoreemitõestuse ja formaalse matemaatika uurimisel. Ka selle kodeerimisväljund on spetsialiseeritud: üldise rakendusekoodi asemel genereerib see Lean 4 lähtekoodi.

Praktiliselt on selle tugevaim omadus kontrollitavus. Genereeritud tõestust saab mehhaaniliselt kontrollida, nii et rakendus võib ebaõige väljundi tagasi lükata, selle asemel et pidada näiliselt usutavat teksti õigeks. See muudab mudeli sobivaks süsteemidele, kus tõestuse korrektsus on vestluslikust mitmekülgsusest olulisem.

Olulised piirangud

• 4096 tokeni suurune kontekstiaken on suurte formaalsete arenduste või ulatusliku kohaliku kontekstiga teoreemiväidete jaoks suhteliselt lühike.
• Kaasasolevas uurimuses ei ole dokumenteeritud kindlat maksimaalse väljundi tokenite arvu.
• Edukas genereerimine eeldab üldjuhul Leani kontrolli ning võib saada kasu korduvast näidiste genereerimisest, parandamisest või puuotsingust.
• Mudel ei ole üldotstarbeline vestlusabiline ning seda ei esitleta multimodaalse süsteemina.
• Dokumenteeritud ametlikku veeb otsingu, tööriistade kasutamise ega funktsioonide kutsumise võimekust ei ole. Lean ja Mathlib on väline kontrollitaristu, mitte mudeli sisseehitatud tööriistad.
• See ei paku loomupärast pildi-, heli-, video- ega muud mittetekstilist väljundit.
• Kontrollpunkti kohta ei ole dokumenteeritud esimese osapoole majutatud API-t ega kasutuspõhist hinda.
• Mudeli vanus ja asendatud staatus võivad tähendada, et uute projektide puhul sobib paremini mõni hilisem teoreemitõestusmudel, kui prioriteediks on suurem võrdlustestide jõudlus või uuemad tööriistad.

Kulude, kiiruse ja juurutamise kompromissid

Kuna DeepSeek-Prover-V1.5-SFT-i levitatakse allalaaditavate kaaludena, ei ole sellel pakkuja API-hinda, mida majutatud teenuste tokenihindadega võrrelda. Rahaline kompromiss seisneb kohaliku taristu ja kontrolli vahel. Ise majutamine võib toetada privaatseid andmeid, korratavaid katseid ja piiranguteta integreerimist Leani kontrollijaga, kuid kontrollpunkti ligikaudu 13,8 GB suurune repositoorium ning mudeli järeldamise ja tõestuste kontrollimise nõuded tekitavad tegevuskulusid.

Uurimuses antakse toimetuslikuks kiirusehindeks 4 ja kuluhindeks 9, kuid need on võrdlevad toimetuslikud hinnangud, mitte DeepSeeki avaldatud tehnilised näitajad. Neid ei tohiks tõlgendada mõõdetud latentsuse ega garanteeritud tõestuse maksumusena. Tegelik kiirus sõltub riistvarast, kvantimisest, pakisuurusest, näidiste arvust ning tõestuste kompileerimisele ja kontrollimisele kuluvast ajast. Paljusid kandidaate genereeriv töövoog võib läbimismäära parandada, kuid suurendab koguarvutusmahtu.

Võrreldes majutatud üldotstarbelise mudeliga pakub see kontrollpunkt suuremat otsest kontrolli juurutamise üle ja spetsialiseeritud tõestuste genereerimise eesmärki, kuid vähem mugavust. Kasutajad peavad mudeli, Lean 4, Mathlib4 ning ümbritseva järeldamis- või otsingukoodi ise installima ja hooldama.

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

Vali DeepSeek-Prover-V1.5-SFT siis, kui põhiülesanne on Lean 4 formaalsete tõestuste genereerimine ja vajad kohalikeks katseteks allalaaditavaid kaalusid. See sobib hästi järgmisteks kasutusjuhtudeks:

• Automaatse teoreemitõestuse ja formaalse matemaatika uurimine.
• Lean 4 tõestuste lõpuleviimine ja kandidaatide genereerimine.
• Kontrollijapõhine genereerimine, tõestuste parandamine ja puuotsingu katsed.
• DeepSeek-Prover-V1.5 töövoo juhendatud õppimise etapi reprodutseeritavad uuringud.
• Privaatsed või võrguühenduseta töövood, kus majutatud API ei sobi.

Hilisem või tugevdusõppega täiendatud teoreemitõestusmudel võib olla sobivam siis, kui peamine eesmärk on võrdlustestide jõudlus. Tarkvaraarenduseks, loomulikus keeles selgitamiseks, laiemaks matemaatiliseks aruteluks või pika kontekstiga tööks võib eelistada üldist kodeerimis- või vestlusmudelit. Majutatud teenus võib samuti olla parem valik, kui taristu hoolduse vähendamine on olulisem kui kogu kohaliku töövoo kontrollimine.

Kokkuvõte

DeepSeek-Prover-V1.5-SFT-i tuleks mõista eelkõige spetsialiseeritud avatud kaaludega Lean 4 tõestuste genereerijana, mitte üldise tehisintellekti assistendina. Selle väärtus seisneb juhendatud tõestuste genereerimise treeningu ja mehhaanilise kontrolli ühendamises: mudel pakub formaalset koodi ning Lean otsustab, kas see kood kehtib. 7B kontrollpunkt, 4096 tokeni pikkune kontekst, avatud kaaludega levitamine ning teatatud miniF2F-i ja ProofNeti tulemused muudavad selle kasulikuks uurimisobjektiks, kuid majutatud API puudumine, piiratud kontekst, sõltuvus välistest tööriistadest ja asendatud staatus vähendavad selle sobivust kohe kasutatavaks tootmislahenduseks.