Tvrtka Mistral AI predstavila je veliki jezični model Devstral, usmjeren na korištenje u razvoju aplikacija (vibe coding) i optimiziran za formalnu verifikaciju koda. Pretpostavlja se da se Devstral može koristiti za stvaranje AI asistenta koji ne samo da generira kod, već i osigurava njegovu ispravnost.
Devstral je postao prvi otvoreni model koji podržava programski jezik Lean 4 i s njim povezani alat za provjeru matematičkih dokaza. Lean 4 omogućava matematičku verifikaciju ispravnosti koda i njegovog usklađivanja sa specifikacijom, što u kontekstu vibe codinga omogućava potvrdu da generirani AI modelom kod radi ono što je predviđeno.
Model obuhvaća 119 milijardi parametara (6.5 milijardi aktiviranih parametara po tokenu), uzima u obzir kontekst od 256 tisuća tokena i objavljen je pod Apache 2.0 licencom. Preuzimajući arhiva s Leanstral-om zauzima 121 GB i pogodan je za korištenje na lokalnim sustavima. Za lokalno pokretanje mogu se koristiti biblioteke vllm, transformers i SGLang.
Osim toga, model se može koristiti za vibe razvoj u otvorenom agentu mistral-vibe, a također se može integrirati s alatom Aeneas za verifikaciju koda na jeziku Rust. Kao ulazni parametri prihvaćaju se tekst i slike, dok se na izlazu isporučuje samo tekst. Podržana je analiza sadržaja slika.
Za procjenu mogućnosti AI modela uzimajući u obzir kvalitetu provođenja formalne verifikacije koda i pisanje matematičkih dokaza, razvijen je novi skup testova FLTEval. U provedenim testovima, model Leanstral značajno je nadmašio postojeće otvorene modele Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B i GLM5 744B-A40B, pokazao je slične rezultate s modelima Claude Haiku 4.5 i Claude Sonnet 4.6 tvrtke Anthropic, ali je zaostajao za modelom Claude Opus 4.6. Naime, model Opus je postigao 39.6 bodova, dok je Leanstral postigao 21.9 pri jednom prolazu i 31.9 pri 16 prolaza. Troškovi korištenja Opusa iznosili su 1650 dolara, dok su troškovi Leanstral-a iznosili 18 dolara pri jednom prolazu i 290 dolara pri 16 prolaza. Model Haiku postigao je 23 boda uz troškove od 184 dolara, dok je model Sonnet skupio 23.7 boda uz troškove od 549 dolara.
Izvor: opennet.ru
