Leanstral : fondation open source pour un vibe coding fiable

Les agents d’IA se sont imposés comme des outils très capables pour la génération de code. Pourtant, à mesure que nous poussons ces modèles vers des domaines à forts enjeux, des mathématiques de recherche de pointe aux logiciels critiques, nous rencontrons un goulot d’étranglement à l’échelle : la relecture humaine. Le temps et l’expertise spécialisée nécessaires à la vérification manuelle deviennent le principal frein à la vitesse d’ingénierie.

Nous imaginons une génération plus utile d’agents de code, capables à la fois d’exécuter leurs tâches et de prouver formellement leurs implémentations au regard de spécifications strictes. Au lieu de déboguer une logique générée par une machine, les humains définissent ce qu’ils veulent. Aujourd’hui, nous franchissons une première étape importante vers cette vision.

Présentation de Leanstral

Nous publions Leanstral, le premier agent de code open source conçu pour Lean 4. Lean 4 est un assistant de preuve capable d’exprimer des objets mathématiques complexes comme les espaces perfectoïdes et des spécifications logicielles comme les propriétés de fragments Rust. Contrairement aux systèmes de preuve existants, qui servent d’enveloppes autour de grands modèles généralistes ou se concentrent sur des problèmes mathématiques isolés, Leanstral est conçu pour être très efficace, avec 6B paramètres actifs, et entraîné pour travailler dans des dépôts formels réalistes.

• Ouvert et accessible : nous publions les poids de Leanstral sous licence Apache 2.0, dans un mode agent au sein de Mistral Vibe, et via un endpoint API gratuit. Nous publierons également un rapport technique détaillant notre approche d’entraînement, ainsi qu’une nouvelle suite d’évaluation, FLTEval, pour déplacer les évaluations au-delà de leur focalisation sur les mathématiques de compétition.

• Efficace et puissant : nous utilisons une architecture très sparse pour Leanstral et l’optimisons pour les tâches d’ingénierie de preuve. En utilisant l’inférence parallèle avec Lean comme vérificateur parfait, Leanstral offre de bonnes performances et un bon rapport coût-efficacité face aux concurrents propriétaires existants.

• Extensible via MCP : Leanstral prend en charge des MCP arbitraires via Vibe et a été spécifiquement entraîné pour atteindre des performances maximales avec lean-lsp-mcp, souvent utilisé. 

Évaluation

Pour refléter l’utilité dans des scénarios réalistes d’ingénierie de preuve, nous évaluons Leanstral sur la complétion de toutes les preuves formelles et la définition correcte de nouveaux concepts mathématiques dans chaque PR du Projet FLT, plutôt que sur des problèmes mathématiques isolés. Nous comparons Leanstral aux principaux agents de code (Claude Opus 4.6, Sonnet 4.6, Haiku 4.5) et à des modèles open source (Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B).

Leanstral ou modèles OSS

Leanstral-120B-A6B démontre un avantage d’efficacité significatif par rapport à ses pairs open source beaucoup plus grands. Alors que des modèles comme GLM5-744B-A40B et Kimi-K2.5-1T-32B peinent à passer à l’échelle, avec des scores FLTEval plafonnant respectivement autour de 16,6 et 20,1, Leanstral les dépasse tous deux avec un seul passage.

Même Qwen3.5-397B-A17B, le concurrent OSS le plus solide présenté ici, nécessite 4 passages pour atteindre un score de 25,4. À l’inverse, Leanstral atteint un score supérieur de 26,3 avec la moitié de cet investissement (pass@2) et continue de passer à l’échelle de façon linéaire, jusqu’à 29,3 au même niveau de coût.

Leanstral ou famille Claude

Leanstral sert d’alternative à forte valeur à la suite Claude, avec des performances compétitives pour une fraction du prix : Leanstral pass@2 atteint un score de 26,3, soit 2,6 points de plus que Sonnet, pour un coût d’exécution de seulement 36 $, contre 549 $ pour Sonnet. À pass@16, Leanstral atteint un score de 31,9 et dépasse nettement Sonnet de 8 points. Claude Opus 4.6 reste en tête sur la qualité, mais son coût est très élevé : 1 650 $, soit 92 fois plus que l’exécution de Leanstral.

Dans notre benchmark, nous avons utilisé Mistral Vibe comme scaffold, sans modification spécifique pour l’évaluation.

Études de cas

Répondre à des posts Stack Exchange sur les changements dans la dernière version de Lean

Lorsque des changements incompatibles arrivent dans une nouvelle version de Lean, migrer du code peut devenir très pénible. Nous avons donné à Leanstral une question réelle issue de Proof Assistants Stack Exchange à propos d’un script qui avait mystérieusement cessé de compiler dans Lean 4.29.0-rc6, une version trop récente pour faire partie de notre entraînement. Le problème venait d’une tactique de réécriture (rw) qui échouait soudainement à faire correspondre des motifs impliquant un simple alias de type, initialement écrit def T2 := List Bool.

