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...
La fin de cet article est réservée aux abonnés. Soutenez le Club Developpez.com en prenant un abonnement pour que nous puissions continuer à vous proposer des publications.
