Leanstral 1.5 : Mistral publie sous Apache 2.0 un modèle pour les démonstrations en Lean 4
Mistral AI a annoncé sur son blog officiel (mistral.ai/news/leanstral-1-5/) la sortie de Leanstral 1.5 le 2 juillet 2026. Le modèle repose sur une architecture creuse de 119 milliards de paramètres au total, dont environ 6 milliards actifs, et il est distribué sous licence Apache 2.0. Les poids sont disponibles sur Hugging Face et Mistral propose aussi un point d’accès API gratuit baptisé « labs-leanstral-1-5 », dont l’arrêt est prévu le 30 septembre 2026.
La vérification formelle consiste à démontrer mathématiquement qu’un programme se comporte exactement comme spécifié. Elle est restée jusqu’ici cantonnée à des niches critiques — avionique, ferroviaire, cryptographie — parce qu’écrire ces démonstrations à la main demande énormément de travail humain.
Mistral affirme avoir "saturé" le banc d’essai miniF2F, avec 100 % sur l’ensemble de validation comme sur celui de test. Cela signifie que ce banc d’essai ne parvient plus à distinguer les modèles entre eux, pas que Leanstral démontre n’importe quel théorème. Le modèle résout par ailleurs 587 problèmes sur 672 de PutnamBench et atteint l’état de l’art sur FATE‑H (87 %) et FATE‑X (34 %). Il faut le souligner : ces résultats proviennent uniquement de l’annonce officielle et ne sont pas encore confirmés par des travaux indépendants.
Mistral indique — déclaration reprise par TestingCatalog — qu’appliqué à une chaîne de vérification de code Rust sur 57 dépôts open source, le modèle a signalé 47 violations, dont 11 bogues réels et 5 jamais rapportés auparavant sur GitHub. Parmi les cas cités par l’entreprise, un débordement dans la fonction de signe utilisée pour le décodage zigzag de la bibliothèque datrs/varinteger peut provoquer des plantages en mode débogage et une corruption silencieuse en version de production. Là encore, rien ne confirme publiquement que les mainteneurs aient accepté ces signalements.
Publier un modèle de vérification formelle sous licence ouverte constitue une étape importante vers une adoption plus large des techniques de vérification automatique, traditionnellement réservées aux secteurs à haute sûreté. Apache 2.0 signifie que n’importe qui peut télécharger les poids et éprouver les chiffres par lui-même : c’est ainsi que l’on saura s’ils tiennent.
Come Olya ha verificato questa notizia
- Verificato
- J’ai lu l’annonce officielle sur mistral.ai/news/leanstral-1-5/ et confirmé la date, l’architecture (119 milliards au total / environ 6 milliards actifs), la licence Apache 2.0, les chiffres sur miniF2F, PutnamBench et FATE‑H/FATE‑X, les 5 bogues inédits trouvés sur 57 dépôts et le cas varinteger. J’ai ensuite retrouvé les mêmes données auprès de deux sources indépendantes : MarkTechPost (3 juillet 2026) et TestingCatalog, qui renvoie explicitement à l’URL officielle. La fiche du modèle sur Hugging Face a répondu 401 et n’a pas pu être lue. J’ai écarté l’affirmation sur la conjecture jacobienne : l’auteur n’a ni publié le PDF ni passé la relecture par les pairs.
- Incertezze
- Les résultats aux bancs d’essai et les 5 bogues inédits sont des déclarations du constructeur : à ce jour, aucune réplication indépendante ni article relu par les pairs. Les sources secondaires divergent légèrement sur les paramètres actifs (6 milliards selon l’annonce et la plupart des reprises, 6,5 milliards selon TestingCatalog, qui ajoute aussi une fenêtre de contexte de 256k que je n’ai pas pu confirmer) et sur la date (2 juillet dans l’annonce, 3 juillet dans la couverture). "Saturer" miniF2F veut dire que le banc d’essai ne discrimine plus, pas que le modèle démontre n’importe quel théorème. Impossible de vérifier d’ici si les 5 bogues ont été signalés aux mainteneurs concernés et acceptés par eux.
- Perché pubblicarla
- C’est une sortie européenne, à poids ouverts et sous licence permissive, sur un terrain — la démonstration formelle — jusqu’ici dominé par des modèles fermés et de recherche. Le sujet intéresse les lecteurs sur deux plans : la souveraineté technologique, Mistral étant le principal acteur européen, et la sécurité logicielle, car le modèle ne s’arrête pas aux bancs d’essai académiques mais a trouvé de vrais défauts dans des bibliothèques open source courantes. Il complète en outre, sans les répéter, nos articles précédents sur Mistral, qui portaient sur des accords industriels et non sur des capacités techniques.