Mistral AI repart à l’attaque de l’IA d’entreprise. Avec Forge, Mistral permet aux organisations d’entraîner des modèles frontières sur leurs propres données. Avec Leanstral, la start-up française publie le premier agent de code open source capable de prouver formellement ce qu’il génère.

Satisfaire les besoins IA des entreprises est désormais la principale ambition de Mistral AI qui espère bien atteindre un revenu annuel récurent de près d’un milliard d’euros dès cette année. Cette attention focalisée lui permet de se démarquer un peu plus d’OpenAI et Claude et d’explorer des voies nouvelles.
En témoignent les deux principales annonces de la semaine : Mistral Forge et Mistral Leanstral.

Forge : entraîner des modèles « frontières » sur vos données

Les modèles généralistes excellent sur les tâches génériques, mais ils ignorent tout du business de l’entreprise, de son vocabulaire interne, de ses bases de code propriétaires et de ses procédures métier. C’est en grande partie l’une des raisons qui expliquent pourquoi tant de POC échouent à passer à l’échelle.

L’un des moyens de contourner cette réalité serait de permettre aux entreprises de réentraîner les modèles sur le savoir informationnel propre à l’entreprise. C’est d’ailleurs ce qui explique le succès l’an dernier des SLM. Mais outre les limitations intrinsèques aux petits modèles, les techniques de « fine-tuning » n’équivalent pas toujours à un entraînement et peuvent de révéler complexes à mettre en place.

C’est ce qui avait amené AWS à lancer en fin d’année dernière le service Nova Forge pour « permettre à chaque entreprise de créer son propre modèle frontière » à partir des modèles Nova d’AWS.

Et c’est une démarche très similaire qui conduit aujourd’hui Mistral AI à lancer Mistral Forge. La plateforme permet aux entreprises d’entraîner des modèles de niveau « frontière » directement sur leurs documentations, leurs codes sources, leurs données structurées et leurs archives opérationnelles.

Le pipeline couvre l’ensemble du cycle : pré-entraînement pour ancrer la connaissance du domaine, post-entraînement pour affiner le comportement sur des tâches spécifiques, et apprentissage par renforcement (RL) pour aligner les modèles ainsi personnalisés sur les politiques et objectifs internes. Côté architectures, Forge supporte les modèles denses comme les Mixture-of-Experts (MoE), avec prise en charge multimodale (texte, images, etc.).

ASML, Ericsson, l’Agence spatiale européenne, DSO et HTX (Singapour) ou encore Reply comptent déjà parmi les premiers partenaires. Les profils sont très variés (semi-conducteurs, télécoms, défense, spatial) mais la promesse de Forge est la même pour tous : transformer le savoir institutionnel en avantage compétitif IA.

Au-delà du besoin technique de forger ses propres modèles, la plateforme répond à une préoccupation croissante des grandes organisations : garder le contrôle sur la façon dont leur connaissance est encodée et exploitée par l’IA. Les modèles restent dans le périmètre de l’entreprise, gouvernés selon ses propres politiques de conformité et standards d’évaluation.

Forge est pour l’instant en accès sur inscription, avec un formulaire dédié pour les entreprises intéressées.

Leanstral : quand le code prouve ce qu’il fait

Deuxième annonce, tout autre registre. Leanstral est le premier agent de code open source (sous licence Apache 2.0) conçu pour Lean 4, le langage de preuve formelle utilisé aussi bien en recherche mathématique qu’en vérification logicielle critique.

On le sait, les agents de code (comme Codex d’OpenAI, Claude Code d’Anthropic ou Mistral Vibe) savent générer du code, mais le défi permanent reste de vérifier que ce qui a été généré est correct. Ce qui un goulot d’étranglement au niveau du contrôle par les humains.

Leanstral cherche en partie à soulager de goulot d’étranglement : l’agent Leanstral génère ET prouve.

Le modèle repose sur une architecture MoE très éparse : 120 milliards de paramètres au total, mais seulement 6 milliards actifs. Cette frugalité lui permet de rivaliser avec des mastodontes. Sur FLTEval, le nouveau benchmark maison basé sur des pull requests réelles du projet Fermat’s Last Theorem (et non de simples problèmes mathématiques isolés), Leanstral pass@2 atteint un score de 26,3, battant Claude Sonnet 4.6 (23,7) pour un coût de 36 $ contre 549 $. À pass@16, il grimpe à un score 31,9 et dépasse nettement Sonnet de 8 points. Seul Claude Opus 4.6 reste devant (39,6), mais son usage engendre une dépense de 1 650 $ : 92 fois plus cher !

Alors que les entreprises cherchent désormais à mieux maîtriser les coûts de l’IA – tout en soignant les besoins de confidentialité, de conformité et de contrôle – alors que l’ingénierie logicielle se réinvente totalement à l’IA agentique, Leanstral apparaît clairement comme une solution pertinente et ancrée dans la réalité terrain des organisations.

Face aux modèles open source concurrents (Qwen 3.5 397B, Kimi-K2.5, GLM5), Leanstral écrase le ratio performance/coût : il surpasse GLM5 et Kimi dès le premier passage, et dépasse Qwen 3.5 au même budget avec deux fois moins de passes.

Mistral illustre les capacités de Leanstral avec deux mises en situation concrètes :
* Premier exemple : après une mise à jour du langage Lean, un programme qui fonctionnait parfaitement refuse soudain de se compiler. Leanstral analyse le problème, identifie qu’une déclaration de type trop stricte bloque le mécanisme de preuve, et propose un correctif simple, le tout sans intervention humaine.
* Second exemple : l’agent convertit automatiquement du code écrit dans un autre langage de preuve (Rocq, anciennement Coq) vers Lean, puis démontre formellement que le programme converti se comporte bien comme prévu.
En clair, Leanstral ne se contente pas de traduire ou de corriger du code : il apporte la garantie mathématique que le résultat est correct.

Leanstral est disponible dès aujourd’hui sous trois formes : intégré à Mistral Vibe en mode zéro configuration, via un endpoint API gratuit (labs-leanstral-2603) pour une durée limitée, et en téléchargement de poids sous licence Apache 2.0. Le modèle supporte les MCP (Model Context Protocol), dont le lean-lsp-mcp fréquemment utilisé par la communauté.

____________________________

À lire également :