Compania Mistral AI a lansat un model lingvistic mare numit Devstral, destinat utilizării în dezvoltarea aplicațiilor (vibe-coding) și optimizat pentru verificarea formală a codului. Se presupune că Devstral poate fi utilizat pentru a crea asistenți AI capabili nu doar să genereze cod, ci și să garanteze absența erorilor în acesta.
Devstral a devenit primul model deschis care suportă limbajul de programare Lean 4 și instrumentele asociate pentru verificarea dovezilor matematice. Lean 4 oferă posibilități pentru demonstrarea matematică a corectitudinii codului și a conformității sale cu specificațiile, ceea ce, în contextul vibe-coding, permite confirmarea faptului că codul generat de modelul AI face exact ceea ce este dorit.
Modelul cuprinde 119 miliarde de parametri (6.5 miliarde de parametri activabili pe token), ia în considerare un context de 256.000 de tokeni și este publicat sub licența Apache 2.0. Arhiva descărcabilă cu Leanstral ocupă 121 GB și este potrivită pentru utilizare pe sisteme locale. Pentru lansare locală pot fi utilizate biblioteci precum vllm, transformers și SGLang.
Printre altele, modelul poate fi utilizat pentru dezvoltarea vibe în agentul deschis mistral-vibe, precum și integrat cu instrumentele Aeneas pentru verificarea codului în limbajul Rust. Ca parametri de intrare se acceptă text și imagini, în timp ce rezultatul se furnizează doar sub formă de text. Este suportată analiza conținutului imaginilor.
Pentru a evalua capacitățile modelelor AI, având în vedere calitatea realizării verificării formale a codului și redactarea dovezilor matematice, a fost dezvoltat un nou set de teste numit FLTEval. În testele efectuate, modelul Leanstral a depășit semnificativ modele deschise existente, precum Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B și GLM5 744B-A40B, a avut rezultate similare cu modelele Claude Haiku 4.5 și Claude Sonnet 4.6 de la compania Anthropic, dar a fost inferior modelului Claude Opus 4.6. În particular, modelul Opus a obținut 39.6 puncte, în timp ce Leanstral a obținut 21.9 în urma unei treceri și 31.9 după 16 treceri. Costurile de utilizare pentru Opus au fost de 1650 de dolari, comparativ cu Leanstral, care a costat 18 dolari pentru o trecere și 290 de dolari pentru 16 treceri. Modelul Haiku a obținut 23 puncte la costuri de 184 dolari, iar modelul Sonnet a adunat 23.7 puncte la costuri de 549 dolari.
Sursa: opennet.ro
