maciek905 - Fotolia

Actualites

Leanstral 1.5 : Mistral AI améliore son modèle de vérification de code

La startup aux 1 000 salariés optimise son modèle de preuve formelle et de vérification de l’exactitude du code. Le LLM open weight dérivé de Mistral Small 4 ferait mieux que ses compétiteurs directs tout en coûtant bien moins cher.

Gaétan Raoul
par
Publié le: 08 juil. 2026

Le 2 juillet, Mistral AI a présenté Leanstral 1.5, un modèle open weight consacré à la vérification programmatique, une pratique dérivée du Lean programming. Comme son prédécesseur, il est entraîné pour utiliser Lean 4, un langage et un assistant de preuve formelle mathématique. En clair, il peut vérifier l’exactitude du code généré ou toute autre application d’un théorème dans le cadre d’un projet d’ingénierie.

Leanstral 1.5 s’appuie à nouveau sur Mistral Small 4. Basé sur une architecture mixture of experts, il n’active à l’inférence que 6,5 milliards de ses 119 milliards de paramètres. Il dispose d’une fenêtre de contexte de 256 000 tokens et peut traiter du texte, ainsi que des images en entrée. Les améliorations principales sont à chercher du côté du pipeline d’entraînement en trois phases.

Leanstral 1.5 est ainsi passé par une étape de « mid-training », de fine-tuning supervisé et d’apprentissage par renforcement à l’aide de l’algorithme CISPO, imaginé par MiniMax.

Le « mid-training » est une étape située entre le pré-entraînement et le post-entraînement. Elle vise principalement à affiner la qualité des données, optimiser les traitements et étendre la fenêtre de contexte.

Ici, Mistral AI a sélectionné 6,5 milliards de tokens dédiés aux étapes de Lean, en sus de données en provenance d’agents d’IA, des instructions et des requêtes d’alignement. Ces « tokens lean contiennent des traces de LLM généralistes » qui ont tenté de démontrer des théorèmes ainsi que des problèmes et leur résolution issue de dépôts Git. En clair, la startup s’est fortement appuyée sur des données synthétiques. Lors du fine-tuning supervisé, 50 % des données d’entraînement provenaient d’un agent consacré à la vérification de la preuve du fonctionnement du code.

Maximiser l’usage de tokens « réflexifs » et (des données synthétiques)

L’algorithme CISPO, lui, vise à échantillonner les poids des modèles plutôt que les tokens utilisés lors d’optimisation des politiques. Habituellement, les autres algorithmes ont tendance à ne pas utiliser tous les tokens « réflexifs » à leur disposition. Plus rares que les tokens de raisonnement pur et ceux des réponses, ceux-là dénotent pourtant de la capacité d’un LLM à vérifier ses « brouillons » avant de les finaliser. Une capacité forcément utile pour un modèle dédiée à la preuve formelle.

Surtout, Mistral AI a utilisé deux environnements d’apprentissage par renforcement. L’un est un environnement multitour consacré à la vérification de théorèmes. L’autre est réservé à la programmation agentique.

Dans l’environnement multitour, « le modèle soumet une démonstration, reçoit les commentaires du compilateur Lean, puis affine son approche à chaque tentative », expliquent les porte-parole de Mistral AI, dans un billet de blog. « Si la démonstration est validée, l’itération est réussie ; dans le cas contraire, la boucle se poursuit jusqu’à ce que le modèle résolve le problème ou épuise son budget ».

Dans l’environnement de programmation, « Leanstral se comporte comme un développeur : il modifie des fichiers, exécute des commandes bash et utilise le serveur de langage Lean pour inspecter en temps réel les objectifs, les erreurs et les informations de type », poursuivent-ils. « Cela lui permet de s’attaquer à des tâches à long terme, telles que compléter des preuves partielles dans un référentiel, construire des lemmes auxiliaires et persister à travers plusieurs cycles de compactage de contexte ».

Lors de cette phase, Mistral AI a utilisé des jeux de données libres disponibles depuis des dépôts GitHub liés à Lean 4. Ensuite, les chercheurs de Mistral AI ont vérifié les résultats à l’aide d’un fork d’un script de Lean 4, SafeVerify.

Les performances de Leanstral premier du nom étaient comparées aux LLM de raisonnement « génériques ». Il y a désormais suffisamment de modèles spécialisés dans la preuve formelle et les benchmarks associés pour une comparaison équilibrée.

Leanstral 1.5, l’un des meilleurs de sa catégorie à un prix très doux, selon Mistral AI

