L’IA générative permet de supprimer les bogues
Des chercheurs américains ont mis au point une méthode de vérification automatique des logiciels avec un taux d’efficacité de près de 66 % en utilisant de grands modèles linguistiques LLM.
L’équipe d’informaticiens dirigée par l’université du Massachusetts Amherst a mis au point une méthode permettant de générer automatiquement des preuves complètes qui peuvent être utilisées pour des logiciels sans bogues et vérifier que le code sous-jacent est correct.
Cette nouvelle méthode, appelée Baldur, utilise de grands modèles de langage (LLM) et, combinée à l’outil de pointe Thor, permet d’atteindre une efficacité sans précédent de près de 66 %. L’équipe s’est récemment vu décerner le prix du meilleur article lors de la conférence européenne conjointe de l’ACM sur le génie logiciel et du symposium sur les fondements du génie logiciel.
- Le défi de conception de silicium par IA générative se prépare pour la fabrication
- MediaTek mise sur l’IA générative pour remplacer les écrans tactiles
- Cadence lance l’IA générative pour la conception de circuits imprimés
« Nous nous sommes malheureusement habitués à ce que nos logiciels soient bogués, bien qu’ils soient omniprésents et que nous les utilisions tous quotidiennement », explique Yuriy Brun (ci-dessus, à droite), professeur au Manning College of Information and Computer Sciences de l’UMass Amherst.
Les bogues dans les logiciels peuvent être potentiellement catastrophiques lorsqu’il s’agit de failles de sécurité ou de logiciels de précision utilisés pour l’exploration spatiale ou pour contrôler les appareils de soins de santé.
Les méthodes formelles pour des logiciels sans bogues peuvent générer une preuve mathématique montrant que le code fait ce qu’il est censé faire, puis utiliser un prouveur de théorème pour s’assurer que la preuve est également correcte.
Mais la rédaction manuelle de ces preuves prend énormément de temps et nécessite une grande expertise. « Ces preuves peuvent être plusieurs fois plus longues que le code du logiciel lui-même », explique Emily First (ci-dessus), l’auteur principal de l’article, qui a effectué cette recherche dans le cadre de sa thèse de doctorat à l’UMass Amherst.
Un modèle de langage étendu est un moyen possible de générer automatiquement de telles preuves.
Cependant, « l’un des plus grands défis des LLM est qu’ils ne sont pas toujours corrects », déclare M. Brun. « Au lieu de se planter et de vous faire savoir que quelque chose ne va pas, ils ont tendance à ‘échouer silencieusement’, en produisant une réponse incorrecte mais en la présentant comme si elle était correcte. Or, souvent, la pire chose à faire est d’échouer silencieusement ».
L’équipe a utilisé Minerva, un LLM formé sur un vaste corpus de textes en langue naturelle, puis l’a affiné sur 118 Go d’articles scientifiques mathématiques et de pages web contenant des expressions mathématiques.
Ensuite, le LLM a été affiné sur un langage, appelé Isabelle/HOL, dans lequel les preuves mathématiques sont écrites. Baldur a ensuite généré une preuve complète et a travaillé en tandem avec le prouveur de théorèmes pour vérifier son travail.
Lorsque le prouveur de théorèmes a détecté une erreur, il a renvoyé la preuve, ainsi que les informations relatives à l’erreur, au LLM, afin qu’il puisse tirer les leçons de son erreur et générer une nouvelle preuve, que l’on espère exempte d’erreurs.
Ce processus permet d’obtenir une amélioration remarquable de la précision. L’outil de pointe pour la génération automatique de preuves s’appelle Thor, qui peut générer des preuves dans 57 % des cas. Lorsque Baldur (le frère de Thor, selon la mythologie nordique) est associé à Thor, les deux peuvent générer des preuves dans 65,7 % des cas.
Bien qu’il y ait encore un grand nombre d’erreurs, Baldur est de loin le moyen le plus efficace et le plus performant jamais conçu pour vérifier l’exactitude d’un logiciel exempt de bogues.
Si vous avez apprécié cet article, vous aimerez les suivants : ne les manquez pas en vous abonnant à :
