Mis on StepFun-Prover-Preview-7B?
StepFun-Prover-Preview-7B on StepFuni välja töötatud avatud kaaludega keelemudel formaalsete matemaatiliste teoreemide tõestamiseks. Selle väljund on tekst, kuid oluline tekstiliik on Lean 4 tõestuskood: masinaga kontrollitav kirjeldus selle kohta, kuidas teoreem tuleneb oma eeldustest ja kättesaadavatest definitsioonidest.
Mudel põhineb mudelil DeepSeek-R1-Distill-Qwen-7B ning seda on täiendavalt treenitud tõestuste genereerimise ülesannete jaoks. Avaldatud mudelihoidla kirjeldab seda ligikaudu 8 miljardi parameetriga BF16-mudelina. BF16 on vähendatud täpsusega numbrivorming, mida kasutatakse tavaliselt järeldamise ajal mälunõuete vähendamiseks, kuigi kaasasolev uurimus ei täpsusta selle kontrollpunkti käitamiseks vajalikku riistvara.
„Preview“ ehk eelvaate tähistus on oluline. Tegemist on uurimistööle suunatud väljalaskega, mis on mõeldud formaalse arutluse ja verifikaatoriga juhitud genereerimise katsetamiseks, mitte laialdaselt toetatud kommertsassistendiks. See on StepFuni mudelihoidlate kaudu avalikult saadaval ning välja antud Apache License 2.0 alusel.
Kuidas Lean 4 tõestusprotsess toimib
StepFun-Prover-Preview-7B on üles ehitatud mudeli ja Lean 4 vahelisele suhtlusele. Lean 4 on programmeerimiskeel ja tõestusassistent, mis suudab kontrollida, kas pakutud formaalne tõestus on kehtiv. Selle asemel et käsitleda mudeli esimest vastust lõplikuna, saab töövoog edastada genereeritud tõestuse visandi Lean 4-le ning kasutada saadud vigu või kontrollitagasisidet järgmise katse suunamiseks.
- Tõestuse genereerimine: mudel saab formaalse teoreemi või sellega seotud tõestusülesande ning pakub välja Lean 4 koodi.
- Kontrollimine: pakutud koodi hinnatakse Lean 4 keskkonnas.
- Parandamine: mudel kasutab keskkonna tagasisidet tõestuse parandamiseks või täiendamiseks.
- Lõpetamine: protsess jätkub seni, kuni Lean 4 tõestuse heaks kiidab või olemasolev genereerimise eelarve ammendub.
See töövoog on mudeli määrav võimekus. See ei ole sama mis üldise API verifitseeritud algupärane funktsioonikutsumine. Uurimus käsitleb tööriistade kasutamist Lean 4 suhtlusprotokolli toetamisena, mitte tõendina, et mudel pakub standardset OpenAI-ga ühilduvat funktsioonikutsumist või üldotstarbelist agendiliidest.
Peamised tugevused
Formaalne ja masinaga kontrollitav väljund
Mudel on suunatud tõestustele, mida saab Lean 4 abil kontrollida, mitte ainult usutavatele loomulikus keeles selgitustele. See on väärtuslik juhul, kui korrektsus tuleb formaalse süsteemi abil kindlaks teha. Lean 4 heaks kiidetud genereeritud tõestus on läbinud verifikaatori kontrollid asjakohase teoreemi, imporditud moodulite, definitsioonide ja tõestussammude osas.
Verifikaatoriga juhitud arutlus
Paljud keelemudelid suudavad genereerida paljutõotava tõestusidee, kuid ebaõnnestuvad süntaksi, puuduvate lemmade, tüübivastuolude või kehtetute vahepealsete sammude tõttu. StepFun-Prover-Preview-7B on loodud nende probleemide lahendamiseks korduva suhtluse kaudu Lean 4-ga. Tagasisideahel annab mudelile konkreetset teavet selle kohta, miks kandidaat-tõestus ebaõnnestus, muutes süsteemi ühekordse tekstigeneerimisega võrreldes sobivamaks iteratiivseks tõestuse otsimiseks.
Avatud kaaludega juurdepääs uurimistööks
Kontrollpunkti levitatakse avalikult, mitte ainult tasulise majutatud lõpp-punkti kaudu. Teadlased ja arendajad saavad avaldatud mudelimaterjale uurida ning luua oma kohaliku või eksperimentaalse järeldamise töövoo. Apache 2.0 litsents muudab väljalaske paljudeks kasutusviisideks paindlikumaks kui suletud ja teenusepakkuja kontrollitud API, kuid arvestada tuleb litsentsi ning kasutaja enda juurutamiskohustustega.
Avaldatud teoreemide tõestamise tulemused
StepFun teatab oma hoidlas MiniF2F-test võrdlusnäitaja hindamisel tulemuseks 66,0% näitajaga Pass@1. Pass@1 mõõdab, kas esimene valimisel saadud katse õnnestub kindlaksmääratud hindamismeetodi järgi. Seotud tehnilises aruandes esitatakse 7B-mudeli kohta teistsuguse hindamise korral tulemuseks 64,2%. Neid arve ei tohiks käsitleda otseselt võrreldavatena: hindamise ülesehitus, valimistingimused või tulemuste esitamise metoodika võivad erineda. Need on teenusepakkuja või uurimisaruande tulemused, mitte sõltumatu toimetuslik hinnang.
Tehnilised näitajad ja piirangud
| Tehniline näitaja | Dokumenteeritud teave |
|---|---|
| Teenusepakkuja | StepFun |
| Mudelite perekond | StepFun-Prover Preview |
| Ligikaudne suurus | Ligikaudu 8 miljardit parameetrit |
| Mudeli vorming | BF16 |
| Baasmudel | DeepSeek-R1-Distill-Qwen-7B |
| Peamine väljund | Tekst, eelkõige Lean 4 tõestuskood |
| Formaalse arutluse keskkond | Lean 4 |
| Avaldatud konteksti näitaja | 20 480 tokenit StepFuni hindamise seadistuses |
| Avaldatud genereerimisnäide | 16 384 maksimaalset väljundtokenit vLLM-i näites |
| Litsents | Apache License 2.0 |
20 480 tokeni suurusesse konteksti tuleb suhtuda ettevaatlikult. Kaasasolevas uurimuses seostatakse seda StepFuni hindamise seadistusega, mitte eraldi dokumenteeritud majutatud API piiranguga. Samuti pärineb väärtus 16 384 avaldatud vLLM-i näitest ning seda ei tohiks automaatselt käsitleda iga järeldusmootori või juurutuskonfiguratsiooni universaalse maksimumina. Praktilisi piiranguid võivad mõjutada saadaolev mälu, järeldamistarkvara, viiba pikkus ja genereerimise seaded.
Modaalsused ja toetatud võimekused
StepFun-Prover-Preview-7B on ainult tekstimudel. See võtab vastu tekstisisendit ja väljastab teksti; puuduvad kaasasolevad tõendid pildi-, heli-, video-, kõne-, muusika- või muu otsese mittetekstilise sisendi või väljundi kohta. Seetõttu ei ole see mõeldud multimodaalsete rakenduste jaoks.
Selle arutlusvõime on üldise asemel spetsialiseeritud. Mudeli keskne ülesanne on formaalsete tõestuste genereerimine ja täpsustamine, eriti Lean 4-s. See võib olla kasulik matemaatiliseks arutluseks juhul, kui probleem on võimalik väljendada toetatud formaalses keskkonnas, kuid uurimus ei tõesta, et see oleks parim valik üldise vestluse, piiranguteta matemaatika, faktiküsimustele vastamise või pika vormi kirjutamise jaoks.
Mudel suudab koodi genereerida konkreetses tähenduses, sest Lean 4 tõestused on programmid või formaalne kood. Kaasasolev teave ei toeta selle kirjeldamist üldise tarkvaratehnika mudeli või laia programmeerimiskeelte toega mudelina. Samamoodi on selle dokumenteeritud tööriistasuhtlus Lean 4 kontrollimine, mitte üldine tööriistaregister ega standardne funktsioonikutsumise API.
Kiiruse, kulu ja juurutamise kompromissid
Mudeli avatud kaaludega vorming võib vältida tokenipõhiseid majutatud API tasusid, kuid see ei muuda järeldamist tasuta. Kasutaja peab tagama ühilduva arvutusvõimsuse, salvestusruumi, järeldamise tarkvarapinu ja Lean 4 keskkonna. Uurimuses ei ole tuvastatud selle mudeli ametlikku tokenipõhist hinnastust ega esimese osapoole majutatud kommerts-API lõpp-punkti.
Iteratiivne tõestuse töövoog võib olla ka aeglasem kui ühekordne teksti genereerimine. Üks teoreem võib nõuda mitut mudeli genereerimis- ja Lean 4 kontrollimisvooru. See lisatöö loob olulise eelise — masinaga kontrollitava tagasiside —, kuid suurendab üldise keelemudeli mitteametliku tõestusselgituse küsimisega võrreldes latentsust ja töökorralduslikku keerukust.
Kulutundlikuks katsetamiseks võib kohalik avatud kaaludega kontrollpunkt olla atraktiivne, kui kasutajal on juba sobiv taristu. Kasutajatele, kes vajavad prognoositavat latentsust, hallatud skaleerimist, teenusetaseme tuge või tavapärast API-t, sobib see mudel halvemini, sest kaasasolevas uurimuses ei tuvastatud selliseid pakkumisi.
Parimad kasutusjuhud
- Lean 4 tõestuse visandite genereerimine formaalse matemaatika jaoks.
- Tõestuskatsete iteratiivne parandamine kompilaatori või verifikaatori tagasiside abil.
- Uurimistöö keelemudelite kohta, mis suhtlevad väliste verifikaatoritega.
- Katsed teoreemide tõestamise otsingu, tõestuste täpsustamise ja tööriistadega integreeritud arutlusega.
- Avatud kaaludega mudelite võrdlusuuringud formaalse matemaatika ülesannetes, näiteks MiniF2F-i laadsetes hindamistes.
Praktiline kasutaja peaks arvestama teoreemiväidete, Lean 4 süntaksi, asjakohase keskkonna ja mudeli järeldamiskoodiga. Mudel on kõige kasulikum siis, kui edu määrab see, kas Lean 4 võtab saadud tõestuse vastu, mitte see, kas selgitus tundub inimlugejale matemaatiliselt veenev.
Millal see mudel valida
Vali StepFun-Prover-Preview-7B siis, kui vajad spetsiaalselt avatud kaaludega mudelit Lean 4 teoreemide tõestamiseks ning oled valmis verifikaatoriahela ise käivitama või integreerima. See sobib eriti hästi uurimistööks ja prototüüpimiseks, kus mudeli kaaludele juurdepääs, reprodutseeritavus ja katsetamine on olulisemad kui majutatud teenuse mugavus.
Vali teist tüüpi mudel siis, kui vajad üldotstarbelist assistenti, multimodaalset sisendit või väljundit, pildi- või heligeneerimist, hallatud kommertslikku lõpp-punkti või standardset funktsioonikutsumise tuge. Tavaliseks rakenduste arenduseks võib paremini sobida üldine kodeerimismudel, samas kui majutatud arutlusteenus võib olla eelistatum juhul, kui taristu ja latentsus on kohalikust juhtimisest olulisemad. Kaasasolevas uurimuses ei tuvastatud konkreetset sõsarmudelit, mida saaks samadel alustel otse võrrelda, seega tuleks alternatiive hinnata nende tegeliku Lean 4 toe, mitte üldise mudelibrändi järgi.
Piirangud, mida arvestada
Mudel on spetsialiseeritud ning eeldada ei tohiks laialdast tootmiskeskkonna tuge. „Preview“ ehk eelvaate olek, tuvastatud ametliku API-hinnastuse puudumine ja sõltuvus kohalikust Lean 4 töövoost muudavad juurutamise vähem valmislahenduseks kui tavapärase majutatud keelemudeli kasutamise. Ka võrdlusuuringute tulemused on seotud vastavate hindamisseadetega ning neid ei tohiks tõlgendada garantiina, et iga teoreem lahendatakse esimesel katsel.
Lõpuks ei täpsusta kaasasolevad allikad teadmiste lõppkuupäeva, täiendtreeningu teenust, vahemäluteenust, pakett-API-t ega eraldi struktureeritud väljundi režiimi. Seetõttu tuleb neid funktsioone käsitleda dokumenteerimata, mitte kättesaadavatena. Mudeli dokumenteeritud väärtus seisneb avatud kaaludega ja verifikaatoriga juhitud Lean 4 tõestuste genereerimises, mitte üldiste API-funktsioonide laias valikus.