Mistral veröffentlicht Leanstral 1.5 für formale Verifikation in Lean 4

Mistral AI hat mit Leanstral 1.5 ein offen verfügbares Modell für formale Verifikation vorgestellt. Das System ist auf Proof Engineering in Lean 4 ausgerichtet und soll mathematische Beweise sowie Verifikationsaufgaben in dieser Umgebung unterstützen.

Wie Mistral in einem Blogbeitrag zu Leanstral 1.5 mitteilt, steht das Modell unter der Apache-2.0-Lizenz bereit. Genannt werden 119 Milliarden Gesamtparameter, von denen 6 Milliarden aktiv sind. Mistral verweist zudem auf die Verfügbarkeit über Hugging Face und eine API. Im Mittelpunkt steht der Einsatz für Proof Engineering mit Lean 4.

Der Anbieter beschreibt Leanstral 1.5 als Nachfolger eines früheren Modells und hebt Fortschritte bei Benchmarks für formale mathematische Aufgaben hervor. Im Beitrag nennt Mistral Ergebnisse auf miniF2F, PutnamBench, FATE-H und FATE-X. Konkrete Vergleichswerte führt das Unternehmen dort als Leistungsnachweis für die neue Version an.

Neben den Benchmark-Ergebnissen skizziert Mistral auch den Trainingsaufbau. Demnach wurde Leanstral 1.5 in mehreren Phasen entwickelt, darunter Mid-Training, Supervised Fine-Tuning und Reinforcement Learning. Dabei spielte laut Beschreibung insbesondere die Interaktion mit der Lean-Umgebung eine wichtige Rolle, um Beweise zu erzeugen und zu überprüfen.

Darüber hinaus verweist Mistral auf praktische Tests außerhalb klassischer Benchmarks. Der Blogbeitrag beschreibt Auswertungen an realen Repositories und stellt die Nutzung des Modells für die Prüfung und Unterstützung formaler Entwicklungsarbeit in den Vordergrund.

Weitere Details und die Bereitstellung des Modells verlinkt Mistral direkt im offiziellen Ankündigungsbeitrag.