Mistral AI a dévoilé Devstral, un modèle de langage de grande envergure conçu pour le développement d'applications (programmation intuitive) et optimisé pour la vérification formelle du code. Devstral devrait permettre de créer des assistants IA capables non seulement de générer du code, mais aussi de garantir son absence d'erreurs.
Devstral est devenu le premier modèle open source à prendre en charge le langage de programmation Lean 4 et son ensemble d'outils de vérification mathématique associé. Lean 4 permet de prouver mathématiquement la correction du code et sa conformité aux spécifications, ce qui, dans le contexte du codage par intuition, permet de confirmer que le code généré par un modèle d'IA fait exactement ce qu'il est censé faire.
Le modèle couvre 119 milliards de paramètres (6.5 milliards de paramètres activés par jeton), prend en compte les contextes de 256 000 jetons et est publié sous licence Apache 2.0. L’archive téléchargeable avec Leanstral pèse 121 Go et est compatible avec une utilisation sur les systèmes locaux. Les bibliothèques vllm, transformers et SGLang peuvent être utilisées pour une exécution locale.
Ce modèle peut notamment servir au développement de l'agent open-source mistral-vibe et s'intégrer à la boîte à outils Aeneas pour la vérification de code Rust. Il accepte du texte et des images en entrée et ne produit que du texte en sortie. L'analyse du contenu des images est prise en charge.
Afin d'évaluer les capacités des modèles d'IA, en tenant compte de la qualité de la vérification formelle du code et de la rédaction des preuves mathématiques, une nouvelle suite de tests FLTEval a été développée. Lors des tests, le modèle Leanstral a nettement surpassé les modèles open source existants Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B et GLM5 744B-A40B. Il a obtenu des résultats similaires à ceux de Claude Haiku 4.5 et Claude Sonnet 4.6 d'Anthropic, mais est resté en deçà du modèle Claude Opus 4.6. Plus précisément, le modèle Opus a obtenu un score de 39.6 points, tandis que Leanstral a obtenu 21.9 points en une seule passe et 31.9 points en 16 passes. Le coût d'utilisation d'Opus était de 1 650 $, tandis que celui de Leanstral était de 18 $ en une seule passe et de 290 $ en 16 passes. Le haïku a obtenu 23 points à 184 $, tandis que le sonnet a obtenu 23.7 points à 549 $.
Source: opennet.ru
