Ettevõte Mistral AI tutvustas suurt keelemudelit Devstral, mis on mõeldud rakenduste (vibe-koodimise) arendamiseks ja optimeeritud koodi formaalseks verifikatsiooniks. Eeldatakse, et Devstral'i saab kasutada AI-assistentide loomiseks, mis mitte ainult ei genereeri koodi, vaid ka tagab selle veatuse.
Devstral on esimene avatud mudel, mis toetab programmikeelt Lean 4 ja sellega seotud tööriistu matemaatiliste tõendite kontrollimiseks. Lean 4 pakub võimalusi koodi korrektsuse tõendamiseks ja vastavuse kontrollimiseks spetsifikatsioonile, mis vibe-koodimise kontekstis võimaldab kinnitada, et AI mudeliga genereeritud kood teeb just seda, mis on ette nähtud.
Mudel katab 119 miljardit parameetrit (6,5 miljardit aktiveeritavat parameetrit tokeni kohta), arvestab konteksti 256 000 tokeni ulatuses ja on avaldatud litsentsi all Apache 2.0. Laaditav arhiiv Leanstraliga on 121 GB ja sobib kasutamiseks lokaalses süsteemis. Kohalikuks käivitamiseks võib kasutada raamatukogusid vllm, transformers ja SGLang.
Muuhulgas saab mudelit kasutada vibe-arendamiseks avatud agent Mistral-vibe, samuti saab seda integreerida Aenease tööriistakasti, et valideerida koodi Rusti keeles. Sisendparameetritena võetakse vastu tekst ja pildid, väljundiks antakse ainult tekst. Toetatakse piltide sisu analüüsi.
AI mudelite võimaluste hindamiseks, arvestades koodi formaalse kontrollimise kvaliteeti ja matemaatiliste tõendite kirjutamist, on loodud uus testide kogum FLTEval. Testide käigus ületas mudel Leanstral märgatavalt olemasolevaid avatud mudeleid Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B ja GLM5 744B-A40B, näidates sarnaseid tulemusi mudelitega Claude Haiku 4.5 ja Claude Sonnet 4.6 ettevõttelt Anthropic, kuid jäi alla mudelile Claude Opus 4.6. Eriti saavutas mudel Opus 39.6 punkti, samas kui Leanstral saavutas 21.9 punktiga ühe läbimise ja 31.9 punktiga 16 läbimise korral. Selle kasutamise kulud Opuse puhul olid 1650 dollarit, Leanstrali puhul aga $18 ühe läbimise ja $290 16 läbimise korral. Mudel Haiku saavutas 23 punkti, kulutades $184, mudel Sonnet aga 23.7 punkti, kulutades $549.
Allikas: opennet.ru
