Leanstral 1.5 : vérification formelle open-source
Original : Leanstral 1.5: Proof abundance for all
Pourquoi c'est important
L'open-source de la vérification formelle accélère l'adoption des méthodes rigoureuses dans le développement logiciel.
Mistral AI a lancé Leanstral 1.5, un modèle Apache-2.0 gratuit de 119B paramètres totaux (6B actifs), spécialisé en vérification formelle Lean 4. Il résout 587/672 problèmes PutnamBench, atteint 87% sur FATE-H et a détecté 5 bugs inédits dans 57 dépôts open-source.
Mistral AI a publié le 2 juillet 2026 Leanstral 1.5, la nouvelle version de son modèle dédié à la vérification formelle en Lean 4. Avec 119B paramètres totaux mais seulement 6B paramètres actifs (architecture mixture-of-experts), le modèle est distribué sous licence Apache-2.0, gratuitement via Hugging Face et une API dédiée.
Sur le plan des performances, Leanstral 1.5 sature le benchmark miniF2F, résout 587 des 672 problèmes PutnamBench, et établit un nouvel état de l'art sur FATE-H (87%) et FATE-X (34%). Au-delà des benchmarks académiques, le modèle a été testé sur 57 dépôts open-source réels, où il a découvert 5 bugs jusqu'alors inconnus.
L'entraînement repose sur trois étapes : mid-training, supervised fine-tuning, puis reinforcement learning via l'algorithme CISPO. Deux environnements RL ont été utilisés : un environnement multitour où le modèle prouve ou réfute un théorème en soumettant des preuves au compilateur Lean, et un second environnement orienté ingénierie de preuves agentique sur du code réel. Mistral positionne Leanstral 1.5 comme un outil pratique pour les développeurs souhaitant appliquer des méthodes formelles rigoureuses à des projets concrets.