Mis on StepFun-Prover-Preview-32B?
StepFun-Prover-Preview-32B on StepFuni avatud kaaludega keelemudel, mille peamine eesmärk on formaalne teoreemide tõestamine. Üldise vestluse, piltide mõistmise või laiapõhjalise tarkvaratoe asemel on see optimeeritud Lean 4 tõestuste genereerimiseks. Lean 4 on tõestusassistent, mis kontrollib, kas matemaatiline argument järgib formaalse süsteemi reegleid.
Tavapärases matemaatilises kirjutises võib pealtnäha usutav tõestus sisaldada märkamatut lünka. Lean 4 hindab tõestust selle asemel, et kontrollida, kas see on kehtiv, mistõttu sobib see mehhaaniliselt verifitseeritud matemaatika jaoks. StepFun-Prover-Preview-32B on üles ehitatud selle kontrollitsükli ümber: see pakub välja tõestuskoodi, saab Leanilt tagasisidet ja püüab puudulikku või kehtetut tulemust parandada.
Mudelit kirjeldatakse 32 miljardi parameetriga mudelina, samal ajal kui Hugging Face'i materjalides on toodud ligikaudu 33B parameetrit. Erinevus tuleneb sellest, kuidas mudelit eri avaldatud materjalides kirjeldatakse, mitte kahest eraldi versioonist. Mudelit levitatakse Apache 2.0 litsentsi alusel Hugging Face'is StepFuni organisatsiooni kaudu.
Kuidas tõestuste genereerimise töövoog toimib
Selle mudeli ja üldotstarbelise vestlusmudeli oluline erinevus seisneb selle kavandatud kasutuses koos tõestuskeskkonnaga. Tüüpiline töövoog algab Lean 4 keeles väljendatud matemaatilisest väitest. Mudel genereerib osalise tõestuse või tõestuse kavandi, mida Lean seejärel hindab. Saadud tagasiside võib tuvastada süntaksivead, ebaõnnestunud taktikad, lahendamata eesmärgid või muud probleemid. Mudel kasutab seda teavet uue katse koostamiseks.
Avaldatud kasutusviis kasutab tõestuskavandite ja Lean REPL-i tagasiside jaoks erimärgiseid. See annab mudelile struktureeritud teavet kontrollimise käigus toimunu kohta, selle asemel et paluda tal hinnata oma vastust ainult teksti põhjal. Praktikas tuleks mudelit mõista kui üht osa genereerimise, kontrollimise ja parandamise töövoost.
See lähenemine on eriti asjakohane tõestuste parandamisel. Kui tõestus on peaaegu valmis, kuid ebaõnnestub allesjäänud eesmärgi või rakendamatu taktika tõttu, annab Leani tagasiside järgmise genereerimissammu jaoks konkreetse sihi. Edu sõltub endiselt teoreemi väite kvaliteedist, kasutatavast Leani keskkonnast, imporditud teekidest, viipamise vormingust ja järeldamise seadistusest.
Võrdlustestide tulemused ja nende tähendus
StepFun teatab miniF2F-test-võrdlustestis tulemuseks 70,0% Pass@1. Hindamisel kasutati suhtlust Lean 4 REPL-iga ja iga ülesande kohta mitut vastust, et hinnata näitajat Pass@1. Seega kajastab esitatud tulemus tööriistatoega teoreemide tõestamise seadistust, mitte lihtsalt üht piiranguteta tekstilõpetust küsimuse kohta.
StepFun teatab ka selgest seosest genereerimise maksimaalse pikkuse ja testitud seadistuses mõõdetud jõudluse vahel. Tulemus kasvas 58,3%-lt 4096 märgi suuruse maksimaalse genereerimispikkuse korral 70,0%-ni 20 480 märgi korral. Pikem genereerimine annab mudelile rohkem ruumi tõestuse uurimiseks, ebaõnnestunud katsetest taastumiseks või pika formaalse argumendi lõpetamiseks, kuid võib suurendada ka latentsust ja ressursikulu.
Tegemist on teenusepakkuja esitatud võrdlustesti tulemustega, mitte garantiiga iga teoreemi või juurutuse kohta. Tulemused võivad erineda, kui muutuvad Leani versioon, teegid, viipamise vorming, valimi võtmise seaded, riistvara või kontrollitsükkel.
Tehnilised andmed ja modaalsused
| Spetsifikatsioon | Esitatud üksikasjad |
|---|---|
| Teenusepakkuja | StepFun |
| Mudeli suurus | 32B mudeli nimes; Hugging Face'i teabe kohaselt ligikaudu 33B |
| Mudeli tüüp | Järeldamisele suunatud põhjuslik keelemudel |
| Konteksti pikkus | 20 000 märki avaldatud hindamisseadistuses |
| Testitud genereerimise maksimaalne pikkus | 20 480 märki |
| Sisend | Tekst, sealhulgas Leani väited, tõestuse kontekst ja keskkonna tagasiside |
| Väljund | Tekst, peamiselt Leani tõestuskood ja sellega seotud arutluskäik |
| Litsents | Apache 2.0 |
| Kättesaadavus | Avatud kaalud Hugging Face'i kaudu |
20 000 märgi suurune kontekst viitab avaldatud hindamise kontekstiaknale, samal ajal kui 20 480 märki on testitud genereerimise maksimaalne pikkus. Neid arve ei tohiks käsitleda tõendina, et iga juurutus pakub identset mälu või teeninduspiiranguid. Praktiliseks paigalduseks on vaja ka piisavat riistvara ja seadistust sellise suurusega mudeli käitamiseks, kuid esitatud allikad ei määra üht kindlat minimaalset riistvaranõuet.
Mudelil on ainult tekstisisend ja tekstiväljund. Dokumenteeritud loomulikku pildi-, heli- ega videosisendit või -väljundit see ei paku. Selle tööriistadega seotud käitumine on spetsialiseeritud: mudel on mõeldud töötama Lean 4 REPL-iga, kuid seda ei tohiks segi ajada üldise majutatud funktsioonikutsete või veebiotsingu API-ga.
Hinnastamine ja juurutamine
Selle mudeli ametlikku StepFuni majutatud tokenipõhist hinda ei ole kontrollitud. Kuna kaalud on allalaaditavad, põhineb peamine kulumudel isehostimisel: kasutaja tagab arvutusvõimsuse, salvestusruumi, teenindustarkvara ja operatiivse hoolduse. See võib olla atraktiivne uurimisrühmadele, kes vajavad kontrolli tõestuskeskkonna üle või soovivad vältida formaalsete ülesannete saatmist kolmanda osapoole teenusele, kuid see ei tähenda, et järeldamine oleks tasuta.
Ametlikud näited näitavad juurutamist Transformersiga, vLLM-i ja SGLangiga. Need võimalused toetavad erinevaid teenindus- ja integratsioonimustreid, kuid mudel jääb isehostitavaks artefaktiks, mitte dokumenteeritud StepFuni hallatavaks järeldamise lõpp-punktiks. Enne teenindusvirna valimist peaksid kasutajad kontrollima hoidla ajakohaseid juhiseid ja ühilduvusnõudeid.
Apache 2.0 litsents lubab litsentsitingimustel laialdast kasutust. See ei vabasta vajadusest üle vaadata mudeli hoidla, sõltuvused, taristukulud ning konkreetses projektis kasutatavate matemaatiliste andmekogumite või ümbritseva tarkvaraga seotud kohustused.
Tugevused ja piirangud
Peamised tugevused
- Spetsialiseeritus: Mudel keskendub Lean 4 teoreemide tõestamisele, mitte üldotstarbelisele vestlusele, mistõttu sobib selle käitumine otsesemalt formaalse matemaatikaga.
- Kontrolliteadlik töövoog: Mudel on loodud Lean REPL-i tagasiside kaasamiseks ja tõestuskatsete muutmiseks, mitte pärast kontrollimata vastust peatumiseks.
- Juurdepääs avatud kaaludele: Teadlased ja arendajad saavad seda avaldatud juurutusnäidete abil lokaalselt või oma taristus käitada.
- Suur tõestuste genereerimise eelarve: Esitatud 20 480 märgi suurune maksimaalne genereerimisseadistus annab ruumi mitmesammulisele tõestuse otsingule, arvestades riistvara ja teeninduse piiranguid.
- Korratav formaalne siht: Leani kontrollija pakub genereeritud tõestuskoodi kehtivuse hindamiseks konkreetset testi.
Peamised piirangud
- Piiratud valdkond: Mudel on eelkõige kasulik formaalseks teoreemide tõestamiseks ning ei tohiks eeldada, et see on igapäevases kirjutamises, laiapõhjalistes teadmisteülesannetes või rakenduste abistamisel samal tasemel kui üldised juhiste järgimise mudelid.
- Hallatava API hinnastust ega liidest ei ole kontrollitud: Kasutajad, kes soovivad lihtsat kasutuspõhist lõpp-punkti, peavad valima mõne muu võimaluse või mudelit ise käitama.
- Arvutusvõimsus ja latentsus: Ligikaudu 32B–33B parameetri suurusklassi kuuluvat mudelit on väiksemate mudelitega võrreldes nõudlikum teenindada. Esitatud kiirusehinnang on toimetuslik, mitte teenusepakkuja avaldatud latentsusgarantii.
- Sõltuvus keskkonnast: Tõestuste edukas genereerimine sõltub Leani versioonidest, imporditud elementidest, teekidest, viipadest ja täpsest tagasisideahelast. Ühes keskkonnas töötav tõestus võib teises vajada kohandamist.
- Dokumenteeritud multimodaalset ega üldist tööriistaliidest ei ole: Leani integratsioon ei tõenda piltide mõistmist, kõnevõimekust, veebiotsingut, loomulikku JSON-režiimi ega üldist funktsioonikutset.
Järeldamise, kodeerimise, kiiruse ja kulude kompromissid
StepFun-Prover-Preview-32B järeldamisvõimet on kõige mõistlikum hinnata formaalsete tõestuste lõpetamise, mitte tavaliste vestlusvõrdlustestide põhjal. Selle keskne võime seisneb matemaatilise otsingu ja välise kontrolli ühendamises. Mudel võib kulutada palju genereerimissamme tõestuse eri teede uurimiseks ning kasutada seejärel Leani vastust parandamise suunamiseks. Seetõttu sobib see hästi tõestuste sünteesiks ja formaliseerimise töövoogudesse, kus korrektsust kontrollitakse mehhaaniliselt.
See suudab genereerida ka koodi, kuid selle kodeerimisroll on spetsialiseeritud. Leani tõestusskriptid on formaalses keskkonnas tõlgendatavad programmid, mistõttu koondub mudeli kodeerimisväärtus teoreemiväidetele, taktikatele, lemmadele ja tõestuste parandamisele. Seda ei tohiks automaatselt valida peamiseks mudeliks üldiseks rakenduste arenduseks, koodibaasi hoolduseks või multimodaalseks programmeerimisabiks.
Võimekuse ja kiiruse vahel on otsene kompromiss. Suur mudel koos pika genereerimislimiidiga saab uurida rohkem tõestusteid, kuid isehostitud järeldamine võib olla aeglasem ja kulukam kui väiksema mudeli või hallatava üldotstarbelise teenuse kasutamine. Esitatud toimetuslik hinnang annab järeldamisele hindeks 9, kodeerimisele 7, kiirusele 4 ja kulule 9; need on subjektiivsed kataloogiskoorid, mitte teenusepakkuja avaldatud võrdlustestide mõõtmised. Need võtavad kokku mudeli kavandatud väärtuse järeldamisülesannetes ja avatud kaalude pakutava kulukontrolli, tunnistades samal ajal selle tõenäolist teeninduskoormust.
Millal seda mudelit valida
Vali StepFun-Prover-Preview-32B siis, kui keskne ülesanne on Lean 4 tõestuste genereerimine, lõpetamine või parandamine ning sul on võimalik kasutada lokaalset või isehostitud järeldamisseadistust. See sobib eriti hästi järgmisteks kasutusjuhtudeks:
- automatiseeritud või poolautomatiseeritud teoreemide tõestamise uurimine;
- Lean 4 kasutavad formaliseerimisprojektid;
- kompilaatori või REPL-i tagasisidest lähtuv tõestuste parandamine;
- katsed, mis vajavad avatud kaale ja kontrolli verifitseerimiskeskkonna üle; ning
- matemaatiliste tõestuskandidaatide pakktöötlus, kus masinkontroll on töövoo osa.
Mõni teist tüüpi mudel võib olla sobivam, kui ülesanne nõuab kiiret interaktiivset vestlust, hallatavat API-t, värsket veebiteavet, pildi- või helitöötlust, laiapõhjalist tarkvaraarendust või dokumenteeritud loomulikku struktureeritud väljundi liidest. Väiksem mudel võib olla eelistatav ka siis, kui teeninduslatentsus ja riistvarakulu on tähtsamad kui ulatuslik tõestuse otsing. Üldotstarbeline mudel võib küll pakkuda kasulikke matemaatilisi ideid, kuid see ei asenda masinkontrollitud tõestuste puhul Leanile keskenduvat genereerimise, kontrollimise ja parandamise töövoogu.
Kokkuvõte
StepFun-Prover-Preview-32B on Lean 4 formaalse matemaatika jaoks mõeldud spetsialiseeritud avatud kaaludega mudel, mitte üldine tehisintellektiassistent. Selle kõige olulisem praktiline eripära on tõestuste genereerimise ja Leani kontrolli kavandatud tsükkel, mida toetavad esitatud 70,0% miniF2F-test Pass@1 tulemus ja pikk testitud genereerimispiir. Kompromiss seisneb käitamises: kasutajad peavad mudelit ise hostima ja tõestuskeskkonda haldama ning mudeli spetsialiseeritus piirab selle kasulikkust multimodaalsete, veebiühendusega või üldotstarbeliste töökoormuste puhul.