Les professeurs Sylvain Hallé et Hugo Tremblay ont récemment publié un article à la conférence Computer Aided Verification (CAV), qui s’est tenue de manière virtuelle en juillet 2021. La conférence CAV compte parmi les meilleures dans le domaine de la vérification logicielle.

L’article, intitulé Foundations of Fine-Grained Explainability, définit les bases mathématiques d’un concept nommé “explicabilité”. De manière informelle, l’explicabilité peut être vue comme la manière de lier la sortie d’un calcul ou d’une opération aux éléments de l’entrée qui ont contribué à sa production. La particularité de leur contribution consiste en le fait que la relation d’explicabilité proposée est dite de granularité fine: il est possible de pointer une partie de la sortie (par exemple, un caractère dans un texte, un événement dans une séquence ou une cellule dans un tableau), et de retracer les parties précises de l’entrée qui lui sont associées.

Les notions théoriques mises de l’avant ont également été implémentées dans une librairie logicielle libre appelée Petit Poucet, faisant référence au personnage du conte de Charles Perreault qui laissait des cailloux derrière lui pour retrouver son chemin dans la forêt. À terme, ces concepts pourraient trouver des applications dans de nombreux domaines: on pourrait ainsi calculer automatiquement la raison pour laquelle une opération produit une certaine valeur à partir des données d’entrées, ou encore “expliquer” pourquoi une condition sur un système n’est pas respectée.

On peut voir ci-dessous la vidéo de la présentation donnée par Sylvain Hallé lors de la conférence.