fr.wedoany.com Rapport : L’entreprise européenne d’intelligence artificielle Mistral AI a annoncé le 2 de ce mois, heure locale, le lancement du modèle Leanstral 1.5, dédié au langage de programmation de preuve formelle mathématique Lean 4. Ce modèle totalise 119B paramètres, avec 6B paramètres activés, et est publié en open source sous licence Apache-2.0.

Mistral AI indique que le modèle Leanstral 1.5 atteint un taux d’achèvement de 100 % sur les ensembles de validation et de test du benchmark mathématique formel miniF2F ; il résout 587 des 672 problèmes Lean 4 de l’ensemble de problèmes mathématiques de compétition PutnamBench ; pour la série de benchmarks d’algèbre abstraite FATE, il obtient un taux de réussite de 87 % sur le niveau master FATE-H et de 34 % sur le niveau doctorat FATE-X, soit les meilleures performances. Ces tests montrent que les capacités mathématiques du modèle ont atteint un niveau utilisable.

Mistral AI souligne l’avantage de coût du nouveau modèle : pour les problèmes de l’ensemble de données PutnamBench, le coût moyen de résolution de Leanstral 1.5 n’est que de 4 dollars, tandis que Seed-Prover 1.5 nécessite plus de 300 dollars et Aleph Prover, entre 54 et 68 dollars.

Dans des applications en situation réelle, Leanstral 1.5 a signalé 47 propriétés non conformes dans les 57 bases de code testées, dont 11 pointaient vers des défauts réels, incluant 5 problèmes non signalés auparavant sur GitHub.