Leanstral : l’agent open source pour l’ingénierie de code fiable et des preuves formelles

(mistral.ai)

1 points par GN⁺ 2026-03-17 | Aucun commentaire pour le moment. | Partager sur WhatsApp

Premier agent de code open source conçu pour Lean 4, avec pour objectif d’automatiser les preuves formelles (formal proof) afin de réduire la charge de vérification humaine
Les poids du modèle sont publiés sous licence Apache 2.0, et l’outil est immédiatement utilisable via l’environnement Mistral Vibe et un endpoint API gratuit
Il s’appuie sur une architecture sparse de 6B paramètres actifs pour améliorer l’efficacité et réduire les coûts, tout en prenant en charge les intégrations MCP comme lean-lsp-mcp
Sur le benchmark FLTEval, il obtient de meilleurs scores que de grands modèles open source comme Qwen3.5, GLM5 et Kimi-K2.5, avec des performances comparables à Claude Sonnet pour un coût plus de 15 fois inférieur
Cette nouvelle approche combine automatisation des preuves formelles et amélioration de la fiabilité du code, avec un potentiel d’usage aussi bien en mathématiques de recherche que pour le développement de logiciels critiques

Présentation de Leanstral

Leanstral est le premier agent de code open source pour Lean 4, fonctionnant dans un environnement d’assistant de preuve (proof assistant)
- Lean 4 permet de représenter des objets mathématiques complexes (par ex. les espaces perfectoids) ainsi que des spécifications logicielles
- Contrairement aux systèmes de preuve existants, souvent centrés sur des wrappers de modèles génériques ou sur des problèmes isolés, Leanstral a été entraîné pour fonctionner efficacement sur des dépôts formels réalistes (formal repositories)
Il adopte une architecture sparse avec 6B paramètres actifs, combinant inférence parallèle (parallel inference) et capacités de vérification de Lean
La prise en charge des intégrations MCP le rend compatible avec des protocoles courants comme lean-lsp-mcp

Les poids du modèle sont publiés sous licence Apache 2.0, et l’agent est proposé en mode agent dans Mistral Vibe
Tout le monde peut y accéder via l’endpoint API gratuit (labs-leanstral-2603), et les retours utilisateurs serviront à améliorer les prochains modèles
Un rapport technique et l’outil d’évaluation FLTEval sont publiés en parallèle afin de mesurer les performances réelles en ingénierie des preuves, au-delà des évaluations existantes centrées sur les mathématiques

L’évaluation se fonde sur la capacité à finaliser, au niveau des Pull Requests du projet FLT, l’ensemble des preuves formelles ainsi que la définition de nouveaux concepts mathématiques
Modèles comparés : Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B

Leanstral-120B-A6B atteint 26,3 points (pass@2), devant GLM5 (16,6 points) et Kimi-K2.5 (20,1 points)
Alors que Qwen3.5 obtient 25,4 points en 4 exécutions (pass@4), Leanstral fait mieux avec deux fois moins d’exécutions
À coût équivalent, les performances montent linéairement jusqu’à 29,3 points (pass@4)

Il affiche une avance de 2,6 points sur Sonnet (26,3 points vs 23,7 points), pour un coût d’exécution de 36 $ vs 549 $, soit plus de 15 fois moins cher
En pass@16, il atteint 31,9 points, soit 8 points de plus que Sonnet
Le meilleur score revient à Claude Opus 4.6 avec 39,6 points, mais pour un coût de 1 650 $, soit 92 fois celui de Leanstral
Tous les benchmarks ont été exécutés dans l’environnement Mistral Vibe sans modification

Entrée d’une question StackExchange portant sur une erreur liée à un alias de type apparue dans Lean 4.29.0-rc6
Leanstral a reproduit l’environnement du problème et diagnostiqué avec précision un problème d’égalité définitionnelle (definitional equality)
Il a proposé d’utiliser abbrev à la place de def, rétablissant ainsi le bon fonctionnement de la tactique rw
Il a aussi expliqué clairement à l’utilisateur la cause du problème et la raison de la solution

Conversion d’une définition de programme en Rocq vers Lean, avec implémentation d’une notation personnalisée
Exemple : démontrer que la commande plus2 ajoute bien 2 à la variable X
À partir de la seule spécification Rocq fournie, Leanstral a complété et prouvé le théorème (theorem) dans Lean

Intégration Mistral Vibe : disponible immédiatement avec la commande /leanstall
Labs API : accès gratuit ou à faible coût
Téléchargement du modèle : exécutable directement sous licence Apache 2.0

Leanstral constitue la première tentative open source de combiner génération de code et automatisation des preuves formelles
Il ouvre des perspectives d’usage en mathématiques de recherche, développement logiciel vérifiable et conception de systèmes à haute fiabilité
Il est présenté comme une nouvelle infrastructure de vérification de code alliant efficacité économique et ouverture