Skip to main content

30 Jan, 2024

Le générateur de preuves alimenté par l’IA aide à débuguer le logiciel 

Le générateur de preuves alimenté par l’IA aide à débuguer le logiciel 

Baldur écrit ses propres preuves pour vérifier automatiquement le code

Tous les logiciels ne sont pas parfaits : de nombreuses applications, programmes et sites Web sont publiés malgré les bugs. Mais les logiciels derrière les systèmes critiques tels que les protocoles cryptographiques, les dispositifs médicaux et les navettes spatiales doivent être exempts d’erreurs, et garantir l’absence de bugs nécessite d’aller au-delà de la révision et des tests de code. Cela nécessite une vérification formelle.

La vérification formelle implique l’écriture d’une preuve mathématique de votre code et constitue « l’un des moyens les plus difficiles mais aussi les plus puissants de garantir que votre code est correct », explique Yuriy Brun , professeur à l’ Université du Massachusetts à Amherst .

Pour faciliter la vérification formelle, Yuri et ses collègues ont conçu une nouvelle méthode basée sur l’IA baptisé Baldur pour générer automatiquement des preuves. L’article d’accompagnement , présenté en décembre 2023 lors de la conférence et du symposium européens conjoints sur le génie logiciel de l’ACM sur les fondements du génie logiciel à San Francisco, a remporté un prix d’article distingué . L’équipe comprend Emily First , qui a réalisé l’étude dans le cadre de sa thèse de doctorat à l’UMass Amherst ; Markus Rabe, ancien chercheur chez Google , où l’étude a été menée ; et Talia Ringer , professeur adjoint à l’ Université de l’Illinois à Urbana-Champaign .

Cet organigramme montre à un niveau élevé comment Baldur génère une preuve. 

Baldur est alimenté par le modèle de langage étendu MinervaLLM ) de Google , qui a été formé sur des articles scientifiques et des pages Web contenant des expressions mathématiques et affiné sur des données sur les preuves et les théorèmes. Baldur travaille avec Isabelle , assistante de preuve ou prouveur automatisé de théorèmes,pour vérifier ses preuves. Lorsqu’on lui donne un théorème, Baldur est capable de générer une preuve complète dans près de 41 % du temps.

Pour renforcer le succès 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, et a constaté que le taux de preuve avait augmenté jusqu’à 47,5 %. 

Cela signifie que Baldur est capable de prendre le contexte et de l’utiliser pour prédire une nouvelle preuve correcte, explique First. Semblable à un programmeur qui peut être mieux équipé pour corriger un bug dans une méthode lorsqu’il sait comment cette méthode est liée à son code environnant et aux autres méthodes de la même classe, Baldur peut mieux fonctionner avec un contexte supplémentaire.

Thor , l’outil de pointe actuel pour la génération automatique de preuves, a un taux de preuve plus élevé, soit 57 %. L’avantage de Baldur réside dans sa capacité à générer des preuves complètes ; Thor prédit la prochaine étape d’une preuve en utilisant un modèle de langage plus petit combiné à une méthode qui recherche l’espace des preuves possibles. Mais lorsque Thor et Baldur ( le frère de Thor dans la mythologie nordique) travaillent ensemble, ils peuvent générer des preuves correctes dans près de 66 % du temps.

L’équipe a également découvert que Baldur peut « réparer » ses propres preuves, améliorant ainsi encore son taux de preuves. Lorsqu’on lui fournit sa précédente tentative ratée ainsi que le message d’erreur renvoyé par Isabelle, Baldur peut transformer sa fausse preuve en une bonne.

« Le fait que le message d’erreur ait été si utile était surprenant », déclare Yuriy Brun. «[Cela] suggère qu’il existe des informations plus utiles qui pourraient potentiellement être introduites dans le grand modèle de langage pour donner de meilleures réponses. Nous ne faisons qu’effleurer la surface.

L’équipe n’a pas encore trouvé la bonne quantité d’informations qui seraient jugées utiles pour le modèle. « Une des limites est que nous lui donnons des informations sur la preuve qu’il essaie de générer, mais nous ne savons pas quelle est la limite et où cela cesse d’être utile », explique Yuriy Brun. Et il existe encore un degré d’erreur considérable, qui, espère-t-il, pourra être amélioré en affinant le modèle en utilisant davantage d’ensembles de données qui expliquent mieux à quoi ressemble une preuve et à quoi ressemblent une paire théorème et preuve.

Cet organigramme montre comment le modèle de réparation de preuve crée de nouvelles données de formation pour Baldur. 

En ce qui concerne les prochaines étapes, First envisage de mettre en œuvre l’approche utilisée pour Baldur dans d’autres assistants de preuve, ainsi que de découvrir des moyens de collecter plus intelligemment des informations contextuelles pouvant contribuer à améliorer la précision du modèle. L’équipe envisage que Baldur aide à simplifier le travail des ingénieurs de preuve , qui sont chargés, par exemple, de la vérification formelle des systèmes de sécurité nationale dans des organisations comme le département américain de la Défense et sa Defense Advanced Research Projects Agency (DARPA).

À plus grande échelle, l’équipe prévoit d’obtenir les commentaires des développeurs de logiciels pour voir comment des outils comme Baldur peuvent les aider, que ce soit en déboguant une erreur dans leur code, en affinant les spécifications ou en créant un système de meilleure qualité.

« Il est très utile de créer des outils interactifs dans lesquels un développeur tente de prouver certaines propriétés de son code », explique Yuriy Brun. « Comprendre comment les développeurs peuvent interagir avec ces outils et les soutenir en créant des approches automatisées peut les amener encore plus loin. »

https://spectrum.ieee.org/ai-debug-software