StepFun-Formalizer-7B

Mida StepFun-Formalizer-7B teeb

StepFun-Formalizer-7B on matemaatilise automaatse formaliseerimise keelemudel. Praktilises mõttes võtab see tavapärases matemaatilises keeles sõnastatud ülesande ja koostab sellest formaalse väite keeles Lean 4, mida kasutatakse definitsioonide, väidete ja tõestuste väljendamiseks masinaga kontrollitaval kujul.

Mudel on suunatud eelkõige formaliseerimise etapile, mitte Leani kontrollija asendamisele. See suudab tuvastada mitteametlikus ülesandes kirjeldatud matemaatilised objektid ja seosed ning pakkuda neile vastava teoreemiväite koos asjakohaste definitsioonide, imporditavate moodulite ja Mathlibi terminoloogiaga. Genereeritud tulemus jääb esialgu kandidaadiks, kuni see kompileeritakse ja kontrollitakse ühilduvas Leani keskkonnas.

See eristus on uute kasutajate jaoks oluline. Ladusalt näiv Leani vastus ei ole automaatselt korrektne formaliseering. Leani kontroll võib paljastada süntaksivead, puuduvad impordid, ebatäpsed teoreemiväited või erinevuse mitteametlikult mõeldud ülesande ja genereeritud väite vahel.

Koht StepFuni mudelivalikus

Mudel kuulub StepFun-Formalizeri perekonda ja on kaasasolevas uurimuses kirjeldatud väiksem nimeline variant. Uurimuses on nimetatud ka 32B suurusega sõsarmudelit, kuid selle lehe teema on StepFun-Formalizer-7B. Väiksem maht muudab selle palju suurema spetsialiseeritud kontrollpunktiga võrreldes praktilisemaks kandidaadiks kohalikuks või piiratud ressurssidega juurutuseks, samas kui suurem sõsarmudel võib olla sobivam siis, kui formaliseerimise maksimaalne kvaliteet on riistvara tõhususest olulisem.

Kanoonilises nimes kasutatakse tähist 7B, kuid Hugging Face'i loendis kirjeldatakse kontrollpunkti ligikaudu 8B parameetriga mudelina. Mudel põhineb mudelil DeepSeek-R1-Distill-Qwen-7B ja seda on peenhäälestatud formaliseerimiseks, mitte üldotstarbeliseks vestlusabiliseks. Seda levitatakse Hugging Face'i kaudu Apache 2.0 litsentsi alusel.

Kuidas mudelit kavatsetakse kasutada ja treenida

StepFuni kirjelduse kohaselt ühendab treeninguviis formaalteadmiste destilleerimise, mitteametlikust formaalseks teisendamise arutluse sünteesi, juhendatud peenhäälestuse ning kontrollimisele suunatud tagasisidega täiendõppe. Nende meetodite eesmärk on siduda tavakeelne matemaatiline arutlus formaalse teoreemitõestaja eeldatava sõnavara ja struktuuriga.

Mudelikaart sisaldab näiteid viipade kohta, milles mudelilt palutakse koostada esitatud Mathlibi päise põhjal Lean 4 väiteid. Praktiline töövoog seisneb seega matemaatilise ülesande esitamises, eeldatava Leani ja Mathlibi keskkonna määratlemises, formaalse väite küsimises ning väljundi seejärel Leanis testimises. Kui väide ei kompileeru või ei väljenda soovitud ülesannet, saab viipa muuta ja genereerida uue kandidaadi.

See töövoog muudab StepFun-Formalizer-7B kasulikuks formaliseerimisabiliseks. See ei tõesta, et mudel suudab iga kirjeldatud teoreemi iseseisvalt tõestada, ning kaasasolevas uurimuses ei nimetata seda täielikuks autonoomseks teoreemitõestussüsteemiks.

Võrdlustulemused ja peamised tugevused

Autorite hindamises saavutas StepFun-Formalizer-7B BEq@1 skoori 38,3% andmekogumis FormalMATH-Lite, 25,1% andmekogumis ProverBench ja 5,2% andmekogumis CombiBench. Kuni 16 genereeritud kandidaadi korral olid teatatud BEq@16 skoorid samades võrdlustes vastavalt 61,2%, 37,9% ja 11,0%.

