Mistral AI har præsenteret en stor sprogmodel, Devstral, som er designet til brug i applikationsudvikling (vibe coding) og optimeret til formel verifikation af kode. Det antages, at Devstral kan anvendes til at skabe AI-assistenter, som ikke bare genererer kode, men også garanterer fraværet af fejl i den.
Devstral blev den første åbne model, der understøtter programmeringssproget Lean 4 og det tilhørende værktøj til verifikation af matematiske beviser. Lean 4 giver muligheder for matematisk at bekræfte korrektheden af koden og dens overensstemmelse med specifikationen, hvilket i forbindelse med vibe coding muliggør bekræftelse af, at koden genereret af AI-modellen gør præcist det, den er tiltænkt.
Modellen dækker 119 milliarder parametre (6,5 milliarder aktiverede parametre pr. token), tager højde for en kontekst på 256.000 tokens og er offentliggjort under Apache 2.0-licensen. Den downloadbare archive med Leanstral fylder 121 GB og er egnet til brug på lokale systemer. Biblioteker som vllm, transformers og SGLang kan anvendes til lokal kørsel.
Blandt andet kan modellen bruges til vibe-udvikling i den åbne agent mistral-vibe og integreres med værktøjet Aeneas til verifikation af kode på Rust-sproget. Den tager tekst og billeder som input og leverer kun tekst som output. Analyse af billedindhold understøttes.
For at vurdere AI-modellers evner med hensyn til kvaliteten af den formelle verifikation af kode og skrivning af matematiske beviser er der udviklet et nyt testset, FLTEval. I de udførte tests overgik Leanstral markant eksisterende åbne modeller som Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B og GLM5 744B-A40B, og viste lignende resultater som modellerne Claude Haiku 4.5 og Claude Sonnet 4.6 fra Anthropic, men var bagefter modellen Claude Opus 4.6. Specifikt fik modellen Opus 39,6 point, mens Leanstral fik 21,9 ved én gennemgang og 31,9 ved 16 gennemgange. Omkostningerne ved at bruge Opus var 1.650 dollars, mens Leanstral kostede 18 dollars ved én gennemgang og 290 dollars ved 16 gennemgange. Modellen Haiku opnåede 23 point ved omkostninger på 184 dollars, mens modellen Sonnet fik 23,7 point ved omkostninger på 549 dollars.
Kilde: opennet.ru
