Společnost Mistral AI představila rozsáhlý jazykový model Devstral, určený pro vývoj aplikací (Vibe Coding) a optimalizovaný pro formální ověřování kódu. Očekává se, že Devstral bude použit k vytvoření asistentů umělé inteligence, kteří nejen generují kód, ale také zajistí jeho bezchybnost.
Devstral se stal prvním open source modelem, který podporuje programovací jazyk Lean 4 a s ním spojenou sadu nástrojů pro matematické ověřování důkazů. Lean 4 umožňuje matematicky prokázat správnost kódu a jeho shodu se specifikacemi, což v kontextu vibe kódování umožňuje potvrdit, že kód generovaný modelem umělé inteligence dělá přesně to, co má dělat.
Model pokrývá 119 miliard parametrů (6.5 miliardy aktivovaných parametrů na token), zohledňuje kontexty 256 000 tokenů a je publikován pod licencí Apache 2.0. Archiv ke stažení s Leanstralem má velikost 121 GB a je vhodný pro použití na lokálních systémech. Pro lokální spuštění lze použít knihovny vllm, transformers a SGLang.
Model lze mimo jiné použít pro vývoj vibrací v open-source agentu mistral-vibe a integrovat s nástrojovou sadou Aeneas pro ověřování kódu Rust. Jako vstupní parametry přijímá text a obrázky a jako výstup produkuje pouze text. Je podporována analýza obsahu obrázků.
Pro vyhodnocení schopností modelů umělé inteligence s ohledem na kvalitu formálního ověřování kódu a psaní matematických důkazů byla vyvinuta nová sada benchmarků FLTEval. V testech model Leanstral výrazně překonal stávající open-source modely Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B a GLM5 744B-A40B. Vykázal podobné výsledky jako Claude Haiku 4.5 a Claude Sonnet 4.6 od Anthropic, ale zaostával za modelem Claude Opus 4.6. Konkrétně model Opus dosáhl 39.6 bodů, zatímco Leanstral dosáhl 21.9 bodů v jednom průchodu a 31.9 bodů v 16 průchodech. Náklady na používání Opusu činily 1 650 dolarů, zatímco Leanstral stál 18 dolarů v jednom průchodu a 290 dolarů v 16 průchodech. Haiku získalo 23 bodů za 184 dolarů, zatímco Sonnet 23.7 bodů za 549 dolarů.
Zdroj: opennet.ru
