Démarrage Février 2025
Thèmes de recherche en lien avec le sujet Apprentissage Automatique, Apprentissage par Renforcement, SAT, Logique, Programmation par Contraintes, I.A. de Confiance
Localisation: LaBRI, Laboratoire Bordelais de Recherche en Informatique, Talence, France
(Ce stage de Master est financé par la chaire “IA digne de Confiance”, portée par Laurent Simon et supporté par la Fondation Bordeaux Université)
Description du projet de master proposé
L’apprentissage automatique (ML) est probablement le domaine de l’intelligence artificielle (IA) qui a le plus contribué aux progrès observés en IA ces dernières années, renouvelant un fort enthousiasme pour ce domaine, né il y a plus de 65 ans. Ces résultats impressionnants sont dus à de multiples facteurs. Outre une meilleure connaissance des forces et faiblesses des algorithmes d’apprentissage, l’écosystème ML s’est massivement tourné vers la production d’outils puissants et ouverts, exploitant dans les meilleures conditions possibles les dernières avancées du matériel mis à disposition. Mieux encore, le matériel a évolué notamment pour les tâches dites de Deep Learning (DL) et des machines spécialisées, ou des cartes de calcul dédiées, sont apparues, permettant l’apprentissage sur des volumes de données gigantesques. L’accessibilité des grandes clusters de calcul a également permis d’envisager des techniques d’apprentissage permettant d’apprendre des stratégies nouvelles. Ces techniques, regroupées sous les principes généraux de l’apprentissage par renforcement (RL), ne considèrent que les actions autorisées, les états possibles d’un système donné et les relations entre eux. Ensuite, guidé par une fonction de récompense spécifique, le système apprend, par lui-même, les actions à entreprendre pour maximiser les récompenses attendues de tout état initial. Les progrès obtenus en RL sont également remarquables dans de nombreux domaines. Par exemple, Alphago, même s’il intègre des algorithmes plus classiques d’exploration d’arbres de jeux, qui ne sont pas appris, est probablement l’exemple le plus frappant de l’ampleur des progrès observés dans le domaine.
Cependant, malgré ces résultats époustouflants (ayant mêmem valu un prix Nobel en Chimie), les approches basées sur le ML / RL n’ont pas encore réussi à surpasser les méthodes conventionnelles dans la résolution de problèmes NP-Difficiles. Cette classe de problèmes, au centre de l’informatique théorique, capture la difficulté de nombreux sous-domaines de l’IA depuis ses débuts, comme la planification, la programmation par contraintes, ou même le problème SAT lui-même (SAT signifie “Test de Satisfiabilité”).
Si le domaine ML peut être qualifié d’IA “statistique” (les approches peuvent souvent être réduites à la recherche de corrélations dans les événements observés), le domaine SAT est, quant à lui, au cœur de nombreuses approches d’IA “symbolique”. Son caractère “symbolique “ vient du fait que ce problème repose principalement sur la manipulation de symboles logiques dotés d’une sémantique précise.
L’objectif de ce stage de Master 2 est d’étudier comment les progrès récents en ML / RL peuvent nous permettre d’envisager l’utilisation et l’extension des techniques ML / RL pour la résolution pratique du problème SAT.
Le problème SAT est basé sur la logique propositionnelle, ce qui lui permet d’être au cœur de toute une classe de problèmes équivalents (en difficulté) en IA, dès lors qu’ils sont basés sur un raisonnement logique. D’apparence extrêmement simple, cette logique s’adapte parfaitement à la force de calcul brute des machines actuelles, tout en offrant un panel de solutions pragmatiques à tout un ensemble de problèmes fondamentaux d’Intelligence Artificielle (IA). La recherche sur la résolution pratique du SAT est particulièrement active. Ainsi, chaque année, la communauté organise des concours pour évaluer les progrès et les défis. Jusqu’à quarante équipes peuvent y participer, impliquant plus de cinquante démonstrateurs dans les compétitions. L’un des principaux paradigmes de recherche autour du SAT consiste à s’appuyer sur la vitesse de calcul des machines pour leur permettre de parcourir extrêmement rapidement l’espace de recherche de solutions. Cela implique le déploiement d’heuristiques de décision extrêmement rapides, permettant aux résolveurs de prendre des centaines de milliers de décisions par seconde.
Il est donc naturel de remettre en cause ce paradigme en permettant aux résolveurs de s’appuyer sur des décisions plus lentes mais plus intelligentes grâce à l’application de méthodes ML / RL pour résoudre le problème.
Derrière cette idée apparemment naturelle se cache cependant un certain nombre de problèmes très difficiles, et relever ce défi signifie s’attaquer à des difficultés à l’intersection des fondements du RL/ML et de SAT.
L’approche que nous proposons d’étudier dans ce stage cherche à améliorer la recherche locale grâce à une modélisation plus ou moins directe des problèmes SAT en RNN (par exemple à base de réseaux de neurones sur graphes (GNN [1,2])). Cette méthode devrait permettre de changer le paradigme des solveurs SAT de recherche locale (LS), qui est basé sur des solveurs extrêmement rapides, ne prenant quasiment pas de temps pour les décisions (chaque décision inverse la valeur d’une variable, dans l’espoir d’atteindre une solution, ou de s’en rapprocher). Malheureusement, cette approche est confrontée à plusieurs problèmes. (1) chaque famille de problèmes SAT a ses propres caractéristiques, ce qui limite les capacités de généralisation des méthodes RL. (2) les temps d’inférence des prédictions NN sont beaucoup trop lents pour corriger leurs imprécisions. (3) la taille des instances à traiter peut varier de manière significative (de quelques centaines de variables à des millions), ce qui rend les modélisations fixes généralement utilisées dans les méthodes RL assez difficiles à mettre en oeuvre. (4) Les problèmes SAT ne peuvent pas être approchés localement, ce qui limite l’utilisation des GNNs. Ces points ont été identifiés dans [5] pour expliquer les raisons de l’échec relatif de ces méthodes dans le cadre du SAT. La difficulté rencontrée n’est pas surprenante : trouver une façon plus intelligente de naviguer dans le paysage des solutions par la recherche locale est un défi important pour la communauté depuis des années. Il s’agit en fait du défi 6, il y a presque 30 ans, proposé par B. Selman, H. Kautz et D. Mc Allister, dans “Ten Challenges in Propositional Reasoning and Search” (IJCAI’97) : Améliorer la recherche locale stochastique sur des problèmes structurés en traitant efficacement les dépendances sémantiques entre les variables. Ce défi n’a jamais été relevé avec succès. Jusqu’à présent, à de rares exceptions près, la recherche locale est restée confinée à des problèmes aléatoires, pour lesquels le paysage des solutions était bien connu.
Arriver à proposer un modèle, éventuellement guidé par le modèle appris par le moteur RL, dans le contexte de problèmes SAT industriels est donc un formidable défi que nous nous proposons d’étudier dans ce stage de Master.
Bibliographie
[1] How Powerful are Graph Neural Networks?, K. Xu, W. Hu, J. Leskovec, S. Jegelka, in Seventh International Conference on Learning Representations (ICLR, 2019)
[2] Learning Local Search Heuristics for Boolean Satisfiability, Emre Yolcu, Barnabas Poczos, NeurIPS 2019
[3] NeuroSAT: Learning a SAT Solver from Single-Bit Supervision, Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill (arxiv)
[4] Guiding High-Performance SAT Solvers with Unsat-Core Predictions, Daniel Selsam, Nikolaj Bjorner (arxiv)
[5] Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver? Kurin, Vitaly and Godil, Saad and Whiteson, Shimon and Catanzaro, Bryan, NeurIPS 2020
[6] On the Non-degeneracy of Unsatisfiability Proof Graphs Produced by SAT Solvers, Rohan Fossé, L. Simon, CP 2018
[7] The Glucose SAT Solver, Gilles Audemard, Laurent Simon, IJAIT’s Volume No.27, Issue No. 01.2018
Candidat
Le candidat devra avoir de solides connaissances en Apprentissage Automatique et en IA symbolique. Une très bonne connaissance de la programmation est également attendue.
Contact: Laurent Simon