Au lieu d’avancer à l’aveugle, Leanstral a analysé le problème. Il a réussi à construire du code de test pour recréer l’environnement en échec et a diagnostiqué le problème sous-jacent lié à l’égalité définitionnelle. Le modèle a correctement identifié que, comme def crée une définition rigide nécessitant un dépliage explicite, elle bloquait la tactique rw et l’empêchait de voir la structure sous-jacente nécessaire à la correspondance.

La correction proposée était simple : remplacer def par abbrev. Comme abbrev crée un alias transparent immédiatement égal définitionnellement au type d’origine, la tactique rw pouvait de nouveau faire correspondre correctement le motif (L2 n).length dans la preuve. Leanstral termine la tâche et explique parfaitement le raisonnement à l’utilisateur. 

Raisonner sur des programmes

Nous avons copié des définitions Rocq depuis https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html et demandé à Leanstral de les convertir vers Lean. Il y est parvenu, en implémentant même une notation personnalisée. Exemple d’extrait :

inductive ceval : com → state → state → Prop where
 | E_Skip (st : state) : ceval .CSkip st st
 | E_Ass (st : state) (a1 : aexp) (n : Nat) (l : ident) (h : aeval a1 st = n) :
     ceval (.CAss l a1) st (update st l n)
 | E_Seq (c1 c2 : com) (st st' st'' : state) (h1 : ceval c1 st st') (h2 : ceval c2 st' st'') :
     ceval (.CSeq c1 c2) st st''
 | E_IfTrue (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = true) (h1 : ceval c1 st st') :
     ceval (.CIf b1 c1 c2) st st'
 | E_IfFalse (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = false) (h1 : ceval c2 st st') :
     ceval (.CIf b1 c1 c2) st st'
 | E_WhileEnd (b1 : bexp) (st : state) (c1 : com) (h : beval b1 st = false) :
     ceval (.CWhile b1 c1) st st
 | E_WhileLoop (st st' st'' : state) (b1 : bexp) (c1 : com) (h1 : beval b1 st = true) (h2 : ceval c1 st st') (h3 : ceval (.CWhile b1 c1) st' st'') :
     ceval (.CWhile b1 c1) st st''


-- Notation for command evaluation
notation:50 c " / " st " ⇒ " st' => ceval c st st'

Il pouvait aussi traduire vers Lean, puis prouver certaines propriétés de programmes dans ce langage, à partir du seul énoncé Rocq, sans preuve :

-- Example command: adds 2 to variable X
def plus2 : com := .CAss "X" (.APlus (.AId "X") (.ANum 2))


-- Theorem: The plus2 command correctly adds 2 to variable X
-- Intuition: If X has value n in the initial state, after executing plus2,
-- X will have value n+2 in the final state
-- This specifies the behavior of the plus2 command
theorem plus2_spec (st : state) (n : Nat) (st' : state) (h1 : st "X" = n) (h2 : plus2 / st ⇒ st') :
 st' "X" = n + 2 := by
 -- plus2 is defined as .CAss "X" (.APlus (.AId "X") (.ANum 2))
 -- Use equation compiler to unfold it
 change ceval (.CAss "X" (.APlus (.AId "X") (.ANum 2))) st st' at h2
 cases h2 with
 | E_Ass _ _ n l h =>
   have : aeval (.APlus (.AId "X") (.ANum 2)) st = n := h
   simp only [aeval] at this
   rw [update]
   simp [← this, h1]

Exigez des preuves. Essayez Leanstral dès aujourd’hui.

Leanstral est disponible dès aujourd’hui pour tous.

• Aucune configuration dans Mistral Vibe : nous avons intégré Leanstral directement dans Mistral Vibe pour permettre le vibe coding et la preuve immédiatement, sans configuration. Utilisez /leanstall pour l’activer. Ensuite, pour utiliser Leanstral, appuyez sur Shift+Tab jusqu’à ce que le modèle affiché soit Leanstral. Vous pouvez aussi utiliser vibe --agent lean.

• Labs API : accédez au modèle via notre endpoint API gratuit ou quasi gratuit labs-leanstral-2603. Nous maintenons cet endpoint très accessible pendant une période limitée afin de recueillir des retours réalistes et des données d’observabilité pour alimenter la prochaine génération de modèles de code vérifié.

• Poids disponibles : téléchargez le modèle sous licence Apache 2.0 et exécutez-le sur votre propre infrastructure.

Documentation - S’inscrire à Mistral Vibe