Das Unternehmen Mistral AI hat das große Sprachmodell Devstral vorgestellt, das für die Anwendungsentwicklung (Vibe-Coding) konzipiert und zur formalen Verifikation von Code optimiert ist. Devstral kann dazu verwendet werden, KI-gestützte Assistenten zu erstellen, die nicht nur Code generieren, sondern auch garantieren, dass dieser fehlerfrei ist.
Devstral ist das erste offene Modell, das die Programmiersprache Lean 4 und die damit verbundenen Werkzeuge zur Überprüfung mathematischer Beweise unterstützt. Lean 4 ermöglicht mathematische Beweise für die Korrektheit von Code und dessen Übereinstimmung mit der Spezifikation, was im Kontext des Vibe-Codings hilft, sicherzustellen, dass der von dem KI-Modell generierte Code genau das tut, was beabsichtigt war.
Das Modell umfasst 119 Milliarden Parameter (6,5 Milliarden aktivierbare Parameter pro Token), berücksichtigt den Kontext von 256.000 Tokens und wird unter der Apache 2.0 Lizenz veröffentlicht. Das herunterladbare Archiv mit Leanstral hat eine Größe von 121 GB und ist für die Verwendung auf lokalen Systemen geeignet. Für den lokalen Betrieb können die Bibliotheken vllm, transformers und SGLang verwendet werden.
Unter anderem kann das Modell für die Entwicklung von Vibes im offenen Agenten Mistral-Vibe verwendet werden und lässt sich auch mit dem Aeneas-Toolset zur Verifizierung von Code in der Programmiersprache Rust integrieren. Als Eingabeparameter werden Text und Bilder akzeptiert, während nur Text ausgegeben wird. Die Analyse von Bildinhalten wird unterstützt.
Für die Bewertung der Fähigkeiten von KI-Modellen unter Berücksichtigung der Qualität der formalen Verifizierung von Code und der Erstellung von mathematischen Beweisen wurde ein neuer Testsatz, FLTEval, entwickelt. In den durchgeführten Tests übertraf das Leanstral-Modell deutlich die bestehenden offenen Modelle Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B und GLM5 744B-A40B, erzielte ähnliche Ergebnisse wie die Modelle Claude Haiku 4.5 und Claude Sonnet 4.6 von Anthropic, jedoch schnitt es schlechter als das Modell Claude Opus 4.6 ab. Insbesondere erzielte das Opus-Modell 39,6 Punkte, während Leanstral 21,9 Punkte bei einem Durchgang und 31,9 Punkte bei 16 Durchgängen erzielt hat. Dabei lagen die Kosten für die Verwendung von Opus bei 1650 Dollar, während Leanstral 18 Dollar bei einem Durchgang und 290 Dollar bei 16 Durchgängen kostete. Das Haiku-Modell erzielte 23 Punkte bei Kosten von 184 Dollar, während das Sonnet-Modell 23,7 Punkte bei Kosten von 549 Dollar erreichte.
Quelle: opennet.ru
