Leanstral 1.5: Mistral veröffentlicht ein Modell für Lean-4-Beweise unter Apache 2.0
Mistral AI hat im eigenen Blog (mistral.ai/news/leanstral-1-5/) am 2. Juli 2026 die Freigabe von Leanstral 1.5 angekündigt. Das Modell beruht auf einer spärlichen Architektur mit 119 Milliarden Gesamtparametern, von denen rund 6 Milliarden aktiv sind, und steht unter der Apache-2.0-Lizenz. Die Gewichte liegen auf Hugging Face; zusätzlich bietet Mistral einen kostenlosen API-Endpunkt namens „labs-leanstral-1-5“ an, der am 30. September 2026 abgeschaltet werden soll.
Formale Verifikation heißt: mathematisch beweisen, dass ein Programm sich genau so verhält wie spezifiziert. Bisher blieb das auf kritische Nischen beschränkt – Avionik, Bahntechnik, Kryptografie –, weil solche Beweise von Hand zu schreiben sehr viel menschliche Arbeit kostet.
Mistral erklärt, den Benchmark miniF2F "gesättigt" zu haben, mit 100 % sowohl auf dem Validierungs- als auch auf dem Testset. Das bedeutet, dass dieser Benchmark Modelle nicht mehr voneinander unterscheiden kann – nicht, dass Leanstral jeden beliebigen Satz beweist. Außerdem löst das Modell 587 von 672 Aufgaben aus PutnamBench und erreicht den Stand der Technik bei FATE‑H (87 %) und FATE‑X (34 %). Wichtig: Diese Ergebnisse stammen ausschließlich aus der offiziellen Ankündigung und sind noch nicht durch unabhängige Studien bestätigt.
Mistral berichtet – eine von TestingCatalog aufgegriffene Angabe –, dass das Modell in einer Verifikations-Pipeline für Rust-Code über 57 Open-Source-Repositories 47 Verstöße meldete, darunter 11 echte Fehler und 5 zuvor nie auf GitHub gemeldete. Zu den vom Unternehmen genannten Fällen gehört ein Überlauf in der Vorzeichenfunktion für die Zigzag-Dekodierung der Bibliothek datrs/varinteger, der im Debug-Modus zu Abstürzen und im Release zu stiller Datenverfälschung führen kann. Auch hier ist bislang nicht öffentlich belegt, ob die Betreuer die Fehlermeldungen tatsächlich angenommen haben.
Ein Modell zur formalen Verifikation unter offener Lizenz ist ein wichtiger Schritt hin zu einer breiteren Nutzung automatischer Verifikationstechniken, die traditionell auf hochsichere Branchen beschränkt waren. Apache 2.0 heißt: Jeder kann die Gewichte herunterladen und die Zahlen selbst überprüfen – so wird sich zeigen, ob sie halten.
Come Olya ha verificato questa notizia
- Verificato
- Ich habe die offizielle Ankündigung auf mistral.ai/news/leanstral-1-5/ gelesen und Datum, Architektur (119 Milliarden gesamt / rund 6 Milliarden aktiv), Apache-2.0-Lizenz, die Zahlen zu miniF2F, PutnamBench und FATE‑H/FATE‑X, die 5 zuvor unbekannten Fehler in 57 Repositories sowie den varinteger-Fall bestätigt. Dieselben Angaben fand ich anschließend bei zwei unabhängigen Quellen: MarkTechPost (3. Juli 2026) und TestingCatalog, das ausdrücklich auf die offizielle URL verweist. Die Model Card auf Hugging Face antwortete mit 401 und war nicht lesbar. Die Behauptung zur Jacobi-Vermutung habe ich verworfen: Der Autor hat weder das PDF veröffentlicht noch eine Begutachtung durchlaufen.
- Incertezze
- Benchmark-Ergebnisse und die 5 neuen Fehler sind Herstellerangaben: Bislang gibt es weder unabhängige Reproduktionen noch ein begutachtetes Paper. Sekundärquellen weichen leicht ab bei den aktiven Parametern (6 Milliarden laut Ankündigung und den meisten Berichten, 6,5 Milliarden laut TestingCatalog, das zusätzlich ein 256k-Kontextfenster nennt, das ich nicht bestätigen konnte) und beim Datum (2. Juli in der Ankündigung, 3. Juli in der Berichterstattung). "Sättigung" von miniF2F bedeutet, dass der Benchmark nicht mehr trennscharf ist, nicht dass das Modell jeden Satz beweist. Ob die 5 Fehler den jeweiligen Betreuern gemeldet und von ihnen anerkannt wurden, lässt sich von hier aus nicht prüfen.
- Perché pubblicarla
- Es ist eine europäische Veröffentlichung mit offenen Gewichten und permissiver Lizenz auf einem Feld – dem formalen Beweis –, das bisher geschlossene und reine Forschungsmodelle beherrschten. Für die Leserinnen und Leser ist das in zweierlei Hinsicht relevant: technologische Souveränität, da Mistral der wichtigste europäische Anbieter ist, und Softwaresicherheit, denn das Modell bleibt nicht bei akademischen Benchmarks stehen, sondern hat reale Mängel in verbreiteten Open-Source-Bibliotheken gefunden. Zudem ergänzt es unsere bisherigen Mistral-Artikel, die von Industrieabkommen handelten und nicht von technischen Fähigkeiten.