Het bedrijf Mistral AI heeft een grote taalmodel Devstral gepresenteerd, gericht op het ontwikkelen van applicaties (vibe-coding) en geoptimaliseerd voor formele verificatie van code. Er wordt verondersteld dat Devstral kan worden gebruikt voor het creƫren van AI-assistenten die niet alleen code genereren, maar ook garanderen dat deze vrij is van fouten.
Devstral is het eerste open model dat de programmeertaal Lean 4 en de bijbehorende hulpmiddelen voor de validatie van wiskundige bewijzen ondersteunt. Lean 4 biedt mogelijkheden voor het wiskundig bewijzen van de correctheid van code en de overeenstemming met de specificatie, wat in de context van vibe-coding bevestigt dat de door het AI-model gegenereerde code precies doet wat bedoeld is.
Het model omvat 119 miljard parameters (6,5 miljard actieve parameters per token), houdt rekening met een context van 256.000 tokens en is gepubliceerd onder de Apache 2.0-licentie. Het te downloaden archief van Leanstral is 121 GB groot en geschikt voor gebruik op lokale systemen. Voor lokaal gebruik kunnen de bibliotheken vllm, transformers en SGLang worden gebruikt.
Onder andere kan het model worden gebruikt voor vibe-ontwikkeling in de open agent mistral-vibe, en ook worden geĆÆntegreerd met het Aeneas-hulpmiddel voor codeverificatie in Rust. De invoerparameters zijn tekst en afbeeldingen, en de output is alleen tekst. Analyse van de inhoud van afbeeldingen wordt ondersteund.
Er is een nieuwe testset FLTEval ontwikkeld om de mogelijkheden van AI-modellen te beoordelen, rekening houdend met de kwaliteit van formele codeverificatie en het schrijven van wiskundige bewijzen. In de uitgevoerde tests overtrof het model Leanstral aanzienlijk bestaande open modellen Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B en GLM5 744B-A40B, en vertoonde het soortgelijke resultaten met de modellen Claude Haiku 4.5 en Claude Sonnet 4.6 van het bedrijf Anthropic, maar bleef achter bij het model Claude Opus 4.6. In het bijzonder behaalde model Opus 39,6 punten, terwijl Leanstral 21,9 behaalde bij Ć©Ć©n poging en 31,9 bij 16 pogingen. De kosten voor het gebruik van Opus bedroegen $1650, terwijl Leanstral $18 bij Ć©Ć©n poging en $290 bij 16 pogingen kostte. Het model Haiku behaalde 23 punten bij kosten van $184, terwijl model Sonnet 23,7 punten behaalde bij kosten van $549.
Bron: opennet.ru
