Leanstral 1.5 : vérification formelle open-source avec 6B paramètres actifs (en)

Mistral publie Leanstral 1.5, un modèle sous licence Apache 2.0 dédié à la vérification formelle en Lean 4, avec 119B paramètres totaux mais seulement 6B actifs. Il atteint 100% sur miniF2F, résout 587/672 problèmes PutnamBench et établit un nouveau state-of-the-art sur FATE-H (87%) et FATE-X (34%). Le modèle opère en mode agentique sur un filesystem réel (édition de fichiers, commandes bash, serveur de langage Lean) et a détecté 5 bugs inconnus dans des dépôts open-source. Disponible via Hugging Face et une API gratuite.