Mistral AI publie Leanstral 1.5 : un modèle agent de code Lean 4 sous licence Apache 2.0, qui résout 587 des 672 problèmes du PutnamBench
Mistral AI a dévoilé Leanstral 1.5, un modèle de type "code agent" spécialisé dans la démonstration automatique de théorèmes avec l'assistant de preuve Lean 4. Ce modèle met à jour la précédente version Leanstral-2603 et appartient à la famille Mistral Small 4. Les poids sont publiés en licence ouverte Apache 2.0, et un point d'accès API gratuit, baptisé leanstral-1-5, est désormais disponible. Sur le plan technique, Leanstral 1.5 repose sur une architecture de mélange d'experts (MoE) comptant 128 experts dont 4 activés par token, pour un total de 119 milliards de paramètres dont 6,5 milliards effectivement mobilisés à chaque inférence. Le modèle gère un contexte de 256 000 tokens, accepte du texte et des images en entrée, et ne produit que du texte en sortie. Son entraînement s'est déroulé en trois phases : pré-entraînement intermédiaire, ajustement supervisé, puis apprentissage par renforcement via la méthode CISPO, appuyé sur deux environnements distincts simulant des tâches de preuve multi-tours et de manipulation directe de fichiers via un agent de code.
Les résultats annoncés par Mistral sont marquants pour le petit monde des mathématiques formelles et de la vérification de code. Le modèle atteint 100% sur les jeux de validation et de test de miniF2F, résout 587 des 672 problèmes de PutnamBench, et établit de nouveaux records sur les benchmarks d'algèbre FATE-H (87%) et FATE-X (34%). Sur FLTEval, un test bâti à partir de véritables demandes de fusion soumises au dépôt du théorème de Fermat, le score pass@1 grimpe de 21,9 à 28,9 et le pass@8 de 31,9 à 43,2, dépassant ainsi Opus 4.6 (39,6) pour un coût sept fois moindre. Sur PutnamBench, Leanstral devance de sept problèmes Seed-Prover 1.5 en configuration haute, pour un coût d'environ 4 dollars par problème contre près de 300 dollars, voire davantage, pour son concurrent. Cette efficacité économique change la donne pour les chercheurs et ingénieurs qui souhaitent automatiser la vérification formelle sans mobiliser des budgets de calcul colossaux.
Ce lancement s'inscrit dans une compétition croissante entre laboratoires d'IA pour dominer le terrain de la démonstration mathématique automatisée, où Mistral se positionne désormais face à des acteurs comme Seed-Prover, Goedel-Architect ou Aleph Prover, ce dernier facturant entre 54 et 68 dollars par problème résolu. Le comportement le plus caractéristique du modèle reste sa capacité de mise à l'échelle au moment de l'inférence : augmenter le budget de tokens alloué à chaque tentative améliore mécaniquement les performances, passant de 44 problèmes résolus avec 50 000 tokens à 587 avec 4 millions. Mistral illustre aussi des usages concrets au-delà des mathématiques pures, comme la preuve formelle de la complexité en O(log n) d'une implémentation réelle d'arbre AVL, ou encore la détection de bugs authentiques dans du code open source, ouvrant la voie à des applications de vérification logicielle à grande échelle.
Mistral AI, entreprise française, renforce sa position dans l'IA de pointe avec un modèle open-source performant sur des benchmarks de mathématiques formelles, démontrant la compétitivité de l'écosystème européen face aux acteurs américains.
Dans nos dossiers
Vu une erreur factuelle dans cet article ? Signalez-la. Toutes les corrections valides sont publiées sur /corrections.




