Mistral AI har lanserat en stor sprÄkmodell, Devstral, som Àr inriktad pÄ anvÀndning för apputveckling (vibe-coding) och Àr optimerad för formell verifiering av kod. Det förvÀntas att Devstral kan anvÀndas för att skapa AI-assistenter som inte bara genererar kod, utan ocksÄ garanterar att den Àr fri frÄn fel.
Devstral Àr den första öppna modellen som stöder programmeringssprÄket Lean 4 och det tillhörande verktyget för verifiering av matematiska bevis. Lean 4 ger möjligheter för mathematiskt bevis av korrekthet av kod och dess överensstÀmmelse med specifikationen, vilket i kontexten av vibe-coding möjliggör att bekrÀfta att den genererade koden av AI-modellen gör det som avsetts.
Modellen omfattar 119 miljarder parametrar (6,5 miljarder aktiverade parametrar per token), tar hÀnsyn till kontexten med 256 000 tokens och har publicerats under Apache 2.0-licensen. Den nedladdningsbara arkiven för Leanstral Àr 121 GB och Àr lÀmplig för anvÀndning pÄ lokala system. För lokal körning kan biblioteken vllm, transformers och SGLang anvÀndas.
Bland annat kan modellen anvÀndas för vibe-utveckling i den öppna agenten mistral-vibe och integreras med verktyget Aeneas för verifiering av kod pÄ Rust-sprÄket. Som indata tas text och bilder, och endast text returneras som utdata. Analys av bildinnehÄllet stöds.
För att utvÀrdera AI-modellers kapabiliteter med avseende pÄ kvaliteten pÄ den formella verifieringen av kod och skrivandet av matematiska bevis har en ny uppsÀttning tester, FLTEval, utvecklats. I genomförda tester övertrÀffade modellen Leanstral betydligt befintliga öppna modeller som Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B och GLM5 744B-A40B, visade liknande resultat som modellerna Claude Haiku 4.5 och Claude Sonnet 4.6 frÄn Anthropic, men lÄg efter modellen Claude Opus 4.6. Specifikt fick modellen Opus 39,6 poÀng, medan Leanstral fick 21,9 vid ett genomförande och 31,9 vid 16 genomföranden. Kostnaderna för anvÀndning av Opus var 1650 dollar, medan Leanstral kostade $18 vid ett genomförande och $290 vid 16 genomföranden. Modellen Haiku fick 23 poÀng med en kostnad pÄ $184, medan modellen Sonnet fick 23,7 poÀng med en kostnad pÄ $549.
KĂ€lla: opennet.ru
