Leanstral : quand l’IA de code passe de la génération plausible à la preuve formelle 

Leanstral est le premier agent de code open-source pour Lean 4, un assistant de preuve formelle développé par Mistral AI. Contrairement aux modèles classiques qui génèrent du code comme du texte « plausible » à relire, Leanstral produit du code Lean accompagné de preuves formelles vérifiées par Lean lui-même. Lancé sous licence Apache 2.0, il est disponible en mode agent intégré à Mistral Vibe, via une API gratuite, ou en déploiement local (par exemple avec vLLM). Il bénéficie d’une fenêtre de contexte longue (jusqu’à 256 000 tokens) et accepte des entrées multimodales (texte+image) pour générer du texte. 

Les forces de Leanstral tiennent à son architecture Mixture-of-Experts (MoE) légère en calcul. Le modèle compte environ 119 milliards de paramètres, mais seul un sous-ensemble (~6,5 milliards) est activé en même temps. En pratique il utilise 128 experts, dont 4 seulement sont actifs simultanément. Il faut retenir que Leanstral est « optimisé pour les tâches de preuve » et qu’il intègre directement les outils Lean 4 (en particulier le protocole Lean-LSP MCP). Autrement dit, Leanstral n’est pas seulement bon en génération de texte, il est conçu pour s’insérer dans un environnement de développement formel, utilisant Lean comme vérificateur automatique à chaque étape. 

Du code « qui paraît correct » au code prouvé 

Les modèles de génération de code traditionnels se contentent souvent de produire une sortie « qui a l’air juste », ce qui exige ensuite une relecture humaine intense. Le véritable goulot d’étranglement reste donc la validation humaine du code produit. Leanstral propose de changer de paradigme : l’agent génère du code Lean accompagné de preuves formelles montrant sa correction. Si Lean valide ces preuves, la correction du code devient un fait mathématique, non plus un simple accord humain. Plus simplement, on passe de la confiance fondée sur le rendu (« le code est plausible ») à une confiance fondée sur la preuve (« le code est démontré correct »). 

Évaluation sur des scénarios réels (FLTEval) 

Pour évaluer Leanstral dans un contexte concret, Mistral a créé FLTEval, une suite d’outil d’évaluation centré sur des tâches réalistes de formalisation (par exemple les preuves du projet Fermat’s Last Theorem – FLT). Plutôt que des exercices abstraits, les modèles sont testés sur la vérification de chaque PR (pull request ou demande de modification) du dépôt FLT. 

Les résultats montrent que Leanstral devance largement les autres modèles, y compris certains très gros modèles open-source. Par exemple, sur FLTEval, Leanstral (pass@2) atteint un score de 26,3 pour un coût d’environ 36 $, contre 23,7 pour Claude Sonnet 4.6 à 549 $. Leanstral (pass@16) atteint 31,9 (avec 290 $), soit 8 points de plus que Sonnet. Même les modèles open-source géants peinent à rivaliser : par exemple Qwen-3.5-397B atteint 25,4 en 4 passes, alors que Leanstral fait 26,3 en 2 passes et 29,3 en 4 passes. 

En pratique, Leanstral offre donc une performance compétitive à une fraction du coût des modèles fermés de même nature.  Cet avantage de coût-efficacité tient au fait que Leanstral exploite Lean comme vérificateur parallèle : l’agent génère du code, Lean vérifie les preuves au fur et à mesure, et on ne dépense pas de ressources à faire tourner le code inutilement. 

Exemple concret : diagnostic de bug Lean 4 

Un cas d’usage illustratif mentionné par Mistral montre la force de Leanstral : face à un bug réel dans un code Lean 4 récent, l’agent n’a pas fait que de tester des solutions à l’aveugle, il a reproduit le contexte du test, identifié la cause du problème dans la logique de Lean, et proposé une correction précise. Cette approche « diagnostique » dépasse de loin la simple complétion de code : Leanstral agit comme un assistant de preuve expert qui raisonne dans le langage du formalisme, pas seulement comme un autocompléteur de code généraliste. 

Perspectives : vers du code AI « prouvable » 

Leanstral marque une étape importante dans l’évolution des assistants de code. Plutôt que de se contenter d’être convaincant (code qui compile et « semble correct »), l’IA permet désormais de démontrer formellement ce qu’elle propose. En pratique, cela ouvre la voie à des assistants capables non seulement d’écrire du code, mais de fournir un certificat de validation. Pour les domaines critiques (calcul formel, cryptographie, protocole de sécurité, etc.), cette garantie mathématique du code écrit pourrait accroître énormément la fiabilité. 

En résumé, au lieu de seulement générer et compter sur la bonne volonté du développeur pour la vérification, Leanstral déplace la confiance dans la machine de la simple apparence à la démonstration formelle. C’est un véritable changement de paradigme pour l’IA génératrice de code. 

Solutions de Transformation NumériqueMarc PLATINI Coordinateur scientifique IA