Présentation succincte
Je suis Professeur des Universités à l’école d’ingénieurs ENSEIRB-MATMECA de Bordeaux INP, et j’effectue ma recherche dans le département Méthodes et Modèles Formelles, M2F au laboratoire d’informatique de Bordeaux, le (laBRI) à l’Université de Bordeaux, depuis 2013. Depuis 2024, je suis également l’un des 180 conseillers régionaux au CESER de Nouvelle-Aquitaine, la seconde chambre régionale (membre qualifié, commission économie, mandature 2024-2030).
L’IA et la formation : de l’université au monde professionnel
Cela fait maintenant plus de deux ans que, avec la chaire IA Digne de Confiance, je suis sollicité pour faire...
C’est avec un très grand plaisir que nous venons d’apprendre l’acceptation définitive (et la publication) d’un article dans Nature npj...
Depuis la rentrée 2021, je suis en charge du département informatique de l’ENSEIRB-MATMECA , une des écoles d’ingénieurs du groupe Bordeaux INP, elle-même membre du réseau national d’école d’ingénieurs INP.
Du point de vue animation de la recherche, mes principales occupations actuelles peuvent se résumer ainsi :
- Porteur d’une chaire industrielle, grâce à la Fondation Bordeaux Université, sur l’IA Digne de Confiance. C’est un projet avec de nombreux financements à la clé pour les étudiants et les collègues. Il a démarré en septembre 2022. N’hésitez pas à visiter le site officiel de la chaire.
- Co-animateur (avec Akka Zemmari) de l’Axe transverse I.A. du LaBRI
- Président de l’Association Française de Programmation par Contraintes (2019-2024)
- Editeur Associé du journal JAIR (Journal of Artificial Intelligence Research) depuis 2021.
- Membre du Comité Editorial du journal ouvert Francophone Revue Ouverte d’Intelligence Artificielle, créée à la suite de la disparition de feu RIA (suite à une vente très discutable du nom de la revue de la part de l’éditeur Elsevier à un éditeur sans morale scientifique)
- Co-éditeur du journal JSAT sur la satisfiabilité
- Porteur de deux projets nationaux (ANR-BLANC) sur SAT (révolus)
Précédemment, j’étais membre du LRI, le Laboratoire d’Informatique de l’Université d’Orsay Paris 11 (à l’époque, maintenant connue sous le nom de Université Paris Saclay), dans le groupe de recherche Intelligence Artificielle et Systèmes d’Inférence (IASI).
Sujets de recherche
Mes principales activités de recherche sont menées au (laBRI) (voir photo ci-dessus). Je m’intéresse aux algorithmes et outils efficaces pour le raisonnement logique, principalement autour de la résolution pratique de la résolution du problème SAT et autour de SAT. Ces outils s’appuient sur les fondements de l’Intelligence Artificielle (impliquant du raisonnement) pour offrir des garanties (qualité, explicabilité, reproduction, complétude, …) sur les décisions qu’elles peuvent recommander. Par ailleurs, du fait des progrès impressionnants obtenus ces dernières années par ces outils, et les bijoux algorithmiques qu’ils recèlent, on les retrouve souvent au coeur de nombreuses méthodes de vérifications formelles de systèmes, voire au coeur des méthodes permettant d’expliquer ou de garantir des propriétés de systèmes de décision de type boites noires (comme les réseaux de neurones).
Je m’intéresse également aux problématiques d’efficacité pour la manipulation et l’exploitation de bases de connaissances, comme la génération efficace d’Impliqués/Impliquants Premiers et la Compilation de Base de Connaissances au sens général, avec un fort appétit pour l’étude expérimentale des outils d’IA qui s’attaquent aux problèmes fortements combinatoires. J’ai également eu l’occasion de travailler
sur des approches décentralisées de certains de ces sujets (raisonnement
sur les réseaux P2P et sociaux, garantie de diagnosticabilité de systèmes décentralisés, …). Depuis quelques années, je travaille sur l’IA de confiance, en particulier dans le contexte de décisions critiques ou lorsqu’une explication est nécessaire. Pour aborder ces problèmes, la logique et les méthodes formelles s’avèrent essentielles.
Plus récemment, je me suis tourné vers la détection de dérives de modèles issus de l’apprentissage.
A propos du solveur SAT Glucose
Glucose est un solveur (démonstrateur) SAT basé sur un mécanisme de mesure de la pertinence des clauses apprises par les solveurs, basé sur le papier publié à IJCAI avec Gilles Audemard. Le nom du solveur vient du concept de “glue clauses”, des clauses qui permettent d’attacher systématiquement un nouveau littéral aux propagation du solveur, d’où “glueclause, gluclause, glucose” (pardon). Glucose s’appuie très fortement sur le travail d’implantation remarkable des solveurs CDCL dans Minisat. Il est important de citer également Minisat si vous souhaitez citer Glucose.
Il y a une page dédiée au solveur Glucose. En 2022, on a décidé, avec Gilles A. de simplifier le code et de le rendre plus efficace (à suivre !).
SAT en deux mots
Le problème SAT (test de satisfiabilité) est l’un des plus importants problèmes en informatique théorique. Intuitivement, ce problème capture la complexité inhérente aux problèmes les plus simples qui demeurent difficiles à résoudre en pratique. Un problème difficile, c’est un problème pour lequel calculer la solution est faisable, mais cela vous demanderait beaucoup trop de temps (typiquement bien bien plus que l’age de l’univers). Si vous voulez en savoir plus, je ne peux que vous conseiller de prendre votre prochain avec la page Wikipedia qui parle de SAT .