Mistral innove : lancement d’un nouveau modèle, partenariat stratégique avec NVIDIA et intégration d’un agent de preuve formelle
Mistral a annoncé simultanément le lancement du modèle Small 4, son adhésion comme membre fondateur à la coalition Nemotron portée par NVIDIA et la mise en service de l’agent de preuve formelle Leanstral.
Mistral Small 4 unifie raisonnement, multimodalité et code agentique
Le Small 4 combine traitement texte et image, raisonnement step-by-step et génération de code agentique dans un seul modèle publié sous licence Apache 2.0. L’architecture est une Mixture of Experts totale de 119 milliards de paramètres avec 6 milliards activés par requête.
La fenêtre de contexte atteint 256 000 tokens. Mistral indique une réduction de latence de 40 % et un débit multiplié par 3 par rapport à Small 3 dans une configuration optimisée. Le paramètre reasoning_effort permet d’ajuster le compromis vitesse/profondeur d’analyse. Small 4 est disponible via l’API Mistral, sur Hugging Face et comme conteneur optimisé NVIDIA NIM, compatible vLLM, llama.cpp, SGLang et Transformers.
Conséquences opérationnelles pour les entreprises suisses
La consolidation fonctionnelle réduit la multiplicité des déploiements pour une banque ou un bureau d’études. Par exemple la banque romande fictive Banque Romande SA peut traiter des documents longs sans segmentation et réduire les coûts d’inférence en production via un seul modèle.
L’offre on-prem via NVIDIA NIM facilite la mise en conformité avec les exigences internes de protection des données, mais pose la question de la dépendance matérielle.
Coalition Nemotron et enjeux de souveraineté numérique
Mistral rejoint NVIDIA, Perplexity, Cursor et Black Forest Labs pour co-développer un modèle de base open source, Nemotron 4, entraîné sur le cloud DGX de NVIDIA.
Le partenariat offre un accès à une infrastructure de calcul à grande échelle et permet à Mistral d’étendre son influence sur les standards open source. Simultanément, l’entreprise renforce ses capacités de calcul en France et en Suède pour limiter une dépendance exclusive aux ressources américaines, question importante pour la souveraineté numérique.
Leanstral et la preuve formelle pour l’agentique
Leanstral génère des preuves formelles en Lean 4 et produit la démonstration vérifiée par le vérificateur Lean. L’agent utilise 6 milliards de paramètres actifs et vise à réduire le goulot d’étranglement humain dans la validation de code critique.
Sur le benchmark interne FLTEval, Mistral communique un pass@2 26,3 à 36 dollars et un pass@16 31,9, avec des comparaisons de coûts favorables face à des modèles généralistes. Ces métriques nécessitent une lecture critique en raison du caractère maison du benchmark et des conditions d’évaluation.
