Mistral AI lance Leanstral 1.5, l'IA gratuite qui vérifie l'exactitude de votre code, un modèle d'agent de code Lean 4 open source capable de résoudre 587 des 672 problèmes du PutnamBench

Mistral AI lance Leanstral 1.5, l'IA gratuite qui vérifie l'exactitude de votre code, un modèle d'agent de code Lean 4 open source capable de résoudre 587 des 672 problèmes du PutnamBench

Mistral AI a lancé Leanstral 1.5. Il s’agit d’un modèle d’agent de code conçu pour Lean 4. Cette version est destinée à la démonstration automatisée de théorèmes et à l’ingénierie de la démonstration. Les poids sont disponibles sous licence Apache 2.0. L’architecture est de type « mixture-of-experts », ou MoE. Un modèle MoE achemine chaque token vers quelques sous-réseaux spécialisés. Cela permet de limiter la charge de calcul tout en conservant une grande capacité totale. Leanstral 1.5 résout 587 des 672 problèmes du PutnamBench et établit de nouveaux records de 87 % sur FATE-H et de 34 % sur FATE-X.

Mistral AI SAS est une entreprise française spécialisée dans l'intelligence artificielle (IA), dont le siège social est situé à Paris. Fondée en 2023, elle dispose de grands modèles de langage (LLM) à poids ouvert, comprenant à la fois des modèles d'IA open source et propriétaires. En 2025, la valorisation de l'entreprise s'élevait à plus de 14 milliards de dollars américains. Lean est un assistant de démonstration et un langage de programmation fonctionnel. Il repose sur le calcul des constructions avec des types inductifs. Il s’agit d’un projet logiciel libre et open source hébergé sur GitHub. Son développement est actuellement soutenu par l’organisation à but non lucratif Lean Focused Research Organization (FRO).

PutnamBench est un nouveau benchmark multilingue destiné à évaluer la capacité des démonstrateurs de théorèmes neuronaux à résoudre des problèmes mathématiques issus de concours. PutnamBench se compose de 1 724 formalisation de problèmes élaborées à la main, issues du concours mathématique William Lowell Putnam, le plus prestigieux concours de mathématiques de niveau licence en Amérique du Nord. On dénombre 672 problèmes formalisés en Lean 4, 640 en Isabelle et 412 en Coq.

La démonstration de ces théorèmes exige une grande capacité de résolution de problèmes et une maîtrise d’un large éventail de sujets enseignés dans les cours de mathématiques de premier cycle. PutnamBench est utilisé pour évaluer plusieurs démonstrateurs de théorèmes neuronaux et symboliques bien établis. Ces approches ne parviennent à résoudre qu’une poignée de problèmes de PutnamBench, ce qui fait de ce benchmark un défi ouvert et difficile pour la recherche sur la démonstration neuronale de théorèmes.

Récemment, Mistral AI a lancé Leanstral 1.5. Il s’agit d’un modèle d’agent de code conçu pour Lean 4. Cette version est destinée à la démonstration automatisée de théorèmes et à l’ingénierie de la démonstration. Les poids sont disponibles sous licence Apache 2.0. Un point de terminaison API gratuit, leanstral-1-5, est désormais accessible. Leanstral 1.5 actualise le modèle précédent, Leanstral-2603. Il appartient à la famille Mistral Small 4.

L’architecture est de type « mixture-of-experts », ou MoE. Un modèle MoE achemine chaque token vers quelques sous-réseaux spécialisés. Cela permet de limiter la charge de calcul tout en conservant une grande capacité totale. Leanstral utilise 128 experts, dont 4 sont actifs par token. La taille totale est de 119 milliards de paramètres, dont 6,5 milliards sont activés par token. La longueur du contexte est de 256 000 tokens. L’entrée est multimodale, acceptant du texte et des images. La sortie est uniquement textuelle.


Voici l'annonce de Mistral AI :

Leanstral 1.5 : l’abondance des preuves pour tous

Depuis son lancement, Leanstral propose une approche ouverte et pratique de l’ingénierie des preuves dans Lean 4. Aujourd’hui, nous lançons Leanstral 1.5, un modèle gratuit sous licence Apache 2.0 comptant 119 milliards de paramètres au total et seulement 6 milliards de paramètres actifs, offrant ainsi une amélioration des performances qui rend la vérification formelle plus puissante et plus accessible que jamais.

