2020 | vrAI: FOrmal VeRification and AI

Axe : IID, Scilex
Coordinateurs : Guillaume Charpiat, équipe TAU, LRI / INRIA Saclay
Zakaria Chihani, équipe LSL, CEA-List/Saclay
Laboratoire gestionnaire : Inria SIF
Autres laboratoires impliqués : LIST, LRI, LSV, LTCI
Équipes concernées et liste des participants :
LRI / INRIA Saclay via l’équipe TAU : Guillaume Charpiat, Michèle Sébag
LSV : Stefan Haar, Benedikt Bollig, Alain Finkel, Serge Haddad
CEA-list : Zakaria Chihani
LTCI : Florence d’Alché-Buc


Présentation :

Ce groupe de travail interdisciplinaire s’intéresse aux interactions entre
l’apprentissage statistique et aux méthodes formelles de certification, à savoir d’une part la certification formelle de modèles appris (par une tâche de machine learning), et d’autre part l’aide que pourrait apporter l’apprentissage statistique aux méthodes formelles, comme par exemple l’accélération de prouveurs via un guidage heuristique par du machine learning. L’apprentissage statistique, sous sa forme classique (méthodes à noyaux, forêts aléatoires, etc.) comme sous sa forme néo-connexioniste en vogue (réseaux de neurones profonds), connait des succès spectaculaires, mais n’offre jamais de garantie sur les modèles appris, autre que statistique. Les critères optimisés lors de l’apprentissage de modèles portent en effet sur l’efficacité statistique de ceux-ci (sur de nombreux échantillons), mais il n’est généralement pas possible de contruire de spécification formelle de ce que devrait accomplir le modèle: pour une tâche de détection de chats dans des photos, aucune spécification de ce à quoi ressemble un chat n’est fournie; c’est d’ailleurs là que réside l’intérêt de l’apprentissage statistique pour les tâches de perception: apprendre ce à quoi un chat ressemble, car le modéliser manuellement serait bien difficile. Cependant, pour certaines applications de l’apprentissage statistique, comme la conduite de véhicule autonome, l’obtention de garanties (de ne pas écraser de piéton, par exemple) est très critique. Comment faire pour formuler et obtenir des garanties tout de même? sachant que les modèles appris souffrent de manque criant de robustesse, comme le montrent les attaques adverses? Tout un pan de la recherche en machine learning est depuis quelques années consacré à ce sujet, en vue d’augmenter la robustesse des modèles appris, ou de certifier ceux-ci. Les méthodes formelles classiques n’étant pas très adaptées à des programmes de type “réseaux de neurones”, de nouvelles astuces ou approches spécifiques aux réseaux de neurones fleurissent dans la littérature ces dernières années. Pour suivre ces évolutions, les comprendre profondément et en proposer de nouvelles, des
compétences des deux côtés (apprentissage statistique et méthodes formelles) sont requises, et un groupe de lecture commun est nécessaire.
Dans l’autre sens, l’apprentissage statistique peut également aider le champ des méthodes formelles. Par exemple, dans le champ des preuves formelles de théorèmes, la complexité des algorithmes pour trouver une preuve peut être gigantesque, le problème étant de nature combinatoire, la recherche de preuve se faisant sur l’arbre généralement profond et large des combinaisons possibles d’axiomes. Toutefois, de bonnes heuristiques peuvent réduire fortement l’espace des possibilités à explorer; de bonnes heuristiques apprises ne peuvent qu’accélérer davantage les prouveurs. Par ailleurs, la question de l’exploration efficace d’un arbre d’actions possibles est un des pans de l’apprentissage par renforcement, celui qui a conduit aux succès des fameux AlphaGo et AlphaStar, qui battent désormais les humains au jeu de Go et à StarCraft. Plus généralement, tout prouveur utilisant des heuristiques est potentiellement améliorable par du machine learning. Là encore, pour ce faire, une collaboration étroite entre les deux communautés est nécessaire, d’où ce groupe de travail.