Das Unternehmen Mistral AI hat das große Sprachmodell Devstral vorgestellt, das für die Entwicklung von Anwendungen (Vibe-Coding) konzipiert ist und für die formale Verifizierung von Code optimiert wurde. Es wird angenommen, dass Devstral zur Erstellung von KI-Assistenten verwendet werden kann, die nicht nur Code generieren, sondern auch die Fehlerfreiheit desselben garantieren.
Devstral ist das erste Open-Source-Modell, das die Programmiersprache Lean 4 und das damit verbundene Werkzeug zur Überprüfung mathematischer Beweise unterstützt. Lean 4 bietet Möglichkeiten zum mathematischen Beweis der Korrektheit von Code und seiner Übereinstimmung mit der Spezifikation, was im Kontext des Vibe-Codings bestätigt, dass der von der KI generierte Code das tut, was beabsichtigt war.
Das Modell umfasst 119 Milliarden Parameter (6,5 Milliarden aktivierte Parameter pro Token), berücksichtigt einen Kontext von 256.000 Tokens und wurde unter der Lizenz Apache 2.0 veröffentlicht. Das herunterladbare Archiv mit Leanstral hat eine Größe von 121 GB und ist für den Einsatz 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 Vibe-Entwicklung im offenen Agenten mistral-vibe verwendet werden und lässt sich auch mit dem Werkzeug Aeneas zur Verifizierung von Code in der Programmiersprache Rust integrieren. Als Eingabeparameter werden Text und Bilder akzeptiert, als Ausgabe wird nur Text geliefert. Die Analyse des Bildinhalts wird unterstützt.
Zur Bewertung der Möglichkeiten von KI-Modellen in Bezug auf die Qualität der formalen Verifizierung von Code und das Verfassen mathematischer Beweise wurde ein neuer Testsatz FLTEval entwickelt. In den durchgeführten Tests übertraf das Modell Leanstral deutlich die bestehenden Open-Source-Modelle Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B und GLM5 744B-A40B, zeigte ähnliche Ergebnisse wie die Modelle Claude Haiku 4.5 und Claude Sonnet 4.6 von Anthropic, blieb jedoch hinter dem Modell Claude Opus 4.6 zurück. Insbesondere erzielte das Modell Opus 39,6 Punkte, während Leanstral 21,9 Punkte bei einem Durchgang und 31,9 Punkte bei 16 Durchgängen erreichte. Dabei betrugen die Kosten für die Nutzung von Opus 1650 US-Dollar, während Leanstral 18 US-Dollar bei einem Durchgang und 290 US-Dollar bei 16 Durchgängen kostete. Das Modell Haiku erhielt 23 Punkte bei Kosten von 184 US-Dollar, während das Modell Sonnet 23,7 Punkte bei Kosten von 549 US-Dollar erzielte.
Quelle: opennet.ru
