La société Mistral AI a présenté un grand modèle linguistique nommé Devstral, destiné à être utilisé pour le développement d'applications (vibe-coding) et optimisé pour la vérification formelle du code. Il est supposé que Devstral peut être utilisé pour créer des assistants IA capables non seulement de générer du code, mais aussi de garantir l'absence d'erreurs dans celui-ci.
Devstral est devenu le premier modèle open source à supporter le langage de programmation Lean 4 et les outils associés pour la vérification des preuves mathématiques. Lean 4 offre des fonctionnalités pour la preuve mathématique de la correction du code et de sa conformité à la spécification, ce qui, dans le contexte du vibe-coding, permet de confirmer que le code généré par le modèle IA fait exactement ce qui est prévu.
Le modèle couvre 119 milliards de paramètres (6,5 milliards de paramètres activés par token), prend en compte un contexte de 256 000 tokens et est publié sous la licence Apache 2.0. L'archive téléchargeable avec Leanstral occupe 121 Go et est utilisable sur des systèmes locaux. Pour un fonctionnement local, les bibliothèques vllm, transformers et SGLang peuvent être utilisées.
Parmi ses nombreuses applications, le modèle peut être utilisé pour le vibe-développement dans l'agent open source mistral-vibe, ainsi qu'être intégré avec l'outil Aeneas pour la vérification de code en langage Rust. Les paramètres d'entrée comprennent du texte et des images, et la sortie ne donne que du texte. L'analyse du contenu des images est également supportée.
Pour é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 de preuves mathématiques, un nouveau jeu de tests nommé FLTEval a été développé. Lors des tests effectués, 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, montrant des résultats similaires aux modèles Claude Haiku 4.5 et Claude Sonnet 4.6 de la société Anthropic, mais était en retard par rapport au modèle Claude Opus 4.6. En particulier, le modèle Opus a obtenu 39,6 points, tandis que Leanstral a reçu 21,9 lors d'un passage et 31,9 lors de 16 passages. Les coûts d'utilisation de l'Opus étaient de 1650 dollars, tandis que Leanstral coûtait 18 $ pour un passage et 290 $ pour 16 passages. Le modèle Haiku a obtenu 23 points avec des coûts de 184 $, tandis que le modèle Sonnet a cumulé 23,7 points pour des coûts de 549 $.
Source : opennet.ru
