Kompania Mistral AI ka paraqitur një model të madh gjuhësor, Devstral, i fokusuar në përdorimin për zhvillimin e aplikacioneve (vibe-coding) dhe i optimizuar për verifikimin formal të kodit. Supozohet se Devstral mund të përdoret për krijimin e asistenteve AI që jo vetëm gjenerojnë kod, por gjithashtu garantojnë që ai nuk ka gabime.
Devstral është bërë modeli i parë i hapur që mbështet gjuhën e programimit Lean 4 dhe mjetet e saj të lidhura për verifikimin e provave matematikore. Lean 4 ofron mundësi për provimin matematikor të saktësisë së kodit dhe përputhshmërisë me specifikimet, që në kontekstin e vibe-coding e lejon të konfirmohet që kodi i gjeneruar nga modeli AI bën saktësisht atë që është menduar.
Modeli përfshin 119 miliard parametra (6.5 miliard parametra aktivizues për token), merr parasysh kontekstin në 256 mijë tokens dhe është publikuar me licencën Apache 2.0. Arkivi i ngarkueshëm me Leanstral zë 121 GB dhe është i përshtatshëm për përdorim në sisteme lokale. Për ekzekutimin lokal mund të përdoren bibliotekat vllm, transformers dhe SGLang.
Ndër të tjera, modeli mund të përdoret për zhvillimin vibe në agjentin e hapur mistral-vibe, si dhe të integrohet me mjetet Aeneas për verifikimin e kodit në gjuhën Rust. Si parametra hyrës pranohet teks dhe imazhe, ndërsa në dalje jepet vetëm tekst. Mbështetet analiza e përmbajtjes së imazheve.
Për të vlerësuar mundësitë e modeleve AI me llogari të cilësisë së realizimit të verifikimit formal të kodit dhe shkruarjes së provave matematikore, është zhvilluar një grup i ri testesh FLTEval. Në testet e kryera, modeli Leanstral ndjeshëm kaloi modelet ekzistuese të hapura Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B dhe GLM5 744B-A40B, duke treguar rezultate të ngjashme me modelet Claude Haiku 4.5 dhe Claude Sonnet 4.6 nga kompania Anthropic, por mbeti mbrapa modelit Claude Opus 4.6. Konkretisht, modeli Opus arriti 39.6 pikë, ndërsa Leanstral 21.9 me një kalim dhe 31.9 me 16 kalime. Megjithatë, shpenzimet për përdorimin e Opus ishin 1650 dollarë, ndërsa Leanstral ishte $18 për një kalim dhe $290 për 16 kalime. Modeli Haiku arriti 23 pikë me shpenzime $184, ndërsa modeli Sonnet 23.7 me shpenzime $549.
Burimi: opennet.ru
