Společnost Mistral AI představila velký jazykový model Devstral, který je zaměřen na použití při vývoji aplikací (vibe-coding) a je optimalizován pro formální verifikaci kódu. Předpokládá se, že Devstral může být použit k vytváření AI asistentů, kteří nejen generují kód, ale také zaručují, že neobsahuje chyby.
Devstral se stal prvním otevřeným modelem, který podporuje programovací jazyk Lean 4 a s ním související nástroje pro ověřování matematických důkazů. Lean 4 poskytuje možnosti pro matematické dokazování správnosti kódu a jeho souladu se specifikací, což v kontextu vibe-codingu umožňuje potvrdit, že generovaný kód AI modelem dělá přesně to, co bylo zamýšleno.
Model pokrývá 119 miliard parametrů (6,5 miliardy aktivovaných parametrů na token), bere v úvahu kontext v 256 tisících tokenech a je publikován pod licencí Apache 2.0. Stahovaný archiv s Leanstral zabírá 121 GB a je vhodný pro použití na lokálních systémech. Pro lokální spuštění mohou být použity knihovny vllm, transformers a SGLang.
Mezi jinými aplikacemi může být model použit pro vibe-vývoj v otevřeném agentu mistral-vibe, a také se integrováním s nástroji Aeneas pro verifikaci kódu v jazyce Rust. Jako vstupní parametry se přijímají texty a obrázky, výstupem je pouze text. Podporována je analýza obsahu obrázků.
Pro posouzení schopností AI modelů s ohledem na kvalitu provádění formální verifikace kódu a psaní matematických důkazů byl vyvinut nový soubor testů FLTEval. V provedených testech model Leanstral výrazně překonal existující otevřené modely Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B a GLM5 744B-A40B, a vykázal podobné výsledky s modely Claude Haiku 4.5 a Claude Sonnet 4.6 od společnosti Anthropic, ale zaostal za modelem Claude Opus 4.6. Model Opus získal 39,6 bodu, zatímco Leanstral 21,9 při jednom průchodu a 31,9 při 16 průchodech. Náklady na použití modelu Opus činily 1650 dolarů, zatímco Leanstral stál 18 dolarů při jednom průchodu a 290 dolarů při 16 průchodech. Model Haiku získal 23 bodů s náklady 184 dolarů, zatímco model Sonnet získal 23,7 bodu při nákladech 549 dolarů.
Zdroj: opennet.ru
