Leanstral 1.5

2026-07-02 · Éditeur : Mistral AI · Domaine : Intelligence Artificielle

Mistral AI publie Leanstral 1.5, agent open source Apache 2.0 de 119 milliards de paramètres (6 milliards actifs) pour les preuves Lean 4, qui sature miniF2F et résout 587 problèmes PutnamBench sur 672.

Mistral AI publie Leanstral 1.5, agent open source Apache 2.0 de 119 milliards de paramètres (6 milliards actifs) pour les preuves Lean 4, qui sature miniF2F et résout 587 problèmes PutnamBench sur 672. ### Ce qui change - Mise à jour de Leanstral avec un mélange de fine-tuning supervisé de meilleure qualité et un raisonnement à long contexte étendu. - Progression forte avec le budget de calcul : de 44 problèmes à 50k tokens jusqu'à 587 à 4M tokens. - Cinq bogues jusque-là inconnus repérés dans 57 dépôts testés. - Endpoint API gratuit. ### Caractéristiques - Paramètres : 119B au total, 6B actifs. Licence : Apache 2.0. - Identifiant API : labs-leanstral-1-5 selon le changelog (le billet cite leanstral-1-5). Retrait annoncé le 30 septembre 2026. - Poids : Hugging Face, Leanstral-1.5-119B-A6B. Utilisation via Mistral Vibe (vibe --agent lean). - Contexte et coupure : non communiqués. ### Tarifs | Élément | Tarif | |---|---| | API | Gratuit (endpoint Labs) | | Coût moyen par problème PutnamBench | environ 4 USD | ### Benchmarks | Benchmark | Score | |---|---| | miniF2F | 100 % | | PutnamBench | 587 / 672 | | FATE-H | 87 % | | FATE-X | 34 % | | FLTEval pass@1 | 28,9 | Scores publiés par l'éditeur. ### À retenir Le retrait annoncé de l'endpoint le 30 septembre 2026 impose de passer aux poids ouverts pour tout usage durable.

Tags : LLM, Mistral, Leanstral, Open Source, Preuve formelle