KIberblick

Leanstral 1.5: Open Source findet echte Bugs

Mistrals Leanstral 1.5 steht unter Apache 2.0 und fand in 57 Repos fünf unbekannte Bugs. Was das Modell kann, was nicht und was Open Source hier heißt.

Entwickler:inQA / Tester:in
5. Juli 20267 Min. Lesezeit

Mistral hat am 2. Juli Leanstral 1.5 veröffentlicht, ein Modell, das mathematische Beweise in der Sprache Lean 4 schreibt. Klingt nach einem Spezialwerkzeug für Formal-Methods-Leute, hat aber einen Nebeneffekt, der weiter reicht: In einem Test scannte das Modell 57 Open-Source-Repositories und fand dabei fünf Bugs, die vorher niemand auf GitHub gemeldet hatte. Darunter ein Overflow in der Bibliothek datrs/varinteger, bei dem der Ausdruck (value + 1) bei der Eingabe Std.U64.MAX überlief.

Was Leanstral eigentlich ist

Der Kern des Modells ist formale Verifikation, nicht Alltags-Coding. Lean 4 ist ein Beweisassistent: Man formuliert eine Aussage über ein Programm oder ein mathematisches Theorem, und das System prüft maschinell, ob der Beweis lückenlos stimmt. Leanstral schreibt diese Beweise. Auf dem Benchmark miniF2F, der von Schulmathematik bis Mathematik-Olympiade reicht, erreicht es 100 Prozent auf Validierungs- und Testmenge. Auf PutnamBench löst es 587 von 672 Aufgaben und führt damit das Open-Source-Feld an.

Das Bug-Finden fällt dabei als Nebenprodukt ab. Wer einen Beweis über die Korrektheit einer Funktion führen will, stößt automatisch auf die Fälle, in denen die Funktion sich falsch verhält. Genau so kam der varinteger-Overflow ans Licht. Das ist kein Ersatz für Cursor oder Claude Code beim Feature-Bauen, sondern ein Spezialwerkzeug für Code, dessen Korrektheit hart nachweisbar sein soll.

Warum "Open Source" hier wirklich stimmt

Bei Mistral lohnt der genaue Blick auf die Lizenz, denn nicht jedes Modell mit "offen" im Marketing lässt sich auch frei betreiben. Leanstral 1.5 steht unter Apache 2.0. Das bestätigen sowohl Mistrals Ankündigung als auch die Modellkarte auf Hugging Face. Die Gewichte sind frei herunterladbar, der Betrieb ist erlaubt, auch kommerziell. Das ist ein anderer Fall als bei Modellen unter der Mistral Research License oder reinen API-Modellen ohne Gewichte.

Modell-TypGewichteKommerzieller Selbstbetrieb
Apache 2.0 (z.B. Leanstral 1.5)frei herunterladbarerlaubt
Mistral Research License (MRL)herunterladbarnur Forschung, nicht kommerziell
Reines API-Modellnicht verfügbarnicht möglich

Für Teams, die Wert auf Datensouveränität legen, ist der Unterschied entscheidend: Mit Apache 2.0 bleibt der Code im eigenen Netz, es fließen keine Daten an einen Anbieter ab, und es gibt keine Nutzungsklausel, die einen kommerziellen Einsatz verbietet.

Der Haken: kein Laptop-Modell

Kostenlos in der Lizenz heißt nicht kostenlos in der Hardware. Leanstral 1.5 ist ein Mixture-of-Experts-Modell mit 119 Milliarden Parametern insgesamt, von denen pro Token nur rund 6 Milliarden aktiv sind (daher das Kürzel A6B im Modellnamen). Die aktive Zahl bestimmt die Rechenlast pro Token, aber alle 119 Milliarden Parameter müssen in den Speicher passen. Die Modellkarte empfiehlt für den Betrieb einen vLLM-Server mit --tensor-parallel-size 4, also ein Setup über vier GPUs.

