Mistral a créé une IA qui ne devine plus si le code est juste, elle le prouve

Mistral innove dans la recherche de bug et fait le constat : plutôt que de chercher des failles par chance, une IA pouvait prouver mathématiquement qu'un bout de code ne contient aucune faille du tout ? C'est exactement ce que fait Leanstral 1.5, un modèle publié en open source cette semaine et passé largement sous les radars du grand public.

Leanstral s'appuie sur Lean 4, un langage utilisé par les mathématiciens pour rédiger des démonstrations que d'autres logiciels peuvent vérifier automatiquement, sans ambiguïté possible. Contrairement à un assistant de code classique qui génère une réponse plausible, Leanstral produit une preuve formelle : soit elle passe la vérification et la propriété est garantie, soit elle échoue et il n'y a rien à discuter. Sur miniF2F, un test de mathématiques allant du lycée aux olympiades, le modèle atteint 100 % de réussite. Sur le très exigeant PutnamBench, il résout 587 des 672 problèmes du concours Putnam, l'une des compétitions de mathématiques les plus difficiles au monde pour des étudiants.

Là où l'histoire devient concrète, c'est que Mistral n'a pas cantonné son modèle aux mathématiques pures. L'équipe l'a lancé sur 57 dépôts de code open source pour voir s'il pouvait repérer de vrais problèmes, et non plus prouver des théorèmes abstraits. Résultat : cinq bugs jusqu'alors inconnus, dont un dans la bibliothèque Rust avec un genre de bug qui peut rester tapi des années dans une dépendance utilisée par des milliers de projets sans que personne ne s'en aperçoive.

L'annonce a un autre mérite : Leanstral est publié sous licence Apache 2.0, librement téléchargeable, et selon Mistral il dépasserait Claude Sonnet de huit points sur les benchmarks de preuve formelle tout en coûtant environ quinze fois moins cher à faire tourner que les alternatives propriétaires. Pour un domaine, la vérification formelle, qui est resté pendant des décennies l'apanage de quelques laboratoires spécialisés et de logiciels critiques (aviation, cryptographie, systèmes bancaires), voir un acteur européen rendre l'outil accessible à n'importe quel développeur change la donne.

On parle beaucoup de la vitesse à laquelle l'IA écrit du code, beaucoup moins de sa capacité à en garantir la fiabilité. Leanstral déplace discrètement le curseur du côté de la confiance plutôt que de la productivité brute, et c'est peut-être le développement le plus important de la semaine pour quiconque dépend, sans le savoir, d'une brique logicielle open source quelque part dans sa pile technique.