Leanstral 1.5 a été évalué face à quatre parangonnages : miniF2F (problèmes élémentaires de niveau olympiades), PutnamBench (672 problèmes exigeant des chaînes de preuve complexe), Fate-H et Fate-X (algèbre abstraite de niveau master/doctorat), ainsi que FLTEval (ingénieur de preuves réelles issues du dépôt du dernier théorème de Fermat). FLTEval est un test open source concocté par Mistral AI.

Résultat, Leanstral 1.5 sature l’évaluation miniF2F, réussit 587 des 672 de PutnamBench et obtient un score de 87 sur 100 contre Fate-H, et 34 sur 100 problèmes face à Fate-X. Seul Aleph Prover, un modèle fourni par la startup américaine Logical Intelligence (soutenue par Yann Le Cun), fait mieux sur le test PutnamBench (668 problèmes résolus sur 672).

Soumis aux tests Fate-H et Fate-X, le modèle de Mistral AI serait devant Seed-prover 1,5 high de Bytedance (TikTok), Goedel-Architect (porté par une équipe de chercheurs de l’université de Princeton), AxProverBase d’Axiomatic AI et Seed-Prover 1.5 agentic only.

Leanstral 1.5 serait largement devant son prédécesseur (Leanstral 1.0), Kimi K2.5, Qwen 3.5 et GLM5 sur le banc d’essai FLTEval. Mieux, il obtient un score légèrement supérieur à Opus 4.6 « à un septième du coût », vante Mistral AI (216 contre 1650 dollars).

En plus de résoudre 587 des 672 exercices du PutnamBench, sept de plus que Seed-prover 1.5 high, Leanstreal 1.5 affiche une moyenne de 4 dollars par problème résolu… contre 300 dollars pour son concurrent chinois. Aleph Prover coûterait entre 54 et 68 dollars par problème.

Alors qu’il disposait en premier lieu d’un budget de 25 000 tokens, Leanstral 1.5 a tout de même consommé 4 millions de tokens pour finir ses 587 problèmes. Mistral AI assure toutefois qu’en matière de mise à l’échelle du test-time computing, son modèle est le meilleur du marché.  

« Les performances progressent de manière fluide et linéaire tout au long du processus, passant de 44 problèmes résolus à 50 000 tokens, jusqu’à 244 à 200 000 tokens, puis à 493 à 1 million de tokens et enfin à 587 à 4 millions de tokens », affirment les porte-parole. « Plutôt que d’abandonner lorsqu’une démonstration s’éternise, Leanstral continue de raisonner, de modifier des fichiers et de réviser son raisonnement sur des millions de tokens, transformant ainsi ce budget directement en problèmes résolus ».

Deux axes d’amélioration

Dans le détail, Mistral AI s’appuie sur la compression de la fenêtre de contexte, tous les 200 000 tokens. Le budget affiché ne reflète pas le volume de tokens dans la « mémoire » du LLM, mais seulement la quantité totale pour résoudre les problèmes.

Ce n’était pas une mince affaire. Les chercheurs expliquent que lors du fine-tuning supervisé, ils ont dû éliminer les traces agentiques comportant des erreurs, des arrêts prématurés et de fausses réussites tout en préservant le prompt original à côté de sa version compressée.

La startup française a également la capacité de son modèle à repérer des bugs dans des dépôts GitHub. Sur les 57 dépôts testés, Leanstreal 1.5 a signalé 47 bugs, dont 11 réels et 5 qui n’avaient jamais été signalés. Un pipeline incluant le modèle permettrait ainsi de compléter les outils de tests unitaires et de fuzzing.

Ce n’est pas parfait, conçoit le fournisseur de LLM. Les chercheurs anticipent deux axes de développement prioritaires. Premièrement, ils veulent développer un système multiagent (un décompose le problème, d’autres résolvent des sous-objectifs, un dernier réintègre les résultats) pour résoudre la latence. Deuxièmement, ils entendent améliorer la persistance afin d’éviter les abandons sur problèmes complexes. Cela passera par davantage de tokens de raisonnement mathématique, lors de l’entraînement et la récupération d’informations.

Le LLM est optimisé pour le volet IDE de Mistral Vibe, mais il est possible de l’installer en local depuis un serveur vLLM. Il faudra également utiliser un serveur MCP spécifique : Lean Theorem Prover MCP. Dans sa déclinaison FP4, Leanstral 1.5 pèse 60 Go, 119 Go en FP8 et 238 Go en FP16. Une grosse station de travail est nécessaire pour l’exécuter ou plusieurs GPU Nvidia H100 (80 Go de VRAM par unité).

Pour approfondir sur IA appliquée, GenAI, IA infusée