Vers la vérification et certification d'algorithmes d'intelligence artificielle

点击翻译按钮获取中文摘要

Nous voulons développer des outils d'analyse formels pour la certification d'agorithmes d'apprentissage automatique (Machine Learning en Anglais), et autres algorithmes d'intelligence artificielle. Il s'agit ici de certifier avec des garanties très fortes, qui pourront permettre d'établir les conditions dans lesquelles des systèmes critiques pourraient utiliser des intelligences artificielles. Le premier axe de recherche sera l'analyse des algorithmes d'intelligence artificielle une fois entrainés. Une difficulté dans l'analyse d'un prédicteur entraîné par des techniques d'intelligence artificielle est de spécifier l'effet des entrées qu'on lui donne durant l'apprentissage ou pendant son utilisation. Il est également important d'arriver à décrire son comportement en termes de données abstraites et de variables abstraites. Nous proposons d'analyser des prédicteurs dans des domaines où des simulateurs (stochastiques) puissants et certifiés d'être représentatifs du monde réel sont disponibles, ce qui est le cas par exemple en aéoronautique. Dans ces situations, les prédicteurs sont à la fois entraînés et utilisés avec des données du simulateur car celles-ci sont très proches des données réelles. Cette situation est intéressante pour la vérification formelle car comme un système certifié fait très peu (ou pas) d'erreur et comme on a accès dans ce domaine à des simulateurs de grande capacité, on pourra utiliser le système certifié comme un modèle de la spécification et tenter de vérifier l'algorithme d'apprentissage en le comparant à ce modèle. Le deuxième axe du programme sera une analyse des algorithmes d'apprentissage pendant leur entraînement, toujours dans l'optique d'utiliser les méthodes formelles, donc de créer des garanties rigoureuses. Il y a beaucoup de recherche et d'avancées sur les réseaux de neurones profonds, par exemple, mais peu de compréhension théorique sur la façon dont ces systèmes fonctionnent. Un réseau de neurones est un transformateurs de distributions de probabilités, et nos travaux pourront éclairer autrement le domaine. Dans les 20 dernières années, mes collaborateurs et moi avons travaillé dans l'analyse des systèmes probabilistes. Nous avons obtenu un prix Test-of-time de la prestigieuse conférence LICS dans ce domaine. Nous proposons d'utiliser ces techniques sur différents systèmes d'intelligence artificielle, dont les processus de décision markoviens et les réseaux de neurones profonds. Les notions pertinentes ici, sont : notions d'équivalence de systèmes, métriques qui mesurent à quel point deux systèmes sont similaires ou non, techniques d'approximations des systèmes probabilistes ayant un ensemble infini non dénombrable d'états.