Mistral AI-k Devstral izeneko hizkuntza-eredu handi bat aurkeztu du, aplikazioen garapenerako (bibrazio-kodeketa) diseinatua eta kodearen egiaztapen formalerako optimizatua. Devstral IA laguntzaileak sortzeko erabiltzea espero da, kodea sortu ez ezik, akatsik gabe dagoela ziurtatu ere egin dezaketenak.
Devstral Lean 4 programazio-lengoaia eta harekin lotutako froga matematikoen egiaztapen-tresna onartzen zituen lehen kode irekiko eredua izan zen. Lean 4-k kodearen zuzentasuna eta zehaztapenekin bat datorrela matematikoki frogatzeko gaitasuna ematen du, eta horrek, bibrazio-kodeketaren testuinguruan, IA eredu batek sortutako kodeak egin behar duena egiten duela baieztatzen du.
Modeloak 119 milioi parametro hartzen ditu barne (token bakoitzeko 6.5 milioi parametro aktibatu), 256 tokenen testuinguruak hartzen ditu kontuan eta Apache 2.0 lizentziapean argitaratzen da. Leanstral-ekin deskargatu daitekeen artxiboa 121 GB-koa da eta tokiko sistemetan erabiltzeko egokia da. vllm, transformers eta SGLang liburutegiak tokiko exekuziorako erabil daitezke.
Besteak beste, eredua mistral-vibe agente irekian bibrazioen garapenerako erabil daiteke eta Aeneas toolkit-arekin integra daiteke Rust kodea egiaztatzeko. Testua eta irudiak onartzen ditu sarrera-parametro gisa, eta testua bakarrik sortzen du irteera gisa. Irudien edukiaren analisia onartzen da.
IA ereduen gaitasunak ebaluatzeko, kode formalaren egiaztapenaren kalitatea eta froga matematikoen idazketa kontuan hartuta, FLTEval erreferentzia multzo berri bat garatu zen. Probetan, Leanstral ereduak nabarmen gainditu zituen Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B eta GLM5 744B-A40B kode irekiko ereduak. Anthropic-en Claude Haiku 4.5 eta Claude Sonnet 4.6-ren antzeko emaitzak erakutsi zituen, baina Claude Opus 4.6 ereduaren atzetik geratu zen. Zehazki, Opus ereduak 39.6 puntu lortu zituen, Leanstral-ek 21.9 puntu lortu zituen bitartean pase bakarrean eta 31.9 puntu 16 pasetan. Opus erabiltzearen kostua 1650 $ izan zen, Leanstral-ek 18 $ balio zuen bitartean pase bakarrean eta 290 $ 16 pasetan. Haikuak 23 puntu lortu zituen 184 dolarrekin, eta Sonnetak, berriz, 23.7, 549 dolarrekin.
Iturria: opennet.ru