Leanstral 1.5 atteint la saturation de miniF2F, résout 587 des 672 problèmes du PutnamBench et établit de nouveaux records de 87 % sur FATE-H et de 34 % sur FATE-X. Au-delà des benchmarks, il vérifie des propriétés de code complexes et détecte des bogues jusque-là inconnus dans des dépôts open source, prouvant ainsi que des méthodes formelles rigoureuses peuvent être à la fois efficaces et pratiques pour une utilisation en conditions réelles.


Entraînement de Leanstral

Leanstral 1.5 suit un processus en trois étapes : entraînement intermédiaire, affinage supervisé et apprentissage par renforcement avec CISPO. Leanstral 1.5 s’appuie sur un entraînement approfondi dans deux environnements d’apprentissage par renforcement :

Dans l’environnement « multiturn », le modèle reçoit l’énoncé d’un théorème et doit soit le prouver, soit le réfuter. Le modèle soumet une preuve, reçoit le retour du compilateur Lean et affine son approche à chaque tentative. Si la preuve est compilée, il réussit ; sinon, la boucle se poursuit jusqu’à ce que le modèle résolve le problème ou épuise son budget.


Dans l’environnement « code agent », Leanstral fonctionne comme un développeur dans un système de fichiers brut : il modifie des fichiers, exécute des commandes bash et utilise le serveur de langage Lean pour inspecter les objectifs, les erreurs et les informations de type en temps réel. 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. Le modèle apprend à naviguer dans l’ensemble du flux de travail d’ingénierie de la démonstration et est finalement vérifié par notre fork de SafeVerify afin de garantir son exactitude pour une liste de théorèmes cibles.


Évaluation

Nous évaluons Leanstral sur les benchmarks suivants :

- miniF2F est un benchmark intersystème pour les mathématiques formelles, allant de problèmes élémentaires à des défis de niveau IMO, testant diverses capacités de démonstration en algèbre, combinatoire et théorie des nombres.

- PutnamBench se compose de 672 problèmes issus du concours mathématique Putnam, nécessitant un raisonnement approfondi et de longues chaînes de démonstration pour résoudre des problèmes mathématiques complexes.

- FATE-H et FATE-X sont des benchmarks d’algèbre abstraite destinés respectivement à des problèmes de niveau master et doctorat, testant le raisonnement avancé dans des domaines tels que la théorie des groupes, la théorie des anneaux et la théorie des modules.

- FLTEval s’appuie sur de véritables pull requests issues du dépôt « Fermat’s Last Theorem » et évalue l’ingénierie pratique de la démonstration face à une complexité réelle.

Nous saturons complètement miniF2F, atteignant 100 % tant sur l’ensemble de validation que sur l’ensemble de test. Sur PutnamBench et FATE-H/X, nous comparons Leanstral 1.5 à Goedel-Architect sans guidage en langage naturel, à Seed-Prover 1.5 dans sa configuration la plus élevée, et à AxProverBase. Leanstral établit un nouveau record sur FATE-H/X, en résolvant respectivement 87 et 34 problèmes. Sur PutnamBench, il devance Seed-Prover 1.5 en configuration haute de 7 problèmes, à un coût bien inférieur : environ 4 $ par problème, contre une estimation de 300 $ ou plus pour Seed-Prover, dont la configuration haute fonctionne avec un budget de 10 jours H20 par problème. Les seuls démonstrateurs mieux classés fonctionnent dans des conditions différentes : certains bénéficient de conseils de démonstration en langage naturel, d’autres ont un coût d’exécution bien plus élevé, comme Aleph Prover, qui coûte entre 54 et 68 dollars par problème.

Leanstral 1.5 présente la meilleure évolutivité en temps de test que nous ayons observée chez un modèle de raisonnement formel. Le graphique ci-dessous suit l’évolution de Pass@8 sur PutnamBench à mesure que nous augmentons le budget de tokens par tentative de 25 000 à 4 millions : les performances progressent de manière fluide et monotone tout au long du parcours, passant de 44 problèmes résolus à 50 000 tokens à 244 à 200 000, puis à 493 à 1 million et enfin à 587 à 4 millions. Plutôt que d’abandonner lorsqu’une preuve s’éternise, Leanstral continue de raisonner, de modifier des fichiers et de réviser sur des millions de tokens, transformant directement ce budget en problèmes résolus — le même comportement que celui à l’origine de la preuve de l’arbre AVL ci-dessous, qui a nécessité plus de 2,7 millions de tokens répartis sur 22 compactages.


