Apprentissage Automatique pour la recherche SAT

Nouvelles les plus récentes

(Liste de toutes les brèves)

Glucose est (enfin) sur Github

(17 Mai 2023)

Glucose est enfin (aussi) distribué sur Github. L’idée est tout simplement de permettre les forks officiels depuis les versions de glucose. Nous le distribuions uniquement via des archives et la...


Interview dans Sud-Ouest autour de l'I.A. de confiance

(3 Mai 2023)

L’I.A. est le sujet de nombreux articles de presse depuis quelques mois. L’exposition au grand public d’outils comme chatGPT4 accèlère encore plus le besoin d’explication et de compréhension de ces...


Séjour au Simons Institute (Berkeley)

(17 Avril 2023)

Dans le cadre du programme d’invitation du Simons Institute au sujet de SAT (SAT Reunion Semester), j’ai eu le plaisir d’être invité sur un séjour long dans ce lieu mythique...


Mise en route du projet CAP-IA

(1 Avril 2023)

Le projet CAP-IA, porté par François Clautiaux (IMB) et l’Université de Bordeaux, accepté en Novembre dernier est enfin lancé. C’est un projet ambitieux dont je porte le volet en lien...


Lancement du projet Européen DIHNAMIC

(20 Mars 2023)

Le projet Dihnamic vient d’être lancé très officiellement. C’est un projet européen et régional de grande ampleur dans lequel je suis membre de “l’advisory board”. Le projet réunit 13 partenaires....

Sujet de Master 2 Recherche en Intelligence Artificielle

Démarrage Février 2023

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é)

Le sujet est associé à la l’élaboration d’une thèse CIFRE avec la société TALAN

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, par les firmes les plus puissantes qui aient jamais été créées (Google, Microsoft, Tesla, Microsoft, Amazon, NVidia, Intel,…). 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 grappes de calcul a également permis d’envisager des techniques d’apprentissage qui découvrent progressivement ce qui doit être appris. 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 de la 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 en reconnaissance de formes et en analyse de signaux (son, image, vidéo, ….) et de textes, 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 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 donc 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. 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). Son apparente simplicité permet le développement d’algorithmes compacts et efficaces - en pratique - pour attaquer toute une classe de problèmes importants, mais insolubles - en théorie -. Edmund Clarke, l’un des lauréats du prix Turing 2007 (et utilisateur de démonstrateurs SAT) a déclaré que “la résolution pratique du problème SAT est une technologie clé pour l’informatique du 21e siècle”. D. Knuth, dans sa brochure sur le SAT, a écrit : “L’histoire de la satisfiabilité est l’histoire d’un triomphe de l’ingénierie logicielle, mélangé à de riches doses de belles mathématiques. Grâce à de nouvelles structures de données élégantes et à d’autres techniques, les solveurs SAT modernes sont capables de traiter couramment des problèmes pratiques impliquant plusieurs milliers de variables, alors que de tels problèmes étaient considérés comme désespérés il y a seulement quelques années”. Il est également important de souligner que 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 25 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.

Le stage peut démarrer dès Février 2023.

Contact: Laurent Simon