Mistral a publicat Leanstral, un model de inteligență artificială pentru codarea vibrațiilor cu verificare formală.

Mistral AI a dezvăluit un model de limbaj extins, Devstral, conceput pentru dezvoltarea de aplicații (codare vibratoare) și optimizat pentru verificarea formală a codului. Se așteaptă ca Devstral să fie utilizat pentru a crea asistenți AI care nu numai că pot genera cod, ci și pot asigura că acesta este fără erori.

Devstral a devenit primul model open source care a suportat limbajul de programare Lean 4 și setul de instrumente asociat pentru verificarea matematică a dovezilor. Lean 4 oferă posibilitatea de a demonstra matematic corectitudinea codului și conformitatea acestuia cu specificațiile, ceea ce, în contextul codării vibratoare, permite confirmarea faptului că codul generat de un model de inteligență artificială face exact ceea ce este destinat să facă.

Modelul acoperă 119 miliarde de parametri (6.5 miliarde de parametri activați per token), ia în considerare contexte de 256 de token-uri și este publicat sub o licență Apache 2.0. Arhiva descărcabilă cu Leanstral are 121 GB și este potrivită pentru utilizarea pe sisteme locale. Bibliotecile vllm, transformers și SGLang pot fi utilizate pentru execuție locală.

Printre altele, modelul poate fi utilizat pentru dezvoltarea vibrațiilor în agentul open-source mistral-vibe și integrat cu setul de instrumente Aeneas pentru verificarea codului Rust. Acceptă text și imagini ca parametri de intrare și produce doar text ca ieșire. Este suportată analiza conținutului imaginilor.

Pentru a evalua capacitățile modelelor de inteligență artificială, ținând cont de calitatea verificării formale a codului și de scrierea demonstrațiilor matematice, a fost dezvoltată o nouă suită de benchmark-uri FLTEval. În teste, modelul Leanstral a depășit semnificativ modelele open-source existente Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B și GLM5 744B-A40B. Acesta a arătat rezultate similare cu cele ale modelelor Claude Haiku 4.5 și Claude Sonnet 4.6 de la Anthropic, dar a rămas în urma modelului Claude Opus 4.6. Mai exact, modelul Opus a obținut 39.6 puncte, în timp ce Leanstral a obținut 21.9 puncte într-o singură trecere și 31.9 puncte în 16 treceri. Costul utilizării Opus a fost de 1650 USD, în timp ce Leanstral a costat 18 USD într-o singură trecere și 290 USD în 16 treceri. Haiku a obținut 23 de puncte, la un preț de 184 de dolari, în timp ce Sonetul a obținut 23.7 puncte, la un preț de 549 de dolari.