|
06.07.2026 18:16 Uhr |
Mistral AI hat mit Leanstral 1.5 ein spezialisiertes KI-Modell für formale Verifikation und mathematische Beweise veröffentlicht. Das unter Apache-2.0 lizenzierte Modell arbeitet mit dem interaktiven Theorembeweiser Lean 4 und soll sowohl akademische Mathematik als auch praktische Codeprüfung abdecken.
Wie Mistral AI in seinem Blogpost erläutert, umfasst die Architektur 119 Milliarden Parameter insgesamt, von denen lediglich 6 Milliarden aktiv sind. Das Modell steht als freier API-Endpunkt sowie über Hugging Face zum Self-Hosting bereit.
Auf dem miniF2F-Benchmark erreicht Leanstral 1.5 laut Mistral 100 Prozent auf Validierungs- und Testset. Beim PutnamBench löst das Modell 587 von 672 Aufgaben aus dem Putnam Mathematical Competition – ein Benchmark, der logisches Denken und lange Beweisketten erfordert. Leanstrals Rechnerei soll dabei laut Mistral teilweise nur ein Siebtel von dem gekostet haben, was Opus 4.6 für die gleiche Aufgabe verbraucht hätte. Auf den Benchmarks FATE-H und FATE-X für abstrakte Algebra auf Graduierten- beziehungsweise Promotionsniveau erreicht Leanstral 87 respektive 34 gelöste Aufgaben.
Neben mathematischen Beweisen demonstriert Mistral eine Pipeline zur automatischen Bug-Erkennung in Rust-Projekten. Dabei übersetzt das Werkzeug Aeneas Rust-Code nach Lean, woraufhin Leanstral Korrektheitseigenschaften ableitet und versucht, diese zu beweisen oder zu widerlegen. In einem Test mit 57 Open-Source-Repositories identifizierte die Pipeline 47 verletzte Eigenschaften, von denen sich 11 als echte Bugs herausstellten – 5 davon waren zuvor auf GitHub nicht gemeldet.
Leanstral 1.5 erweitert Mistrals Portfolio an spezialisierten KI-Werkzeugen, das kürzlich bereits mit Mistral OCR 4 für Dokumentenanalyse gewachsen war. Die Apache-2.0-Lizenz ermöglicht Self-Hosting – für Unternehmen mit hohen Compliance-Anforderungen ein relevanter Aspekt.
(rie)