Mistral AI je objavio Leanstral 1.5, otvoreni model namenjen radu u Lean 4, sistemu za formalnu verifikaciju dokaza. Kompanija navodi da je model objavljen pod Apache-2.0 licencom, da ima 119 milijardi ukupnih i 6 milijardi aktivnih parametara, kao i da je dostupan besplatno preko Hugging Face-a i kao API endpoint.
Prema rezultatima koje je objavio Mistral, Leanstral 1.5 je na testu miniF2F dostigao 100 odsto uspeha na validacionom i testnom skupu, na PutnamBench rešio je 587 od 672 zadatka, dok je na testovima FATE-H i FATE-X ostvario rezultate od 87 odsto i 34 odsto. To su, prema tvrdnji kompanije, najbolji rezultati u tim kategorijama za njen model.
Kako je model treniran
Mistral navodi da je Leanstral 1.5 prošao kroz tri faze razvoja: mid-training, supervised fine-tuning i reinforcement learning pomoću CISPO metode. Mid-training je dodatno prethodno treniranje na velikom skupu podataka, supervised fine-tuning je naknadno prilagođavanje na označenim primerima, a reinforcement learning je učenje na osnovu povratne informacije o uspehu zadatka.
U članku se objašnjava da je model treniran u dva okruženja. U prvom, takozvanom multiturn režimu, model dobija iskaz teoreme, pokušava da napiše dokaz i zatim dobija povratnu informaciju Lean kompajlera. Ako dokaz ne prođe proveru, pokušaj se ponavlja. U drugom, code agent okruženju, model radi u fajl sistemu, menja kod, pokreće komande i koristi Lean alatke za proveru ciljeva i tipova u realnom vremenu.
Šta su pokazali rezultati
Na PutnamBench testu, koji sadrži 672 zadatka sa matematičkog takmičenja Putnam, Mistral tvrdi da je Leanstral 1.5 uz manje troškove nadmašio neke uporedne sisteme. Kompanija navodi da je model rešavao zadatke uz približan trošak od 4 dolara po problemu, dok je za Seed-Prover 1.5 u visokom režimu navela procenu od 300 dolara ili više po problemu. Ove vrednosti treba čitati kao tvrdnje proizvođača, jer nisu nezavisno proverene u tekstu.
Mistral takođe ističe da Leanstral 1.5 pokazuje snažno test-time scaling, odnosno poboljšanje performansi kada se modelu daje više vremena i tokena tokom rešavanja. Prema prikazanim podacima kompanije, broj rešenih zadataka na PutnamBench-u rastao je sa većim budžetom: od 44 rešenja na 50 hiljada tokena, do 587 rešenja na 4 miliona tokena.
Na dodatnom testu FLTEval, koji je Mistral sada otvorio kao open source, model je, prema navodima kompanije, podigao pass@1 sa 21,9 na 28,9, a pass@8 sa 31,9 na 43,2. Pass@1 označava uspeh u prvom pokušaju, dok pass@8 meri uspeh kroz osam pokušaja. Kompanija tvrdi i da je time nadmašen rezultat modela Opus 4.6 uz znatno niži trošak.
Primena u proveri koda
Iako je primarno treniran za matematiku, Leanstral 1.5 je, prema Mistralu, pokazao i dobre rezultate u proveri softverskog koda. U jednom slučaju model je dokazivao vremensku složenost AVL stabala, samobalansirajućih binarnih stabala pretrage. Kompanija navodi da je za to bilo potrebno višemilionsko računanje, uključujući više od 2,7 miliona tokena i 22 kompakcije konteksta.
U drugom primeru, Mistral kaže da je automatizovani sistem u kome Leanstral pomaže u proveri otkrio greške u 57 repozitorijuma otvorenog koda. Navodi se da je sistem identifikovao 47 prekršenih tvrdnji, od čega je 11 ukazivalo na stvarne bagove, a 5 nije bilo ranije prijavljeno na GitHub-u. Jedan od primera bio je problem u funkciji za znak pri zigzag dekodiranju u biblioteci datrs/varinteger, gde je prelivanje pri izrazu (value + 1) moglo da izazove pad programa ili pogrešan rezultat.
Šta je dostupno korisnicima
Mistral navodi da je Leanstral 1.5 dostupan besplatno preko Hugging Face-a i kao besplatan API endpoint pod nazivom leanstral-1-5. Kompanija preporučuje korišćenje kroz svoj alat Mistral Vibe, uz dodatne korake za podešavanje okruženja i opcioni Lean LSP MCP servis, koji pomaže radu sa Lean jezom i proverom dokaza.
Za istraživače i timove koji rade na formalnoj verifikaciji, ova objava je važna jer pokazuje da otvoreni modeli sve ozbiljnije ulaze u oblast dokazivanja teorema i provere koda. Za širu AI publiku u Srbiji i regionu, to je još jedan primer da se upotreba velikih jezičkih modela širi izvan generisanja teksta i kodiranja, ka specijalizovanim zadacima gde je tačnost proverljiva kroz formalna pravila.
