Leanstral

2026-03-16 · Éditeur : Mistral AI · Domaine : Intelligence Artificielle

Mistral AI publie Leanstral, un agent open source Apache 2.0 d'environ 120 milliards de paramètres (6 milliards actifs) pour l'ingénierie de preuves formelles en Lean 4 et le codage vérifiable.

Mistral AI publie Leanstral, un agent open source Apache 2.0 d'environ 120 milliards de paramètres (6 milliards actifs) pour l'ingénierie de preuves formelles en Lean 4 et le codage vérifiable. ### Ce qui change - Modèle conçu pour des dépôts Lean réalistes plutôt que pour les seules mathématiques de compétition. - Intégré à Mistral Vibe (commande /leanstral). - Endpoint API gratuit ou quasi gratuit sur une période limitée. - Architecture parcimonieuse : environ 6B de paramètres actifs. ### Caractéristiques - Paramètres : environ 120B au total (119B côté Hugging Face), 6B actifs. - Identifiant API : labs-leanstral-2603. - Licence : Apache 2.0, poids téléchargeables. - Disponibilité : API, Mistral Vibe, Hugging Face (Leanstral-2603). - Contexte, sortie maximale, coupure : non communiqués. ### Tarifs | Élément | Tarif | |---|---| | Endpoint API | Gratuit ou quasi gratuit pendant une période limitée | | Coût d'évaluation FLTEval, pass@2 | 36 USD | | Coût d'évaluation FLTEval, pass@16 | 290 USD | Les montants de pass@k sont des coûts d'évaluation du benchmark, pas des tarifs par token. ### Benchmarks | Mesure (FLTEval) | Score | |---|---| | pass@2 | 26,3 (Claude Sonnet : 23,7, pour 549 USD) | | pass@16 | 31,9 | Scores publiés par l'éditeur. ### À retenir Un vérificateur formel ouvert et peu coûteux intéresse les équipes qui veulent des garanties sur du code critique, au-delà de la simple relecture par un LLM.

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