BEq mõõdab, kas vähemalt üks genereeritud formaalne väide on hindamisprotseduuri kohaselt alusväitega definitsiooniliselt või semantiliselt samaväärne. Ühe näidise ja 16 näidise tulemuste erinevus näitab, kui kasulik võib olla mitme kandidaadi genereerimine juhul, kui juurutusvoog suudab neid järjestada või kontrollida. See näitab ka, miks hindamistulemusi ei tohiks tõlgendada garantiina, et esimene väljund on korrektne.

Võrdlusandmestikud hõlmavad muu hulgas algebra, arvuteooria, matemaatilise analüüsi ja kombinatoorika ülesandeid. Oma sihtvaldkonnas on mudeli peamised tugevused spetsialiseerumine Lean 4-le, võime teisendada mitteametlikku matemaatilist keelt formaalseteks väideteks ning suhteliselt tagasihoidlik avatud kaaludega mudeli suurus. Apache 2.0 litsents ja allalaaditav kontrollpunkt võimaldavad juurutajatel luua kohalikke töövooge, sõltumata teenusepakkuja hallatavast järeldusliidesest.

Tehnilised näitajad ja toetatud modaalsused

Mudel on oma loomulikus liideses ainult tekstipõhine. See ei genereeri algupäraselt pilte, heli ega videot ning puuduvad tõendid pildi-, heli- või videosisendi toetuse kohta. 16 384 tokeni pikkune kontekst on oluline siis, kui viibad sisaldavad pikki matemaatilisi kirjeldusi, definitsioone või Mathlibi päiseid, kuigi tegelik kasutatav pikkus sõltub ka valitud järeldussüsteemist ja viiba vormingust.

Kaasasolevas uurimuses ei ole täpset maksimaalset väljundtokenite piirmäära määratletud. Seetõttu ei tohiks kasutajad käsitleda konteksti pikkust avaldatud maksimaalse lõpetamispikkusena. 16 384 tokeni näitaja kirjeldab teatatud konteksti mahtu, mitte eraldi kontrollitud väljundi lubatud pikkust.

Hinnakujundus ja juurutuskulud

StepFun-Formalizer-7B ametlikku hostitud tokenihinda ei ole esitatud. Mudel on avatud kaaludega kontrollpunkt, seega põhineb juurdepääs mudeli allalaadimisel ja käitamisel, mitte dokumenteeritud korduva API-paketi ostmisel. Mudelikaart sisaldab juurutusnäiteid Transformersile ja vLLM-ile ning hoidla on seotud ka SGLangi tööriistadega.

See ei tähenda, et järeldamine oleks tasuta. Käitajad peavad tagama sobiva riistvara, salvestusruumi, elektri ja järeldustarkvara. Tegelik kulu ja kiirus sõltuvad juurutuse konfiguratsioonist, sealhulgas riistvarast ja genereerimisseadetest. Hallatava API-ga võrreldes võib kohalik juurutus pakkuda suuremat kontrolli ning prognoositavat kontrolli viipade ja väljundite üle, kuid see nõuab seadistamist ja operatiivset vastutust.

Väiksem mudelimaht on selle peamine kulueelis võrreldes märksa suuremate formaliseerimismudelitega. Väiksem kontrollpunkt võib siiski soovitud edukuse saavutamiseks vajada rohkem kandidaatide genereerimist, viipade korduvat kohandamist või välist kontrolli. Kontrollimise töövoos tuleb mitme kandidaadi genereerimise kulu arvestada koos Leani kontrollide käitamise kuluga.

Arutlus, programmeerimine ja tööriistade tugi

StepFun-Formalizer-7B-d on kõige otstarbekam käsitleda kitsale tehnilisele valdkonnale suunatud arutlusele keskenduva koodigeneratsiooni mudelina. Selle arutlusvõime väljendub matemaatiliste seoste tõlgendamises ja formaalsete väidete koostamises, samas kui koodiväljund keskendub konkreetselt Lean 4-le, mitte laiapõhjalisele tarkvaraarendusele.

