Des chercheurs développent une méthode de vérification automatique basée sur l'IA pour vérifier le code logiciel

Une équipe d'informaticiens dirigée par l'Université du Massachusetts à Amherst a récemment annoncé une nouvelle méthode permettant de générer automatiquement des preuves complètes pouvant être utilisées pour éviter les bogues logiciels et vérifier que le code sous-jacent est correct.

Cette nouvelle méthode, appelée Baldur, exploite la puissance de l'intelligence artificielle des grands modèles de langage (LLM) et, combinée à l'outil de pointe Thor, offre une efficacité sans précédent de près de 66 %. L’équipe a récemment reçu un prix Distinguished Paper lors de la conférence et symposium européens conjoints sur le génie logiciel de l’ACM sur les fondements du génie logiciel.

“Nous en sommes malheureusement venus à nous attendre à ce que notre logiciel soit bogué, même s'il est partout et que nous l'utilisons tous quotidiennement”, déclare Yuriy Brun, professeur au Manning College of Information and Computer Sciences de l'UMass Amherst et directeur principal du journal. auteur.

Les effets des logiciels bogués peuvent aller de l'ennuyeux (formatage défectueux ou pannes soudaines) à potentiellement catastrophique en ce qui concerne les failles de sécurité ou les logiciels de précision utilisés pour l'exploration spatiale ou pour contrôler les appareils de soins de santé.

Bien entendu, il existe des méthodes de vérification des logiciels depuis aussi longtemps qu’ils existent. Une méthode populaire est la plus simple : vous demandez à un être humain de parcourir le code, ligne par ligne, en vérifiant manuellement qu’il n’y a pas d’erreurs. Ou vous pouvez exécuter le code et le comparer à ce que vous attendez de lui. Si, par exemple, vous vous attendez à ce que votre logiciel de traitement de texte coupe la ligne chaque fois que vous appuyez sur la touche « retour », mais qu'il génère à la place un point d'interrogation, alors vous savez que quelque chose dans le code ne va pas.

Le problème avec les deux méthodes est qu’elles sont sujettes à l’erreur humaine, et vérifier tous les problèmes possibles est extrêmement long, coûteux et irréalisable pour tout autre système que trivial.

Une méthode beaucoup plus approfondie, mais plus difficile, consiste à 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. Cette méthode est appelée vérification automatique.

Mais la rédaction manuelle de ces preuves prend énormément de temps et nécessite une expertise approfondie. “Ces preuves peuvent être plusieurs fois plus longues que le code du logiciel lui-même”, explique Emily First, l'auteur principal de l'article qui a réalisé cette recherche dans le cadre de sa thèse de doctorat à l'UMass Amherst.

Avec l’essor des LLM, dont ChatGPT est l’exemple le plus célèbre, une solution possible est d’essayer 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”, explique Brun. « Au lieu de s'effondrer et de vous faire savoir que quelque chose ne va pas, ils ont tendance à « échouer en silence », produisant une réponse incorrecte mais en la présentant comme si elle était correcte. Et, souvent, la pire chose que vous puissiez faire est d'échouer en silence.

C'est là qu'intervient Baldur.

Premièrement, dont l'équipe a effectué son travail chez Google, a utilisé Minerva, un LLM formé sur un vaste corpus de textes en langage naturel, puis l'a peaufiné sur 118 Go d'articles scientifiques mathématiques et de pages Web contenant des expressions mathématiques.

Ensuite, elle a affiné le LLM 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ème pour vérifier son travail. Lorsque le prouveur de théorème a détecté une erreur, il a renvoyé la preuve, ainsi que les informations sur l'erreur, dans le LLM, afin qu'il puisse tirer les leçons de son erreur et générer une nouvelle preuve, espérons-le, sans erreur.

Ce processus donne une augmentation remarquable de la précision. L'outil de pointe pour générer automatiquement des preuves s'appelle Thor, qui peut générer des preuves 57 % du temps. Lorsque Baldur (le frère de Thor, selon la mythologie nordique) est associé à Thor, les deux peuvent générer des preuves 65,7 % du temps.

Bien qu'il existe encore un grand degré d'erreur, Baldur est de loin le moyen le plus efficace et efficient jamais conçu pour vérifier l'exactitude des logiciels, et à mesure que les capacités de l'IA sont de plus en plus étendues et raffinées, l'efficacité de Baldur devrait également croître.

L'article est publié dans le cadre du Actes de la 31e conférence et symposium européens conjoints sur le génie logiciel de l'ACM sur les fondements du génie logiciel.