Baldur, une nouvelle méthode d'IA pour prévenir les bogues de logiciels et vérifier le code sous-jacent
Baldur, une nouvelle méthode d'IA pour générer automatiquement des preuves complètes avec LLM qui peuvent être utilisées pour prévenir les bogues de logiciels et vérifier que le code sous-jacent est correct
Des chercheurs de l'UMass Amherst rapprochent le rêve d'un logiciel sans bogues de la réalité. La méthode primée, appelée Baldur, vérifie automatiquement les logiciels avec une efficacité de près de 66 %.
Une équipe d'informaticiens dirigée par l'université du Massachusetts Amherst a récemment annoncé une nouvelle méthode pour générer automatiquement des preuves entières qui peuvent être utilisées pour prévenir les bogues de 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, lorsqu'elle est associée à l'outil de pointe Thor, elle permet d'obtenir une efficacité sans précédent de près de 66 %. L'équipe s'est récemment vu décerner le prix très convoité de l'article distingué 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.
"Nous nous sommes malheureusement habitués à ce que nos logiciels soient bogués, alors qu'ils sont partout et que nous les utilisons tous quotidiennement", déclare Yuriy Brun, professeur au Manning College of Information and Computer Sciences de l'UMass Amherst et auteur principal de l'article.
Les effets d'un logiciel bogué peuvent aller de l'ennui - formatage défectueux ou plantage soudain - à la catastrophe potentielle lorsqu'il s'agit de failles de sécurité ou de logiciels de précision utilisés pour l'exploration spatiale ou pour le contrôle d'appareils de soins de santé.
Bien entendu, il existe des méthodes de vérification des logiciels depuis que ceux-ci existent. L'une des méthodes les plus répandues est la plus simple : un être humain parcourt le code, ligne par ligne, et vérifie manuellement qu'il n'y a pas d'erreurs. Vous pouvez également 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 affiche à la place un point d'interrogation, vous savez que quelque chose dans le code ne va pas.
Le problème de ces deux méthodes est qu'elles sont sujettes à l'erreur humaine et que la vérification de tous les problèmes possibles prend énormément de temps, est très coûteuse et n'est pas réalisable pour des systèmes autres que triviaux.
Une méthode beaucoup plus complète, 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 s'appelle le "machine-checking".
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, auteur principal de l'article, qui a effectué 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 ces preuves automatiquement. Cependant, "l'un des plus grands défis des LLM est qu'ils ne sont pas toujours corrects", explique 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 en silence".
C'est là que Baldur entre en jeu.
D'abord, l'équipe de Baldur, qui a effectué ses travaux chez Google, a utilisé Minerva, un LLM formé sur un vaste corpus de textes en langage naturel, puis l'a affiné 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èmes pour vérifier son travail. Lorsque le prouveur de théorèmes détectait une erreur, il renvoyait 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 augmentation 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 subsiste un grand nombre d'erreurs, Baldur est de loin le moyen le plus efficace et le plus efficient jamais conçu pour vérifier l'exactitude d'un logiciel, et à mesure que les capacités de l'IA s'étendent et s'affinent, l'efficacité de Baldur devrait s'accroître.
Outre First et Brun, l'équipe comprend Markus Rabe, employé par Google à l'époque, et Talia Ringer, professeur adjoint à l'université de l'Illinois-Urbana Champaign. Ces travaux ont été réalisés chez Google et soutenus par la Defense Advanced Research Projects Agency et la National Science Foundation.
Résumé
La vérification formelle des propriétés des logiciels est une tâche hautement souhaitable mais qui demande beaucoup de travail. Des travaux récents ont développé des méthodes pour automatiser la vérification formelle en utilisant des assistants de preuve, tels que Coq et Isabelle/HOL, par exemple en formant un modèle pour prédire une étape de preuve à la fois, et en utilisant ce modèle pour rechercher dans l'espace des preuves possibles. Cet article présente une nouvelle méthode pour automatiser la vérification formelle : Nous utilisons de grands modèles de langage, formés sur du texte et du code en langage naturel et affinés sur des preuves, pour générer des preuves entières de théorèmes en une seule fois, plutôt qu'une étape à la fois. Nous combinons ce modèle de génération de preuves avec un modèle de réparation finement ajusté pour réparer les preuves générées, ce qui augmente encore la puissance de preuve. Comme principales contributions, cet article démontre pour la première fois que : (1) la génération de preuves complètes à l'aide de transformateurs est possible et aussi efficace que les techniques basées sur la recherche sans nécessiter de recherche coûteuse. (2) Le fait de donner au modèle appris un contexte supplémentaire, tel qu'une tentative de preuve antérieure qui a échoué et le message d'erreur qui s'en est suivi, permet de réparer la preuve et d'améliorer encore la génération automatique de preuves. (3) Nous établissons un nouvel état de l'art pour la synthèse de preuves entièrement automatisée. Nous réifions notre méthode dans un prototype, Baldur, et l'évaluons sur un benchmark de 6.336
Théorèmes d'Isabelle/HOL et leurs preuves.
En plus de montrer empiriquement l'efficacité de la génération de preuves complètes, de la réparation et de l'ajout de contexte, nous montrons que Baldur améliore l'outil de pointe, Thor, en générant automatiquement des preuves pour 8,7 % supplémentaires des théorèmes. Ensemble, Baldur et Thor peuvent prouver 65,7 % des théorèmes de manière entièrement automatique. Cet article ouvre la voie à de nouvelles recherches sur l'utilisation de grands modèles de langage pour automatiser la vérification formelle.
Source : Etude réalisée par les chercheurs Emily First, Yuriy Brun, Markus Rabe et Talia Ringer
Et vous ?
Que pensez-vous de Baldur ?
Voir aussi :
Répondre avec citation
Partager