Mistral bringt Leanstral 1.5: offenes Modell für formale Beweise und Code-Verifikation in Lean 4

Leanstral 1.5 ist ein Spezialmodell für Lean 4, einen Beweisassistenten, in dem sich mathematische Sätze und Software-Spezifikationen maschinenprüfbar formalisieren lassen. Architektonisch ist es ein Mixture-of-Experts-Modell mit 119 Milliarden Parametern insgesamt und etwa 6,5 Milliarden aktiven Parametern pro Token (128 Experten, davon 4 pro Token aktiv). Die Gewichte stehen unter Apache 2.0 auf Hugging Face; zusätzlich bietet Mistral einen kostenlosen API-Endpunkt (leanstral-1-5) und den Aufruf über das hauseigene Tool Mistral Vibe (vibe --agent lean).

Auf den von Mistral genannten Benchmarks erreicht das Modell 100 Prozent auf miniF2F (laut Anbieter auf Validierungs- und Testset gesättigt), löst 587 von 672 Aufgaben auf PutnamBench und erzielt 87 Prozent auf FATE-H sowie 34 Prozent auf FATE-X, die Mistral jeweils als State of the Art ausweist. Diese Werte sind Anbieter-Eigenmessungen und bislang nicht unabhängig nachgeprüft.

Der praxisnähere Teil: In einem Code-Verifikationstest identifizierte Leanstral nach Mistrals Angabe fünf bisher unbekannte Fehler über 57 getestete Repositories hinweg, darunter eine kritische Überlauf-Schwachstelle in der Vorzeichenfunktion der varinteger-Bibliothek. Mistral hebt zudem starkes Test-Time-Scaling hervor – die Leistung steige bei Rechenbudgets bis zu vier Millionen Token pro Problem weiter an.

Einordnung: Existenz, Lizenz, Architektur und Verfügbarkeit sind über den Mistral-Blog und die Hugging-Face-Model-Card (beide Primärquelle) belegt; The Decoder zeichnet die Meldung auf Deutsch nach. Die Leistungszahlen bleiben anbieter-selbstberichtet – der belastbare Kern der Meldung ist die offene Verfügbarkeit eines Lean-4-Verifikationsmodells und die konkret gefundenen realen Fehler, nicht die einzelnen Benchmark-Prozente.