Diese neue KI prüft ihren Code mathematisch auf Fehler

Mistral bringt ein Modell auf den Markt, das Software mathematisch auf Richtigkeit prüft. Die Benchmarks überzeugen.

Andreas Becker16.03.26 Nano Banana

Kurzfassung Quellen

Mistral AI veröffentlicht das neue Open-Source-Modell Leanstral für Softwareentwickler.
Die KI nutzt die Sprache Lean 4, um Programmcode direkt mit mathematischen Beweisen auf Fehlerfreiheit zu prüfen.
Dank einer effizienten Sparse-Architektur arbeitet das Modell extrem kostengünstig und schlägt deutlich größere Konkurrenten.
Nutzer können die Leistung der KI durch parallele Durchläufe flexibel skalieren und laden die Gewichte kostenfrei herunter.

Mistral AI bringt mit Leanstral ein spezialisiertes Open-Source-Modell für Softwareentwickler auf den Markt. Die KI schreibt nicht nur Programmcode, sondern beweist dessen fehlerfreie Funktion direkt auf mathematischer Ebene.

Fokus auf mathematische Präzision

Bisherige KI-Modelle generieren Code, der oft versteckte Fehler enthält. Leanstral löst dieses Problem durch den Einsatz der Umgebung Lean 4 für formale Beweise. Die KI wandelt die Vorgaben in funktionierenden Programmcode um und liefert den mathematischen Beweis für dessen fehlerfreie Funktion direkt mit.

Das Modell basiert auf einer effizienten Sparse-Architektur. Von den insgesamt 119 Milliarden Parametern nutzt die KI für eine einzelne Aufgabe nur etwa 6 Milliarden aktiv. Diese gezielte Aktivierung spart enorm viel Rechenleistung.

Hohe Leistung schlägt große Konkurrenten

Um die Fähigkeiten realistisch zu messen, veröffentlicht Mistral den neuen Benchmark FLTEval. Dieser Test bewertet die KI bei anspruchsvollen Ingenieursaufgaben jenseits von simplen Rechenbeispielen.

Leanstral dominiert in dieser Auswertung die quelloffene Konkurrenz. Das Modell schlägt riesige Systeme wie Kimi-K2.5 mit einer Billion Parametern oder GLM5 mit 744 Milliarden Parametern deutlich. Auch das große Qwen3.5-Modell bleibt in allen Durchläufen messbar hinter Leanstral zurück.

Nutzer steuern die Leistung der neuen KI gezielt durch paralleles Rechnen. Bei einem einfachen Durchlauf, einem sogenannten Pass, erreicht das Modell 21,9 Punkte. Erhöht man die Durchläufe auf vier, steigt das Ergebnis auf 29,3 Punkte.

Quelle: Mistral

Effizienz im Preisvergleich

Diese parallele Berechnung macht das System besonders kosteneffizient im direkten Vergleich mit geschlossenen Modellen. Ein Basis-Durchlauf von Leanstral kostet in der Referenzauswertung 18 US-Dollar. Für 290 US-Dollar führt das System 16 Durchläufe durch und erreicht einen starken Wert von 31,9 Punkten.

Andere Anbieter verlangen für eine ähnliche Leistung deutlich mehr Geld. Das Konkurrenzmodell Sonnet erzielt lediglich 23,7 Punkte, kostet aber bereits 549 US-Dollar.

Nur das absolute Spitzenmodell Opus übertrifft Leanstral mit 39,6 Punkten, schlägt allerdings mit immensen Kosten von 1.650 US-Dollar zu Buche. Interessierte Entwickler laden die Modellgewichte ab sofort unter einer offenen Apache-2.0-Lizenz herunter. Zudem stehen Anbindungen über eine freie API und das Model Context Protocol bereit.