Article
Leanstral 1.5: Mistral's neues Open-Source-Modell für formale Beweise
Mistral veröffentlicht Leanstral 1.5 – ein Apache-2.0 lizenziertes Modell mit 119B total und nur 6B aktiven Parametern, spezialisiert auf formale Verifikation in Lean 4.
Die Benchmarks sind beeindruckend: Leanstral 1.5 saturiert miniF2F komplett, löst 587 von 672 PutnamBench-Problemen, und erreicht State-of-the-Art auf FATE-H (87%) und FATE-X (34%). Aber was bedeutet das praktisch?
Das Modell wurde durch drei Phasen trainiert: Mid-Training, Supervised Fine-Tuning, und Reinforcement Learning mit CISPO. Es arbeitet in zwei RL-Umgebungen: In der einen muss es Theoreme beweisen oder widerlegen, mit Lean-Compiler-Feedback als Belohnung. In der anderen agiert es als “Proof Engineer” und sucht aktiv nach Beweisen.
Praktischer Nutzen: Das Modell hat 5 bisher unbekannte Bugs in 57 getesteten Repositories gefunden – Beweis, dass formale Methoden effektiv für echte Code-Verifikation sein können.
Der Clou: Leanstral 1.5 ist vollständig Open-Source, via Hugging Face verfügbar, und Mistral bietet eine kostenlose API. Für Proof Engineering in Lean 4 ist dies ein signifikanter Schritt nach vorne – formale Verifikation wird für Praktiker zugänglicher.