Mistral avaldas Leanstrali, AI mudeli vibe-koodimiseks koos formaalse valideerimisega

Mistral AI esitles suurt keeltemudelit Devstral, mis on suunatud rakenduste arendamisele (vibe-kodeerimine) ja optimeeritud koodi formaalseks valideerimiseks. Arvatakse, et Devstral võib olla abiks AI-assistendi loomiseks, mis mitte ainult ei genereeri koodi, vaid tagab ka, et selles pole vigu.

Devstral on esimene avatud mudel, mis toetab programmeerimiskeelt Lean 4 ja selle matemaatiliste tõendusmaterjalide kontrollimise tööriistade komplekti. Lean 4 pakub võimalusi koodi õigsuse ja spetsiifikale vastavuse matemaatiliseks tõendamiseks, mis võimaldab vibe-kodeerimise kontekstis kinnitada, et AI-mudeliga genereeritud kood teeb just seda, mida on plaanitud.

Mudeli mahus on 119 miljardit parameetrit (6.5 miljardit aktiveeritavat parameetrit tokeni kohta), see arvestab 256 tuhande tokeniga konteksti ja on avaldatud Apache 2.0 litsentsi all. Laaditav arhiiv Leanstraliga on 121 GB ja sobib kohalikele süsteemidele kasutamiseks. Kohalikuks käivitamiseks võivad kasutada raamatukogusid vllm, transformers ja SGLang.

Muuhulgas võib mudelit kasutada vibe-arendamiseks avatud agendis mistral-vibe ja integreerida tööriistakomplekti Aeneas koodi valideerimiseks Rusti keeles. Sisendparameetritena vastu võetakse tekst ja pildid, väljundina antakse vaid tekst. Toetatakse piltide sisu analüüsi.

AI-mudelite võimaluste hindamiseks, arvestades koodi formaalse valideerimise kvaliteeti ja matemaatiliste tõendusmaterjalide koostamist, on välja töötatud uus testikomplekt FLTEval. Testide käigus ületas mudel Leanstral märgatavalt olemasolevad avatud mudelid Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B ja GLM5 744B-A40B, näidates sarnaseid tulemusi Anthropicult pärit mudelite Claude Haiku 4.5 ja Claude Sonnet 4.6ga, kuid jäi maha mudelist Claude Opus 4.6. Eelkõige saavutas mudel Opus 39.6 punkti, samas kui Leanstral saavutas 21.9 ühe läbimise korral ja 31.9 16 läbimisega. Opuse kasutamise kulud olid 1650 dollarit, Leanstrali puhul aga 18 dollarit ühe läbimise ja 290 dollarit 16 läbimise korral. Haiku mudel saavutas 23 punkti kuludega 184 dollarit, samas kui Sonnet mudel sai 23.7 punkti kuludega 549 dollarit.

Allikas: opennet.ru