Mudel ise genereerib teksti ja Leani koodi, kuid kaasasolev uurimus ei kinnita loomulikku funktsioonikutsete tuge, tööriistade kasutamist, veebotsingut ega teenusepakkuja hallatavat agendiliidest. Leani ja Mathlibi saab ümbritsevas töövoos kasutada väliste kontrollivahenditena, kuid see erineb sellest, kui mudelil oleks sisseehitatud tööriistakasutuse API. Samuti ei ole tuvastatud ametlikku JSON-režiimi, hostitud pakett-API-t ega hallatavat vahemällu salvestamise teenust.

Usaldusväärseks kasutamiseks võib rakendus paigutada mudeli Leani kompilaatori või kontrollija kõrvale: genereerida ühe või mitu väidet, saata need valideerimiseks, uurida vigu ning säilitada ainult väljundid, mis kompileeruvad ja vastavad soovitud teoreemile. See ümbritsev protsess on tehniline töövõtt, mitte kontrollpunkti väidetav sisseehitatud võimekus.

Piirangud ja millal seda mudelit valida

StepFun-Formalizer-7B on hea valik siis, kui peamine ülesanne on matemaatilise teksti teisendamine Lean 4-ks, eriti juhul, kui organisatsioon soovib avatud kaaludega mudelit, mida saab kohapeal käitada. See sobib eriti hästi formaalse matemaatika uurimiseks, teoreemiväidete genereerimiseks, õppekatseteks ja tõestusabi töövoogudesse, kus iga väljund kontrollitakse väliselt.

See võib olla üldotstarbelisest hostitud keelemudelist sobivam siis, kui Leanile omane sõnavara ja formaliseerimine on olulisemad kui laiapõhjaline vestlusvõime. Avatud litsents ja ise hallatav juurutus võivad olla samuti atraktiivsed juhul, kui andmed peavad jääma kohalikku taristusse või kui projekt ei soovi sõltuda tokenipõhisest API-hinnast.

Üldise veebiuuringu, ajakohase teabe hankimise, multimodaalse töö või rakenduste puhul, mis vajavad dokumenteeritud hostitud API-t koos tööriistakutsete, struktureeritud väljundite, pakettöötluse või avaldatud latentsus- ja hinnagarantiidega, võib sobivam olla mõni muu võimalus. Suuremat sõsarmudelit, näiteks StepFun-Formalizer 32B-d, tasub hinnata juhul, kui projekt suudab toetada suuremat ressursikulu ja seab esikohale mudeli mahu, ehkki kaasasolev uurimus ei anna otsest kõrvutustulemust, mis tõestaks selle paremust iga ülesande puhul.

Mudelit ei tohiks kasutada matemaatilise korrektsuse ainsa autoriteedina. Selle võrdlustulemused on spetsialiseeritud võimekuse kohta tähenduslikud tõendid, kuid need ei taga, et konkreetne genereeritud väide on korrektne. Leani kompileerimine ja semantiline ülevaatus on endiselt vajalikud, eriti kui formaliseeringut kasutatakse teadustöös, õppetöös või tootmistarkvaras.

Kokkuvõte

StepFun-Formalizer-7B on keskendunud avatud kaaludega mudel, mis teisendab loomulikus keeles esitatud matemaatika Lean 4 formaalseteks väideteks. Selle praktiliselt tugevaim kombinatsioon on spetsialiseerumine, kohapealne juurutatavus, Apache 2.0 litsents ja 16 384 tokeni pikkune kontekst. Kompromissid on sama selged: avaldatud hostitud hind või hallatav API puudub, kontrollitud loomulikku multimodaalset ega tööriistakasutuse liidest ei ole, maksimaalset väljundipikkust pole määratletud ning miski ei asenda Leanil põhinevat kontrolli. Kasutajatele, kes ehitavad formaliseerimise töövoogu, mitte üldotstarbelist vestlusrobotit, on need omadused põhjus seda sihtotstarbelist mudelit hinnata.