Alors que les systèmes autonomes et l’intelligence artificielle deviennent de plus en plus courants dans la vie quotidienne, de nouvelles méthodes apparaissent pour aider les humains à vérifier que ces systèmes se comportent comme prévu. Une méthode, appelée spécifications formelles, utilise des formules mathématiques qui peuvent être traduites en expressions en langage naturel. Certains chercheurs affirment que cette méthode peut être utilisée pour expliquer les décisions qu’une IA prendra d’une manière interprétable par les humains.

Les chercheurs du MIT Lincoln Laboratory voulaient vérifier ces affirmations d’interprétabilité. Leurs résultats indiquent le contraire : les spécifications formelles ne semblent pas interprétables par les humains. Dans l’étude de l’équipe, il a été demandé aux participants de vérifier si le plan d’un agent IA réussirait dans un jeu virtuel. Lorsqu’on leur a présenté les spécifications formelles du plan, les participants ont eu raison dans moins de la moitié du temps.

« Ces résultats sont une mauvaise nouvelle pour les chercheurs qui prétendent que les méthodes formelles confèrent une interprétabilité aux systèmes. Cela pourrait être vrai dans un sens restreint et abstrait, mais pas pour quoi que ce soit qui se rapproche de la validation pratique du système », déclare Hosea Siu, chercheur au du laboratoire Groupe de technologie IA. Celui du groupe papier a été accepté à la Conférence internationale 2023 sur les robots et systèmes intelligents qui s’est tenue au début du mois.

L’interprétabilité est importante car elle permet aux humains de faire confiance à une machine lorsqu’elle est utilisée dans le monde réel. Si un robot ou une IA peut expliquer ses actions, les humains peuvent alors décider s’ils ont besoin d’ajustements ou s’ils peuvent leur faire confiance pour prendre des décisions équitables. Un système interprétable permet également aux utilisateurs de la technologie – et pas seulement aux développeurs – de comprendre et de faire confiance à ses capacités. Cependant, l’interprétabilité constitue depuis longtemps un défi dans le domaine de l’IA et de l’autonomie. Le processus d’apprentissage automatique se déroule dans une « boîte noire », de sorte que les développeurs de modèles ne peuvent souvent pas expliquer pourquoi ou comment un système a pris une certaine décision.

« Lorsque les chercheurs disent « notre système d’apprentissage automatique est précis », nous demandons « dans quelle mesure ? » et « en utilisant quelles données ? » et si ces informations ne sont pas fournies, nous rejetons l’affirmation. Nous n’avons pas fait grand-chose lorsque les chercheurs disent que « notre système d’apprentissage automatique est interprétable » et nous devons commencer à soumettre ces affirmations à un examen plus approfondi », déclare Siu. .

Perdu dans la traduction

Pour leur expérience, les chercheurs ont cherché à déterminer si les spécifications formelles rendaient le comportement d’un système plus interprétable. Ils se sont concentrés sur la capacité des utilisateurs à utiliser de telles spécifications pour valider un système, c’est-à-dire pour comprendre si le système répondait toujours aux objectifs de l’utilisateur.

L’application de spécifications formelles à cette fin est essentiellement un sous-produit de son utilisation initiale. Les spécifications formelles font partie d’un ensemble plus large de méthodes formelles qui utilisent des expressions logiques comme cadre mathématique pour décrire le comportement d’un modèle. Étant donné que le modèle est construit sur un flux logique, les ingénieurs peuvent utiliser des « vérificateurs de modèles » pour prouver mathématiquement des faits sur le système, y compris lorsqu’il est ou non possible pour le système d’accomplir une tâche. Aujourd’hui, les chercheurs tentent d’utiliser ce même cadre comme outil translationnel pour les humains.

« Les chercheurs confondent le fait que les spécifications formelles ont une sémantique précise et qu’elles sont interprétables par les humains. Ce n’est pas la même chose », explique Siu. « Nous avons réalisé que presque personne ne vérifiait si les gens comprenaient réellement les résultats. »

