Pour repérer des bugs dans des logiciels sensibles, des chercheurs font appel à l’IA

Tous les logiciels ne sont pas parfaits. De nombreuses applications, programmes et sites web sont mis sur le marché malgré la présence d’erreurs. Dans la plupart des cas, les conséquences ne sont pas dramatiques. Il n’en va pas de même avec les systèmes critiques tels que les protocoles cryptographiques, les appareils médicaux, les fusées…

Le 4 juin 1996 à 9h35 du matin, la fusée Ariane 5 échappe à tout contrôle et explose en vol après seulement 36 secondes. L’origine de cet accident se trouve dans quelques lignes de code. Pour des raisons de coûts, un code dans les systèmes informatiques qui gèrent le guidage a été copié de Ariane 4 à Ariane 5. Or, le logiciel Ariane 4 utilisait des nombres entiers de 16 bits, tandis que les capteurs Ariane 5 envoyaient des nombres flottants de 64 bits.

Cette intégration a provoqué une erreur de conversion. Le logiciel a cru que la fusée allait dans une mauvaise direction et a ordonné une correction massive. Résultat, la fusée s’est autodétruite. Coût : 500 millions d’euros.

Au début des années 1980, Therac-25 a entraîné la mort de cinq malades. Développée conjointement par l’Énergie atomique du Canada Limitée et CGR MeV, cette machine de radiothérapie avait provoqué une overdose de radiations à cause d’un bug informatique. La machine sera retirée du marché en… 1987.

Ces deux exemples confirment que la moindre erreur dans un logiciel peut avoir de graves conséquences. Mais la repérer est un vrai casse-tête. C’est pourtant indispensable lorsqu’il s’agit d’appareils médicaux. Problème, un logiciel dans un pacemaker peut nécessiter plus de 80 000 lignes de code, une pompe à perfusion de 170 000 lignes et un scanner à IRM (Imagerie à Résonance Magnétique) plus de 7 millions de lignes.

Baldur et Thor trouvent des preuves

Pour relever ce défi, on s’appuie sur des méthodes dites « formelles ». Elles permettent de répondre aux besoins de certification des logiciels critiques en assurant la fiabilité et l’absence de dysfonctionnement d’un système ou d’un logiciel. En reposant sur des formules mathématiques, les ambiguïtés ne sont pas possibles ! On apporte la preuve qu’il n’y a pas de bugs et que le logiciel fonctionne correctement.

Pour faciliter cette vérification formelle, une équipe de chercheurs de l’Université de Massachusetts Amherst a mis au point une nouvelle méthode basée sur l’intelligence artificielle. Appelée Baldur, elle permet de générer automatiquement des preuves mathématiques.

Dirigée par Yuriy Brun, cette équipe s’appuie sur le grand modèle de langage (LLM) Minerva de Google. Baldur a été entraîné à partir d’articles scientifiques (équivalent de 118 Go de données) et de pages web contenant des expressions mathématiques. L’étape suivante a consisté à s’appuyer sur des données relatives aux preuves et aux théorèmes.

Baldur travaille avec Isabell/HOL, un langage dans lequel les preuves mathématiques sont écrites. Lorsqu’il reçoit un énoncé de théorème, Baldur est capable de générer une preuve complète dans près de 41 % des cas. Si Isabell/HOL trouve une erreur, les informations relatives à cette erreur sont renvoyées au LLM pour lui permettre d’apprendre de son erreur et de générer une autre preuve avec moins d’erreurs, voire aucune.

Pour augmenter le taux de réussite de Baldur, l’équipe a fourni au modèle des informations contextuelles supplémentaires, telles que d’autres définitions ou les lignes précédant l’énoncé du théorème dans un fichier théorique. Le taux de preuve a progressé à 47,5 %. Cela signifie que Baldur est capable de prendre en compte le contexte et de l’utiliser pour prédire une nouvelle preuve correcte.

La situation s’améliore encore plus lorsque Baldur est associé à Thor, un autre outil spécialisé dans la génération automatique de preuves. Ce binôme parvient à générer des preuves correctes dans près de 66 % des cas.

Il reste donc encore un degré d’erreur considérable. Mais les techniques d’intelligence artificielle continuant de s’améliorer, les capacités de Baldur devraient progresser également. En attendant, ce projet a été approuvé par la Defense Advanced Research Projects Agency (DARPA) et la National Science Foundation.