Die Entwickler von Leanstral haben das KI-Modell Leanstral 1.5 veröffentlicht. Das mit der Apache-2.0-Lizenz freigegebene System konzentriert sich auf formale Verifikation und Beweisingenieurwesen in Lean 4. Obwohl das Modell über 119 Milliarden Gesamtparameter verfügt, arbeiten lediglich sechs Milliarden aktiv, was es effizient und kostengünstig macht. Die Gewichte stehen auf Hugging Face bereit, zudem wird ein kostenloser API-Endpunkt angeboten. Das Training von Leanstral 1.5 folgt einer dreistufigen Pipeline aus Midtraining, überwachtem Feintuning und Verstärkungslernen mit der CISPO-Methodik. Das System nutzt dabei zwei spezifische RL-Umgebungen: eine mehrstufige Umgebung für direkte Theorembeweise mit automatischer Compiler-Rückmeldung sowie eine Code-Agent-Umgebung, in der das Modell dateibasiert arbeitet, Befehle ausführt und den Lean-Language-Server zur Echtzeit-Analyse von Typen und Fehlern nutzt. Dieser Ansatz ermöglicht das Bewältigen langfristiger Aufgaben wie das Vervollständigen von Teilbeweisen oder das Erstellen von Hilfssätzen über mehrere Kontextkomprimierungen hinweg. In der Evaluation übertrifft Leanstral 1.5 aktuelle Referenzmodelle auf mehreren Benchmarks. Auf miniF2F wird eine Sättigung bei 100 Prozent erreicht. Auf PutnamBench löst das Modell 587 von 672 Aufgaben der Putnam Mathematical Competition. Zudem erzielt es neue State-of-the-Art-Ergebnisse mit 87 Prozent auf FATE-H und 34 Prozent auf FATE-X, die fortgeschrittene abstrakte Algebra testen. Auf FLTEval, das reale Pull-Requests aus dem Fermat-Repository nutzt, verbessert sich der pass@1-Wert auf 28,9 und übertrifft damit Opus 4.6 bei einem Bruchteil der Kosten. Das Modell demonstriert zudem eine starke Test-Time-Scaling-Eigenschaft: Steigt der Token-Budget pro Versuch, wächst die Lösungsrate kontinuierlich, da das Modell auch nach mehreren hunderttausend Tokens weiter reasoning und Code anpasst. Neben mathematischen Beweisen zeigt Leanstral 1.5 bedeutende Stärken in der Code-Verifikation. In einer Fallstudie bewies das Modell die Zeitkomplexität von O(log n) für AVL-Bäume über 2,7 Millionen Tokens und 22 Kontextkomprimierungen hinweg. Für reale Anwendungsfälle wurde eine Pipeline aufgebaut, die Rust-Code in Lean übersetzt und automatisch Korrektheitsbedingungen generiert. Bei der Untersuchung von 57 Open-Source-Repositories identifizierte das System elf echte Softwarefehler, darunter fünf unbekannte Lücken. Ein besonders kritischer Fehler trat in der Funktion zur Dekodierung vorzeichenbehafteter Integer-Strukturen auf und verursachte Überläufe unter bestimmten Randbedingungen, die konventionelle Tests nicht entdeckten. Für die Nutzung wird die Integration über Mistral Vibe empfohlen. Nach Erhalt eines API-Schlüssels können Nutzer das Modell direkt zur Beweisführung, Fehlersuche oder Repository-Beiträgen einsetzen. Optional wird die Installation des Lean LSP MCP-Servers zur Verbesserung der Echtzeit-Interaktion empfohlen. Mit der vollständigen Open-Source-Veröffentlichung markiert Leanstral 1.5 einen Schritt hin zu praktikablen, formal verifizierbaren Entwicklungsmethoden, die komplexe mathematische und softwaretechnische Probleme zuverlässig und effizient adressieren.