Dans l’expérience de l’équipe, il a été demandé aux participants de valider un ensemble de comportements assez simples avec un robot jouant à un jeu de capture du drapeau, en répondant essentiellement à la question « Si le robot suit exactement ces règles, est-il toujours gagnant ? »

Les participants comprenaient à la fois des experts et des non-experts en méthodes formelles. Ils ont reçu les spécifications formelles de trois manières : une formule logique « brute », la formule traduite en mots plus proches du langage naturel et un format d’arbre de décision. Les arbres de décision en particulier sont souvent considérés dans le monde de l’IA comme un moyen interprétable par l’homme de montrer la prise de décision de l’IA ou des robots.

Les résultats : « Les performances de validation dans l’ensemble étaient assez médiocres, avec une précision d’environ 45 %, quel que soit le type de présentation », explique Siu.

En toute confiance faux

Ceux précédemment formés aux spécifications formelles n’ont que légèrement mieux réussi que les novices. Cependant, les experts ont déclaré avoir beaucoup plus confiance dans leurs réponses, qu’elles soient correctes ou non. Dans l’ensemble, les gens avaient tendance à faire trop confiance à l’exactitude des spécifications qui leur étaient présentées, ce qui signifie qu’ils ignoraient les règles autorisant les pertes de jeu. Selon les chercheurs, ce biais de confirmation est particulièrement préoccupant pour la validation du système, car les gens sont plus susceptibles de négliger les modes de défaillance.

« Nous ne pensons pas que ce résultat signifie que nous devrions abandonner les spécifications formelles comme moyen d’expliquer les comportements du système aux gens. Mais nous pensons qu’il reste encore beaucoup de travail à faire dans la conception de la façon dont elles sont présentées aux gens et dans le flux de travail dans lequel les gens les utilisent », ajoute Siu.

En réfléchissant aux raisons pour lesquelles les résultats ont été si médiocres, Siu reconnaît que même les personnes qui travaillent sur des méthodes formelles ne sont pas suffisamment formées pour vérifier les spécifications comme le leur demandait l’expérience. Et il est difficile de réfléchir à tous les résultats possibles d’un ensemble de règles. Malgré cela, les règles présentées aux participants étaient courtes, équivalentes à un paragraphe de texte, « beaucoup plus courtes que tout ce que vous rencontreriez dans n’importe quel système réel », explique Siu.

L’équipe ne tente pas de lier directement ses résultats aux performances des humains lors de la validation de robots dans le monde réel. Au lieu de cela, ils visent à utiliser les résultats comme point de départ pour examiner ce qui peut manquer à la communauté de la logique formelle lorsqu’elle revendique l’interprétabilité, et comment de telles affirmations peuvent se concrétiser dans le monde réel.

Cette recherche a été menée dans le cadre d’un projet plus vaste sur lequel Siu et ses coéquipiers travaillent pour améliorer la relation entre les robots et les opérateurs humains, en particulier ceux de l’armée. Le processus de programmation de la robotique peut souvent laisser les opérateurs à l’écart. Dans le même but d’améliorer l’interprétabilité et la confiance, le projet tente de permettre aux opérateurs d’enseigner directement des tâches aux robots, d’une manière similaire à la formation des humains. Un tel processus pourrait améliorer à la fois la confiance de l’opérateur dans le robot et l’adaptabilité du robot.

En fin de compte, ils espèrent que les résultats de cette étude et leurs recherches en cours pourront améliorer l’application de l’autonomie, à mesure qu’elle s’intègre davantage dans la vie humaine et la prise de décision.

« Nos résultats soulignent la nécessité de procéder à des évaluations humaines de certains systèmes et concepts d’autonomie et d’IA avant que trop d’affirmations ne soient faites sur leur utilité chez les humains », ajoute Siu.