Leanstral 1.5 de Mistral AI change la manière d’aborder le code et les mathématiques formelles. Pensé pour Lean 4, cet agent open source ne se contente pas de proposer une réponse plausible, il cherche à prouver chaque étape logique avec rigueur. Pour les équipes techniques, les chercheurs et les entreprises, cela ouvre une nouvelle façon de vérifier du code, de formaliser des raisonnements et de détecter des erreurs subtiles.
En quelques lignes :
Leanstral 1.5 rend la vérification formelle opérationnelle pour Lean 4, en offrant des preuves rigoureuses, des performances élevées et un coût d’usage faible pour automatiser la validation de code et de démonstrations.
- Priorisez les cas où la preuve formelle apporte une vraie valeur (sécurité logicielle, propriétés algorithmiques, validations mathématiques), plutôt que la génération d’applications classiques.
- Profitez de la licence Apache-2.0 et des poids mistralai/Leanstral-1.5-119B-A6B pour expérimenter librement; testez d’abord l’endpoint API gratuit, puis migrez local via vLLM si vous devez garder le contrôle des données.
- Organisez vos entrées pour le contexte long (fenêtre de contexte de 256 000 tokens, attention pratique au seuil d’environ 200 000 tokens) : segmentez les gros corpus pour maintenir la précision des preuves.
- Surveillez le coût et le retour sur investissement : coût moyen PutnamBench ~4 dollars par problème, ce qui rend rentable l’automatisation de vérifications répétées par rapport aux outils plus coûteux.
- Intégrez Leanstral 1.5 dans vos pipelines (revues de code, CI) pour transformer les alertes en preuves exploitables, et utilisez ses sorties pour prioriser corrections et audits approfondis.
Qu’est-ce que Leanstral 1.5 de Mistral AI ?
Leanstral 1.5 est un agent IA open source spécialisé dans la vérification formelle de code, conçu pour le langage Lean 4. Il s’inscrit dans une logique très différente des modèles génératifs classiques, car son objectif n’est pas seulement de produire du texte ou du code, mais de garantir la validité d’une démonstration ou d’un raisonnement.
Le modèle fonctionne sous licence Apache-2.0, ce qui autorise une utilisation libre, y compris commerciale, sans contraintes juridiques lourdes. Avec ses 119 milliards de paramètres, son architecture Mixture of Experts n’en active que 6,5 milliards à l’inférence, ce qui améliore le compromis entre puissance et efficacité.
Leanstral 1.5 repose sur la famille Mistral Small 4 et succède à Leanstral-2603. Il marque surtout un tournant important, celui du passage de la génération de code “plausible” à la production de preuves formelles vérifiées. C’est un changement de nature, pas seulement de niveau.
Avec sa fenêtre de contexte de 256 000 tokens, le modèle peut traiter de longs contenus et, selon les usages décrits par Mistral, combiner texte et images dans une même requête. Cela le rend adapté à des environnements où la quantité d’informations à analyser est importante, notamment en mathématiques, en programmation et en documentation technique.
Des performances très solides sur les benchmarks
Les résultats observés sur les benchmarks montrent que Leanstral 1.5 n’est pas un simple prototype. Il s’impose comme un modèle capable de résoudre des problèmes complexes avec un très haut niveau de fiabilité. Cette montée en puissance intéresse autant les chercheurs que les entreprises à la recherche d’outils de vérification plus automatisés.
Résultats mathématiques et informatiques
Sur miniF2F, Leanstral 1.5 atteint 100 % de réussite sur les jeux de validation et de test. Ce score indique une excellente maîtrise des exercices formels de base et montre que le modèle sait suivre des chaînes de preuve avec cohérence.
Sur PutnamBench, benchmark composé de problèmes de mathématiques avancées, il résout 587 problèmes sur 672. Ce résultat le place très au-dessus du précédent record open source, souvent situé autour d’une cinquantaine de problèmes. Le seul modèle propriétaire qui le dépasse est Aleph Prover, avec 668 problèmes résolus.
Du côté de FATE, qui évalue des problèmes d’algèbre abstraite, Leanstral 1.5 obtient 87 % au niveau master, appelé FATE-H, et 34 % au niveau doctorat, FATE-X. Sur FLTEval, ses scores progressent aussi nettement, avec un pass@1 qui passe de 21,9 % à 28,9 % et un pass@8 qui grimpe de 31,9 % à 43,2 %.
Le tableau ci-dessous résume quelques indicateurs clés.
| Benchmark | Résultat de Leanstral 1.5 | Lecture du score |
|---|---|---|
| miniF2F | 100 % | Maîtrise complète sur validation et test |
| PutnamBench | 587 sur 672 | Très haut niveau sur les mathématiques avancées |
| FATE-H | 87 % | Fort niveau en algèbre abstraite master |
| FATE-X | 34 % | Bon résultat sur des problèmes doctoraux |
| FLTEval pass@1 | 28,9 % | Amélioration nette du premier essai réussi |
| FLTEval pass@8 | 43,2 % | Meilleure robustesse sur plusieurs tentatives |
Au-delà des scores bruts, ce qui frappe surtout, c’est le positionnement du modèle. Il ne vise pas uniquement la génération rapide, mais la validation formelle dans des contextes où l’exactitude compte davantage que la vitesse de production de texte. Cette orientation le distingue nettement des assistants généralistes.
Une efficacité économique remarquée
Leanstral 1.5 se distingue aussi par son coût d’usage. Le coût moyen pour résoudre un problème PutnamBench est d’environ 4 dollars. À titre de comparaison, Seed-Prover 1.5 dépasse les 300 dollars, et Aleph Prover se situe entre 54 et 68 dollars.
Cette différence change la donne pour les équipes qui veulent explorer la preuve formelle à grande échelle. Quand le coût par problème baisse fortement, il devient plus réaliste de tester davantage de cas, d’automatiser des vérifications répétitives et d’intégrer ces analyses dans des flux de travail industriels ou académiques.
En pratique, cela signifie que la vérification formelle peut sortir d’un usage réservé à quelques projets d’élite. Avec un niveau de performance élevé et un coût contenu, Leanstral 1.5 rend possible une adoption plus large, notamment dans les organisations qui cherchent un bon équilibre entre qualité de preuve et budget.
Leanstral 1.5 appliqué au code : quels cas d’usage ?
Si le modèle a été conçu pour la preuve formelle, ses capacités dépassent le cadre purement théorique. Il peut aussi analyser du code source, repérer des incohérences et mettre en évidence des défauts que des revues classiques laissent parfois passer. C’est là que son intérêt devient très concret pour la sécurité logicielle.
On trouve des cas d’usage concrets pour les PME et les équipes qui souhaitent intégrer l’IA dans leurs processus de sécurité et de développement.
Détection de bugs et analyse statique
Leanstral 1.5 a été testé sur 57 bases de code open source. Dans cet environnement, il a identifié 47 propriétés non conformes. Parmi ces alertes, 11 défauts réels ont été confirmés, dont 5 bugs jamais signalés publiquement auparavant.
Un cas cité concerne un bug d’overflow dans la bibliothèque Rust varinteger. Ce type de détection montre que le modèle peut repérer des erreurs discrètes, parfois invisibles lors d’un audit rapide. Il agit alors comme un analyste statique capable de lire le code ligne par ligne, de trouver les ruptures logiques et de proposer une correction fondée sur un raisonnement formel.
Dans ce rôle, il peut compléter ou remplacer une partie de la shortlist de points suspects habituellement produite par des équipes de sécurité ou des outils SAST pour Static Application Security Testing. L’intérêt n’est pas seulement de signaler un problème, mais d’aider à comprendre pourquoi la logique casse et comment la démonstration peut être réparée.
Un usage orienté preuve plutôt que génération applicative
Il faut bien comprendre le positionnement de Leanstral 1.5. Ce modèle n’est pas pensé pour écrire une interface web, un site vitrine ou une application métier complète. Son terrain de jeu, c’est la vérification logique, la formalisation mathématique et la détection de bugs subtils.
Autrement dit, si vous cherchez un assistant pour prototyper rapidement une application classique, vous serez en dehors de son domaine de force. En revanche, si votre objectif est d’obtenir une preuve rigoureuse, de valider une propriété de code ou de tester une hypothèse mathématique, Leanstral 1.5 a une vraie valeur ajoutée.
Comment accéder à Leanstral 1.5 et l’utiliser
L’accès au modèle a été pensé pour être simple. Les poids sont disponibles gratuitement sous le nom mistralai/Leanstral-1.5-119B-A6B, ce qui permet de l’examiner, de le déployer ou de l’intégrer à des pipelines spécialisés.
Mistral propose aussi un endpoint API gratuit pour exécuter le modèle sans installation locale. Cette option intéressera les équipes qui veulent tester rapidement les performances ou éviter la complexité d’un déploiement lourd sur leur propre infrastructure.
Pour un usage privé, l’installation locale reste possible, notamment via vLLM. Cette solution convient aux organisations qui veulent garder le contrôle sur les données, les environnements d’exécution et les paramètres de calcul.
La licence Apache-2.0 facilite l’intégration dans des contextes académiques comme commerciaux. C’est un avantage non négligeable pour les entreprises qui souhaitent expérimenter la preuve formelle sans se heurter à des barrières juridiques trop restrictives.
Bonnes pratiques et erreurs à éviter avec Leanstral 1.5
Pour bien utiliser Leanstral 1.5, il faut partir de son point fort : la preuve formelle. Le modèle excelle lorsqu’il s’agit de vérifier une démonstration, d’analyser une propriété de code ou de raisonner sur une structure mathématique. C’est dans ces scénarios qu’il apporte le plus de valeur.
À l’inverse, il ne faut pas le détourner de son objectif pour lui demander de générer du code applicatif généraliste. Une interface utilisateur, une application mobile ou un back-end complet ne relèvent pas de son usage naturel. Son efficacité baisse dès qu’on l’éloigne de la logique formelle.
Une autre limite à garder en tête concerne la gestion du contexte. Le modèle doit compresser sa fenêtre tous les 200 000 tokens, ce qui peut réduire la précision lors de l’analyse de documents très longs. Pour des corpus massifs, il vaut donc mieux segmenter les entrées et organiser les requêtes avec méthode.
Malgré cette contrainte, le niveau atteint par Leanstral 1.5 est suffisamment élevé pour être jugé utilisable dans de vrais cas d’usage industriels et scientifiques. C’est ce qui explique l’intérêt croissant autour de la preuve formelle assistée par IA, un domaine longtemps resté confidentiel.
Son ouverture en source libre participe aussi à une forme de démocratisation. Des pratiques autrefois réservées à des structures spécialisées deviennent plus accessibles, avec des coûts plus faibles et une diffusion plus large des méthodes de vérification.
Au final, Leanstral 1.5 s’impose comme un modèle de référence pour la preuve formelle assistée par IA, à la fois performant, accessible et orienté résultats vérifiables. Pour qui travaille sur Lean 4, la sécurité logicielle ou les démonstrations mathématiques, il ouvre un terrain d’expérimentation particulièrement intéressant.
