Leanstral 1.5 : Mistral prouve qu'un modèle open-source spécialisé peut battre les géants sur la vérification formelle
Dans un écosystème dominé par les modèles propriétaires aux ressources colossales, Mistral AI continue de démontrer qu'une approche ciblée et ouverte peut faire la différence. Avec la sortie de Leanstral 1.5, l'entreprise française publie un modèle open-source (licence Apache 2.0) entièrement dédié à la vérification formelle dans le langage Lean 4 — et les résultats sur les benchmarks officiels sont difficiles à ignorer.
Lean 4 et vérification formelle : de quoi parle-t-on ?
Avant d'entrer dans les performances du modèle, un rappel de contexte s'impose. Lean 4 est un langage de programmation et un assistant de preuve conçu pour vérifier formellement des preuves mathématiques et la correction de logiciels. Contrairement aux tests unitaires classiques qui vérifient le comportement d'un programme sur un ensemble fini de cas, la vérification formelle cherche à prouver mathématiquement qu'un programme est correct pour toutes les entrées possibles.
C'est un domaine exigeant, longtemps réservé aux chercheurs académiques, mais qui suscite un intérêt croissant dans l'industrie — notamment pour les systèmes embarqués, les protocoles cryptographiques ou les smart contracts. L'idée d'automatiser une partie de ce processus avec un LLM spécialisé est donc particulièrement pertinente.
Des benchmarks qui parlent d'eux-mêmes
Mistral annonce des résultats impressionnants sur les principaux benchmarks de vérification formelle mathématique :
- miniF2F : 100 % de réussite sur ce benchmark couvrant des problèmes allant du niveau lycée aux olympiades mathématiques.
- PutnamBench : 587 problèmes résolus sur 672, issus du concours Putnam — l'une des compétitions mathématiques universitaires les plus prestigieuses aux États-Unis. Leanstral 1.5 domine l'ensemble des modèles open-source sur ce benchmark.
- FATE-H et FATE-X : Ces benchmarks d'algèbre évaluent des tâches de niveau master et doctorat (théorie des groupes, théorie des anneaux). Leanstral 1.5 obtient respectivement 87 % et 34 %, des scores en tête du classement open-source.
Le seul modèle qui surpasse Leanstral 1.5 sur PutnamBench est Aleph Prover, un modèle fermé et propriétaire. Autrement dit, dans le monde open-source, Leanstral 1.5 n'a pas de concurrent direct à ce niveau de performance.
Ces résultats illustrent une tendance de fond : la spécialisation d'un modèle sur un domaine précis peut permettre à une solution open-source de rivaliser — voire de dépasser — des géants aux paramètres bien plus nombreux, mais généralistes.
Au-delà des maths : détecter de vrais bugs dans du code réel
Le volet le plus intéressant pour les développeurs n'est peut-être pas les benchmarks académiques, mais bien l'application concrète à la vérification de code. Mistral indique que Leanstral 1.5, bien qu'entraîné principalement pour les mathématiques, obtient également de bonnes performances sur la vérification de programmes.
Dans un test pratique, le modèle a analysé 57 dépôts open-source et détecté cinq bugs jusqu'alors inconnus, dont un bug d'overflow dans la bibliothèque Rust varinteger. Ce type de résultat — trouver des régressions ou des erreurs logiques dans du vrai code de production — est bien plus parlant qu'un score sur un benchmark synthétique.
Pour un développeur PHP/Symfony, la question naturelle est : est-ce transposable à nos stacks ? Pas directement, puisque Leanstral 1.5 opère dans l'écosystème Lean 4 / Rust. Mais ce résultat ouvre la voie à une réflexion plus large : les LLMs spécialisés dans la vérification formelle pourraient, à terme, devenir un outil de revue de code de haute précision, complémentaire aux linters, analyseurs statiques (PHPStan, Psalm) et suites de tests.
Entraînement et disponibilité
Leanstral 1.5 a été entraîné via une combinaison de trois phases :
- Mid-training : ajustement de la base du modèle sur des données spécialisées.
- Supervised Fine-Tuning (SFT) : affinage supervisé sur des exemples annotés.
- Reinforcement Learning (RL) : apprentissage par renforcement pour optimiser les performances sur les tâches cibles.
Le modèle est disponible sur Hugging Face et accessible via une API gratuite. La licence Apache 2.0 permet une utilisation commerciale sans restriction, ce qui le rend exploitable dans un contexte professionnel sans friction juridique.
Ce que ça change pour la qualité logicielle
L'émergence de modèles comme Leanstral 1.5 s'inscrit dans une tendance plus large : l'automatisation du raisonnement formel. Là où les outils d'analyse statique détectent des patterns connus, un modèle de vérification formelle peut potentiellement raisonner sur des invariants, des conditions aux limites et des propriétés logiques complexes.
Pour les équipes qui travaillent sur des composants critiques — gestion de sessions, moteurs de calcul, parseurs, protocoles d'échange de données — cette catégorie d'outils mérite d'être suivie de près. Non pas pour remplacer les pratiques existantes, mais pour ajouter une couche de confiance supplémentaire là où les enjeux de fiabilité sont élevés.
Conclusion
Leanstral 1.5 est une démonstration convaincante de ce que peut accomplir un modèle open-source bien ciblé. En atteignant 100 % sur miniF2F, en dominant PutnamBench parmi les modèles ouverts et en détectant des bugs réels dans des projets existants, Mistral confirme que la spécialisation est une stratégie viable face aux modèles généralistes fermés.
Pour la communauté des développeurs, c'est aussi un signal : la vérification formelle, longtemps perçue comme un domaine élitiste et inaccessible, commence à se démocratiser. Les outils arrivent. À nous de commencer à les intégrer dans nos réflexions sur la qualité logicielle.
Source originale : The Decoder
