A Mistral AI bemutatott egy új nyelvi modellt, a Devstralt, amelyet alkalmazásfejlesztésre (vibe-kódolásra) szántak, és amelyet a kód formális verifikációjának optimalizálására fejlesztettek ki. Úgy vélik, hogy a Devstral használható AI-asszisztensek létrehozására, amelyek nemcsak kódot generálnak, hanem garantálják, hogy az hibamentes.
A Devstral lett az első nyílt modell, amely támogatja a Lean 4 programozási nyelvet és a matematikai bizonyítékok ellenőrzésére szolgáló eszközkészletet. A Lean 4 lehetőséget nyújt a kód helyességének matematikai bizonyítására és a specifikációval való összhangjának ellenőrzésére, ami a vibe-kódolás kontextusában lehetővé teszi a generált AI-modell kódjának megerősítését, hogy az pontosan azt végzi, amit szántak.
A modell 119 milliárd paramétert fed le (6,5 milliárd aktiválható paraméter tokenenként), figyelembe veszi a 256 ezer tokenes kontextust, és Apache 2.0 alatt került közzétételre. A Leanstral letölthető archívuma 121 GB méretű, és helyi rendszereken való használatra alkalmas. Helyi futtatáshoz a vllm, transformers és SGLang könyvtárak használhatók.
A modell többek között használható vibe-fejlesztésre a nyílt ügynökben, a mistral-vibe-ben, valamint integrálható az Aeneas eszközkészletével a Rust nyelvű kód verifikációjához. Bemeneti paraméterként szöveget és képeket fogad, a kimenet csak szöveg. Támogatja a képek tartalmának elemzését.
Az AI-modellek képességeinek értékelésére, figyelembe véve a kód formális verifikálásának és matematikai bizonyítékok írásának minőségét, új tesztsorozatot fejlesztettek ki, az FLTEval-t. A végzett tesztek során a Leanstral jelentősen megelőzte a létező nyílt modelleket, mint a Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B és a GLM5 744B-A40B, hasonló eredményeket mutatott a Claude Haiku 4.5 és Claude Sonnet 4.6 modellekkel, amelyeket az Anthropic készített, de elmaradt a Claude Opus 4.6 modelltől. Különösen az Opus 39,6 pontot szerzett, míg a Leanstral 21,9-et egy átmenet során és 31,9-et 16 átmenet során. Eközben az Opus használati költsége 1650 dollár volt, míg a Leanstral 18 dollár egy átmenet során és 290 dollár 16 átmenet során. A Haiku 23 pontot ért el 184 dolláros költséggel, míg a Sonnet 23,7 pontot 549 dolláros költséggel.
Forrás: opennet.ru