Avec cette version, nous rendons également FLTEval entièrement open source. Leanstral 1.5 fait passer le taux de réussite « pass@1 » sur le benchmark de 21,9 à 28,9 et le taux de réussite « pass@8 » de 31,9 à 43,2, surpassant ainsi le score de 39,6 d’Opus 4.6 pour un coût sept fois moindre. Il creuse également son avance sur des modèles open source 3 à 10 fois plus volumineux, comme le montre la figure ci-dessous.


Études de cas sur la vérification de code

Bien qu’il ait été principalement entraîné pour les mathématiques, Leanstral 1.5 fait preuve de solides capacités en matière de vérification de code. Nous présentons deux études de cas critiques pour démontrer son impact.

- Arbres AVL : démonstration de la complexité temporelle

Les arbres AVL sont des arbres de recherche binaires auto-équilibrés qui maintiennent une hauteur de O(log n) grâce à un rééquilibrage lors des insertions et des suppressions. Leanstral 1.5 a démontré ces garanties de complexité temporelle pour une implémentation réelle — une tâche qui a nécessité une induction structurelle pour refléter la structure récursive de l’arbre, une gestion minutieuse du suivi temporel monadique et une analyse exhaustive des cas pour les chemins de rééquilibrage. Sur plus de 2,7 millions de tokens et 22 compactages, Leanstral a systématiquement déplié chaque couche de la monade TimeM, mettant à nu les calculs sous-jacents malgré leur entrelacement avec le flux de contrôle. Il a établi une borne quasi-serrée de 48 étapes par unité de hauteur plus une constante pour l’insertion, puis a relié la hauteur à la taille de l’arbre via une relation logarithmique, fournissant ainsi des preuves complètes et vérifiées que l’insertion et la suppression sont bien de complexité O(log n).

- Détection de bogues : repérer les failles cachées

Pour tester les capacités de détection de bogues de Leanstral, nous avons mis en place un pipeline automatisé : Aeneas traduit le code Rust en Lean, tandis que Leanstral déduit l’intention de l’utilisateur et génère des propriétés de correction à partir du code. Leanstral tente ensuite de prouver chaque propriété en quatre essais. Si tous échouent, il tente de prouver la négation à la place, également en quatre essais. Sur les 57 dépôts testés, ce processus a signalé 47 propriétés violées, dont 11 indiquaient des bogues réels — 5 d’entre eux n’avaient jamais été signalés auparavant sur GitHub.

L’un de ces bogues se trouvait dans la fonction « sign » pour le décodage en zigzag de la bibliothèque datrs/varinteger. Avec une entrée Std.U64.MAX, l’expression (valeur + 1) provoquait un débordement, entraînant des plantages en mode débogage et une corruption silencieuse en mode production — un cas limite que les tests et le fuzzing auraient généralement manqué. Le pipeline de Leanstral l’a détecté automatiquement, démontrant ainsi que la vérification formelle peut déjà être appliquée à des bases de code réelles et détecter des bogues que certaines méthodes traditionnelles négligent.

Sources : Annonce Leanstral 1.5, Présentation PutnamBench

Et vous ?

Pensez-vous que cette annonce est crédible ou pertinente ?
Quel est votre avis sur le sujet ?

Voir aussi :

La start-up française Mistral AI lance Mistral Small 4, un modèle d'IA open source qui combine raisonnement, programmation et IA multimodale, pour offrir un outil unique et adaptable

Le grand modèle de langage MoE LongCat-2.0 s'affranchit de Nvidia en étant entraîné exclusivement avec des puces chinoises, un modèle de 1 600 milliards de paramètres, le moteur de calcul derrière "Owl Alpha"

Le nouveau modèle GLM-5.2 de Z.ai devient la référence sur le marché des IA open source. Il surpasse GPT-5.5 d'OpenAI sur plusieurs benchmarks de codage à long terme, pour un coût six fois moindre