Leanstral 1.5: Beweis-Fülle für alle
(mistral.ai)- Im Zuge des Trends, formale Verifikation näher an reale Entwicklungsarbeit heranzuführen, hat Mistral AI Leanstral 1.5, ein Apache-2.0-Modell für Lean 4, veröffentlicht
- Das Modell aktiviert nur 6B von insgesamt 119B Parametern und lernt durch Mid-Training, Supervised Fine-Tuning und CISPO-Reinforcement-Learning sowohl das Schreiben von Beweisen als auch Arbeiten an Code-Repositories
- Mit miniF2F 100 %, PutnamBench 587/672, FATE-H 87 % und FATE-X 34 % zeigt es starke Leistung in Benchmarks für mathematische Beweise und in Bewertungen realer Proof-Engineering-Aufgaben
- Bei der Verifikation echten Codes fand es über einen Beweis der O(log n)-Zeitkomplexität von AVL-Bäumen und eine Rust-to-Lean-Pipeline 11 echte Bugs in 57 Repositories
- Gewichte und die kostenlose API
leanstral-1-5sind veröffentlicht, sodass das Modell direkt für praktisches Proof Engineering wie Theorembeweise, Proof-Debugging und Repository-Beiträge eingesetzt werden kann
Veröffentlichung von Leanstral 1.5 und Modelleigenschaften
- Leanstral 1.5 ist ein Modell, das für Proof Engineering in Lean 4 entwickelt wurde
- Die Lizenz ist Apache-2.0; die Modellgröße beträgt insgesamt 119B Parameter, davon 6B aktive Parameter
- Durch verbesserte formale Verifikationsleistung lässt es sich nicht nur für mathematische Benchmarks, sondern auch zur Verifikation realer Code-Eigenschaften nutzen
- Es sättigt miniF2F, löst 587 von 672 Aufgaben in PutnamBench und erreicht 87 % bei FATE-H sowie 34 % bei FATE-X
Dreistufiges Training mit gelerntem Proof-Feedback
- Das Training besteht aus drei Stufen: Mid-Training, Supervised Fine-Tuning und CISPO-basiertem Reinforcement Learning
- Für das Reinforcement Learning werden zwei Umgebungen verwendet
- Multi-Turn-Umgebung: Das Modell erhält eine Theorem-Aussage, beweist oder widerlegt sie und überarbeitet den Beweis wiederholt auf Basis des Feedbacks des Lean-Compilers
- Wenn der Beweis kompiliert, gilt der Versuch als erfolgreich; andernfalls läuft die Schleife weiter, bis die Aufgabe gelöst oder das Budget ausgeschöpft ist
- Code-Agent-Umgebung: Das Modell bearbeitet Dateien wie ein Entwickler in einem rohen Dateisystem, führt bash-Befehle aus und prüft Ziele, Fehler und Typinformationen in Echtzeit über den Lean Language Server
- Die Code-Agent-Umgebung deckt lange Aufgaben ab, etwa das Vervollständigen partieller Beweise in Repositories, das Schreiben von Hilfslemmata und das Fortsetzen der Arbeit auch nach mehreren Kontextkompressionen
- Die endgültige Korrektheit wird anhand der Zieltheoremliste in Mistrals SafeVerify-Fork verifiziert
Benchmarks für Mathematik und Proof Engineering
- Für die Evaluation werden miniF2F, PutnamBench, FATE-H/FATE-X und FLTEval verwendet
- miniF2F ist ein Benchmark für formale Mathematik mit Aufgaben von Grundschulniveau bis hin zu IMO-Niveau
- PutnamBench besteht aus 672 Aufgaben der Putnam Mathematical Competition
- FATE-H und FATE-X sind Benchmarks für abstrakte Algebra auf Graduate- bzw. PhD-Niveau
- FLTEval bewertet den Schwierigkeitsgrad von Proof Engineering auf Basis echter Pull Requests aus dem Repository zu Fermat’s Last Theorem
- In miniF2F erreicht es sowohl auf dem Validierungs- als auch auf dem Testset 100 %
- In PutnamBench und FATE-H/X wird es ohne Beweisleitfäden in natürlicher Sprache mit Goedel-Architect, Seed-Prover 1.5 high und AxProverBase verglichen
- FATE-H/X-Leistung:
- FATE-H erreicht 87 %, FATE-X 34 % und setzt damit neue Bestwerte
- In PutnamBench löst es 7 Aufgaben mehr als Seed-Prover 1.5 high; die Kosten pro Aufgabe liegen bei etwa 4 US-Dollar
- Die High-Einstellung von Seed-Prover nutzt ein Budget von 10 H20-days pro Aufgabe, mit geschätzten Kosten von über 300 US-Dollar
- Einige höher platzierte Prover erhalten Beweisleitfäden in natürlicher Sprache oder laufen, wie Aleph Prover, unter anderen Bedingungen mit Kosten von 54–68 US-Dollar pro Aufgabe
Skalierbarkeit bei langen Reasoning-Budgets und FLTEval
- Bei PutnamBench steigt die Pass@8-Leistung von Leanstral 1.5 mit wachsendem Token-Budget glatt und monoton an
- In Experimenten mit einem Token-Budget pro Versuch von 25k bis 4M steigt die Zahl gelöster Aufgaben wie folgt
- 50k Token: 44 Aufgaben
- 200k Token: 244 Aufgaben
- 1M Token: 493 Aufgaben
- 4M Token: 587 Aufgaben
- Das Verhalten, bei langen Beweisen nicht abzubrechen, sondern über Millionen von Tokens hinweg weiter zu schlussfolgern, Dateien zu bearbeiten und Korrekturen vorzunehmen, führt zu Leistungssteigerungen
- Auch FLTEval wird vollständig als Open Source veröffentlicht
- In FLTEval steigert Leanstral 1.5 pass@1 von 21,9 auf 28,9 und pass@8 von 31,9 auf 43,2
- pass@8 von 43,2 übertrifft die 39,6 von Opus 4.6, bei einem Siebtel der Kosten
- Unter den Open-Source-Modellen zeigt es auch gegenüber 3- bis 10-mal größeren Modellen eine bessere Leistung
Beispiele für reale Code-Verifikation
-
Beweis der Zeitkomplexität von AVL-Bäumen
- AVL-Bäume sind selbstbalancierende binäre Suchbäume, die bei Einfügen und Löschen durch Rebalancing eine Höhe von O(log n) beibehalten
- Leanstral 1.5 verifiziert für eine reale Implementierung, dass Einfügen und Löschen O(log n) sind
- Diese Aufgabe erforderte strukturelle Induktion, die die rekursive Baumstruktur widerspiegelt, die Behandlung monadenbasierter Zeitverfolgung und eine vollständige Fallanalyse der Rebalancing-Pfade
- Der Beweis lief über mehr als 2,7 Millionen Tokens und 22 Kontextkompressionen
- Leanstral entfaltet systematisch jede Ebene der TimeM-Monade und macht so Berechnungen sichtbar, die mit dem Kontrollfluss vermischt sind
- Für das Einfügen stellt es eine Grenze von 48 Schritten pro Höheneinheit plus nahezu konstantem Term auf und verbindet Höhe und Baumgröße über eine logarithmische Beziehung
-
Bugs in Rust-Code finden
- Das Bug-Detection-Experiment besteht aus einer Pipeline, in der Aeneas Rust-Code nach Lean übersetzt und Leanstral aus dem Code die Nutzerintention ableitet, um Konsistenzeigenschaften zu erzeugen
- Leanstral versucht, jede Eigenschaft 4-mal zu beweisen; wenn alle Versuche scheitern, versucht es anschließend 4-mal, deren Negation zu beweisen
- In 57 Repositories wurden 47 verletzte Eigenschaften markiert, von denen 11 auf echte Bugs hinweisen
- 5 der echten Bugs waren zuvor nicht auf GitHub gemeldet worden
- Ein Beispiel wurde in der zigzag-decoding-sign-Funktion der Bibliothek datrs/varinteger gefunden
- Bei Eingabe von
Std.U64.MAXläuft der Ausdruck(value + 1)über - Im Debug-Modus kommt es zu einem Crash, im Release-Modus zu stiller Datenbeschädigung
- Dieser Edge Case ist ein Beispiel, das typische Tests und Fuzzing leicht übersehen
Veröffentlichung und Nutzung
- Die Gewichte sind auf Hugging Face veröffentlicht
- Der kostenlose API-Endpunkt wird in der Model Card unter dem Namen
leanstral-1-5bereitgestellt - Als Nutzungsumgebung wird Mistral Vibe empfohlen
- Der Einstieg erfolgt in dieser Reihenfolge: Mistral Vibe einrichten, Leanstral 1.5 installieren, den Agent ausführen, optional Lean LSP MCP installieren und mit Proof-Aufgaben beginnen
- Für Lean LSP MCP wird empfohlen, es durch Hinzufügen zu
~/.vibe/config.tomlzu installieren - Falls kein bestehender MCP-Server vorhanden ist, muss
mcp_servers = []möglicherweise entfernt werden - Leanstral kann zum Lösen von Theoremen, zum Debuggen von Beweisen und für Beiträge zu Repositories verwendet werden
1 Kommentare
Meinungen auf Hacker News
Die Kritik, dass es für Mistral schwierig ist, mit großen Modellen zu konkurrieren, ist berechtigt, aber tatsächlich scheint der Fokus darauf zu liegen, bestimmte Funktionen in kleinen Modellen in hoher Qualität bereitzustellen
Ich nutze Mistral für Aufgaben wie OCR oder Dateianalyse; wenn man 100 Dollar auf das Konto lädt, läuft das ein Jahr lang, ohne dass man sich über das Anfragevolumen Sorgen machen muss
Die Kosten sind extrem gering, sodass es auch dann genug Wert bietet, wenn es nicht mit Opus 4.8 konkurrieren kann
Ordentliche Qualität zu einem niedrigen Preis wirkt eher wie ein Nischenmarkt, als später den zehnfachen Preis für höchste Qualität zu zahlen, um Fehler zu reduzieren
OCR ist bereits fast eine Commodity und wird auch von Open-Source-Modellen oder Anbietern wie AWS standardmäßig bereitgestellt
Außerdem lässt sich mit einem Preisschild von 100 Dollar pro Jahr kaum Loyalität aufbauen, und ohne Wechselkosten können Kunden sofort gehen, sobald ein niedrigerer Preis auftaucht
Wenn ein leicht kopierbares Low-Cost-Tool keinen Kunden-Lock-in hat, ist es eher ein Feature als ein Geschäft
Aus Käufersicht ist das gut, aber wenn man will, dass europäische Unternehmen langfristig über Produktfähigkeiten mit globalen Wettbewerbern konkurrieren, wirkt es wie eine schlechte Strategie
Die Arbeit an sich ist gut, aber das Beispiel für den gefundenen Bug fühlte sich seltsam an
Es hieß, dass in der sign-Funktion des Zigzag-Decodings bei Eingabe von
Std.U64.MAX(value + 1)überläuft, was im Debug-Modus zu einem Crash und im Release-Modus zu stiller Datenbeschädigung führt; ich weiß nicht, ob man das wirklich eine Randbedingung nennen kann, die Tests „normalerweise übersehen“Schlechte Tests würden das übersehen, aber sorgfältige Menschen oder Machine-Learning-basierte Coding-Systeme sind ziemlich gut darin, auf die Idee zu kommen: „Ich sollte Extremwerte testen.“ Besonders bei Code, der Benutzereingaben parst
Ich frage mich, ob sie auch interessantere Bugs gefunden haben, die sich nur nicht schnell erklären ließen, und deshalb dieses Beispiel gewählt haben
Bei einer solchen Encoding-Bibliothek wäre Fuzzing die grundlegende Erwartung an ordentlichen Code, und ich glaube, es hätte das mit ziemlicher Sicherheit in wenigen Sekunden gefunden
Tatsächlich habe ich mit
proptesteinen sehr einfachen Round-Trip-Test erstellt, und in weniger als einer Sekunde gab es Dutzende Fehlschläge sowie folgendes Ergebnis:thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:Test failed: attempt to multiply with overflow.minimal failing input: value = 4611686018427387904successes: 2local rejects: 0global rejects: 0Der Vorteil von Lean wird deutlich: Man muss weniger clever auswählen, welche Beispiele man testen sollte
Das macht mich neugierig auf den Hintergrund der Autoren
Jedes System für Property-based Testing, das etwa seit 1980 erfunden wurde, sucht nach Grenzwerten
Praktisches Testen kann wegen der Semantik von C und C++ oder deren Fehlen schwierig sein. Denn es ist zulässig, dass der Compiler für jede Eingabe, die zu undefiniertem Verhalten führt, „Test bestanden“ ausgibt
In der Mitte des Artikels werden mehrere Frontier-LLMs verglichen, aber alle sind Modelle von vor einem halben Jahr
Das kam ziemlich lustig rüber, nach dem Motto: „Unser neues Modell ist besser als chinesische Modelle von vor drei Generationen“
Die Bibliothek ist https://github.com/datrs/varinteger
Eine Woche vor Veröffentlichung des Papers wurde dasselbe Problem bereits in diesem Repository gemeldet, daher ist es vermutlich die richtige: https://github.com/datrs/varinteger/issues/8
Ich weiß nicht, ob diese Person bei Leanstral arbeitet oder ob Leanstral dieses Issue einfach übernommen hat
Die Bibliothek ist klein, ihre Tests sind erstaunlich dürftig, und seit acht Jahren wurde sie fast nicht angerührt: https://github.com/datrs/varinteger/blob/master/tests/test.r...
Die Downloads liegen bei etwa 1.000 pro Tag und wirken damit eher niedrig: https://crates.io/crates/varinteger
Deshalb wirkt es nicht wie ein besonders großer Erfolg, um ihn als einziges Beispiel herauszustellen. Automatische Erkennung ist durchaus nützlich, aber ich bin mir nicht sicher, ob das in diesem Teilgebiet eine bemerkenswerte Leistung ist
Ich habe noch keine LLMs zum Schreiben von Beweisen verwendet, aber da die Trainingsdaten eher knapp sind, wäre ich nicht überrascht, wenn sie holpriger sind als allgemeine Coding-Modelle
Nebenbei: Auf https://crates.io/crates/varinteger wird https://github.com/mafintosh/varinteger-rs angezeigt, aber diese Adresse leitet auf https://github.com/datrs/varinteger weiter, daher scheint es entgegen dem ersten Eindruck dieselbe Bibliothek zu sein
Der Kern ist nicht, einen Bug zu finden, sondern zu beweisen, dass bestimmte Arten von Bugs unter bestimmten Annahmen nicht existieren
Aber diese Geschichte lässt sich schwer verkaufen, deshalb driftet Marketing oft in Richtung „Wir haben diesen Bug gefunden“ ab
Kann es auch für jemanden nützlich sein, der Lean überhaupt nicht kennt? Man möchte Software verifizieren, an der man arbeitet, hat aber keine Erfahrung mit formaler Verifikation
Es ist unklar, ob man allein mit Spezifikation, Code und begrenzter Lernzeit brauchbare Ergebnisse erzielen kann
Es ist weniger Mathematik, sondern eher wie das Lesen von Haskell-Typen; nur das Vokabular scheint stark aus der Mathematik entlehnt zu sein
Man könnte sich im Dialog vielleicht auch dabei helfen lassen, Lean-Code für die Verifikation einer Anwendung zu schreiben, sicher ist das aber nicht
Andernfalls kann man die Ausgabe nicht verifizieren
Mechanisch könnte zwar eine als korrekt geprüfte Aussage bewiesen worden sein, aber wenn man nicht weiß, was diese Aussage bedeutet und ob sie tatsächlich das abdeckt, was man verifizieren wollte, ist das bedeutungslos
Es ist erstaunlich, wie konsistent und flüssig die Modelle in Lean4 sind. Das galt nicht nur für Modelle an der Spitze, sondern auch für kleine lokale Modelle; LLMs scheinen Lean4 einfach gut zu verstehen
Ich habe noch einen Weg vor mir, bevor ich mich Lean4-Experte nennen würde, aber inzwischen brauche ich die Unterstützung nicht mehr zwingend, um nützliche Programme zu schreiben
Dass man auch mit sehr wenig Vorwissen Teilen vertrauen kann, die man nicht vollständig versteht, beschleunigt das Lernen enorm. Es ist praktisch und motivierend, auch mit unvollständigem Wissen verlässliche Programme zu erhalten
Es fühlt sich so an, als würden die Grenzen nicht durch den gesamten Zwischenbeweisprozess bestimmt, sondern durch den Teil der Sprache, der die Oberfläche der eigenen Axiome und Aussagen beschreibt. Mit der Zeit muss man mehr verstehen, um mehr tun zu können, aber in gewisser Weise kann man sicher auf N+1-Niveau arbeiten
Lean4 ist unabhängig von seiner Rolle als Theorem Prover auch eine angenehme Programmiersprache und erstaunlich schnell
Ich verwende es angebunden an
io_uring, und in vielen Fällen ist es deutlich schneller als C++/libuv oder Rust/TokioWenn gelegentlich lange Tails etwa bei der p99.99-Latenz auftreten, muss man tunen, zum Beispiel Zahlen auf feste Breite umstellen, aber auch C++ und Rust müssen getunt werden
Interessant, dass Lean 4 für formale Verifikation vorangetrieben wird
Ich dachte, dieser Bereich gehöre eher zu Isabelle/HOL und TLA+
Ich hätte zumindest ein Modell erwartet, das darauf trainiert ist, alle drei zu verwenden. Für die Vorwärtsableitung in linearer Algebra wirkt auch Isabelle/Isar besser; kann das jemand erklären?
In diesem Bereich wurde sogar Agda häufiger eingesetzt
Allerdings gewinnt Lean derzeit als Alternative erheblich an Schwung, insbesondere wegen seiner Fähigkeiten als universelle funktionale Programmiersprache
Persönlich halte ich Ansätze auf Basis von Hoare-Logik oder Separation Logic, bei denen sich Anforderungen und Spezifikationen leichter in Einklang bringen lassen, für praktischer. Dafny und F* gefallen mir
Amüsant war, dass die Entwickler in der Twitter-Ankündigung Le Chaton Fat nebenbei erwähnt haben
Unabhängig davon, ob sie tatsächlich an Le Chaton Fat beteiligt waren, scheint bald wirklich ein „neues großes Allzweckmodell“ zu kommen
Dass sie es auch nach dem Medientrubel direkt erwähnt haben, macht neugierig. Der Name dürfte gern kreativer sein als „Large 4“
In der neuesten OpenATP-Version kann man Leanstral 1.5 ausprobieren
OpenATP ist ein Open-Source-Python-Paket und eine CLI für agentische automatische Theorem Prover und unterstützt standardmäßig die lokale Ausführung in Docker oder die Remote-Ausführung in einer Modal-Sandbox
GitHub: https://github.com/henryrobbins/open-atp
Docs: https://open-atp.henryrobbins.com