Selbst hosten lässt sich das Modell also durchaus, aber es braucht ernsthafte Hardware, nicht das Notebook unter dem Schreibtisch. Was das konkret kostet, hängt weniger am Token-Preis als an der Arbeitsweise.

Was ein Verifikationslauf grob kostet

Preise pro Million Token sagen wenig darüber, was ein konkreter Einsatz kostet. Entscheidend ist, wie Leanstral arbeitet: nicht interaktiv wie ein Chatassistent, sondern als Batch-Aufgabe, die einmal über ein Projekt läuft. Im gezeigten Workflow übersetzt zuerst das Werkzeug Aeneas den Rust-Code nach Lean, dann versucht Leanstral jede abgeleitete Eigenschaft in bis zu acht Anläufen zu beweisen. Der Aufwand hängt also an der Zahl der Eigenschaften und Beweisversuche, nicht an den Codezeilen. Und er zielt vorerst auf Rust, weil Aeneas ein Rust-nach-Lean-Übersetzer ist.

Daraus ergeben sich zwei Wege, hier bewusst als grobe Beispielrechnung mit offen benannten Annahmen:

GPU mieten für den Lauf. Eine Cloud-GPU mit genug Speicher fürs quantisierte Modell (rund 70 GB, also etwa eine H200 oder zwei H100) kostet 2026 grob vier bis sechs Dollar pro Stunde. Ein Verifikationslauf ist eine einmalige Batch-Aufgabe, keine Dauerlast: Man mietet die Maschine für die Laufzeit und gibt sie danach frei. Nimmt man an, dass ein Lauf über eine mittelgroße Rust-Bibliothek zwischen ein paar Minuten und wenigen Stunden dauert, landet man pro gründlichem Durchgang im Bereich weniger Euro bis grob unter dreißig Euro. Kein Abo, sondern Kosten pro Lauf, ungefähr ein Kinoticket pro geprüftem Projekt.

Mistrals API nutzen. Zum Ausprobieren gibt es einen gedrosselten kostenlosen Tier. Darüber wird pro Token abgerechnet, und das ist der schwer greifbare Teil: Ein Beweis-Workload schwankt je nach Projekt zwischen ein paar Dutzend und mehreren Tausend Versuchen. Belastbarer als jede Vorab-Schätzung ist ein kleiner Testlauf über ein einzelnes Modul, dessen Verbrauch man dann hochrechnet.

Wer regelmäßig verifiziert, fährt mit eigener Hardware günstiger. Eine Workstation mit genug Speicher, etwa ein Mac Studio mit 128 GB oder mehr, ist eine vierstellige Einmalinvestition, danach kosten die Läufe im Wesentlichen Strom.

Einordnung

Leanstral passt in ein Muster, das wir seit Wochen beobachten: KI, die Sicherheitslücken findet. Vergangene Woche ging es um die Explosion gemeldeter CVEs, seit Modelle autonom nach Schwachstellen suchen. Leanstral zeigt die zugängliche Seite davon: Statt eines geschlossenen Konzern-Programms ein frei nutzbares Werkzeug, dessen Funde nachprüfbar sind, weil sie aus einem formalen Beweis stammen und nicht aus einer Wahrscheinlichkeitsschätzung.

Fazit

Leanstral 1.5 ist kein Allzweck-Coding-Modell, sondern ein Spezialist für beweisbare Korrektheit, der nebenbei echte Bugs in fremdem Code aufdeckt. Die Apache-2.0-Lizenz macht es zu echtem Open Source, das man auch kommerziell selbst betreiben darf. Der Preis dafür ist die Hardware: 119 Milliarden Parameter wollen versorgt werden. Für DACH-Teams, die formale Garantien und Datensouveränität zusammenbringen wollen, ist das ein bemerkenswertes Werkzeug, solange man weiß, wofür es gemacht ist und wofür nicht.

Quellen

Quellen3