Un nouvel « entretien autour de l’informatique », celui de Daniel Le Berre, Médaille CNRS de l’Innovation 2018, enseignant-chercheur en informatique à l’Université d’Artois, au Centre de recherche en informatique de Lens. Daniel Le Berre est l’initiateur et le développeur principal du solveur Sat4j, un logiciel libre utilisé par des millions de personnes à travers le monde. Cet article est publié en collaboration avec le Blog Binaire.
Binaire : tu es chercheur en intelligence artificielle. Comment devient-on chercheur en IA ?
D. L. B. : Je suis un pur produit de l’Université. Je n’avais aucune idée de ce qu’était le métier d’enseignant-chercheur avant d’en rencontrer à la fac à Brest. J’ai été particulièrement impressionné par la diversité des connaissances en informatique de mes enseignants en licence et maîtrise d’informatique et je me suis dit : quel métier formidable ; je veux faire ça ! Cela m’a donné envie de faire une thèse. J’ai choisi l’informatique car j’aime depuis le collège utiliser des ordinateurs (on avait un Bull Micral 30 à la maison pour faire la comptabilité de la ferme). Je suis de cette génération qui a eu la chance d’une initiation à l’informatique au lycée. Ça a disparu ensuite pour n’être réinstallé que depuis peu. Après Brest, je suis parti à Toulouse pour sa réputation en intelligence artificielle. C’est là que j’ai découvert le problème SAT autour duquel j’ai travaillé depuis. Après ma thèse, je suis parti en post-doc en Australie, c’est à cette période que j’ai découvert la conférence SAT au cours d’un atelier à Boston en 2001. Quelques semaines après mon arrivée à Lens en septembre 2001, on me proposait de co-organiser la compétition SAT. J’avais plongé dans le grand bain, le bain des grands !
On ne va pas faire durer plus le suspense. Si tu nous disais ce que c’est que ce fameux problème SAT, sans doute le problème le plus étudié en informatique.
Le problème SAT est un problème parmi les plus simples des problèmes compliqués.
Imaginez un immeuble avec des pièces éclairées par des ampoules. Chaque ampoule peut être éclairée par un ou plusieurs interrupteurs, dans une position donnée (ouvert ou fermé). Chaque interrupteur peut contrôler une ou plusieurs ampoules, et on connaît pour chaque ampoule les interrupteurs associés. Les interrupteurs sont au pied de l’immeuble. On cherche à éclairer toutes les pièces de l’immeuble. Ce n’est pas toujours possible (par exemple si l’on dispose de deux pièces reliées chacune seulement à une position différente de l’interrupteur, on ne pourra jamais éclairer les deux pièces en même temps). Dès que l’on associe plus de 2 interrupteurs à une ampoule, ce problème est difficile.
Un algorithme simple permet de résoudre le problème. On met tous les interrupteurs à off et on essaie. Si ça ne marche pas, on essaie ensuite toutes les configurations possibles avec un seul interrupteur à on, puis deux… Si j’ai 3 interrupteurs, cela fait 8 configurations à tester ; avec 4, ça en fait 16… À chaque interrupteur que j’ajoute, je double le nombre de configurations à tester. On vous parle souvent de croissance exponentielle dans les journaux. Là c’est vraiment exponentiel. C’est vite effrayant : dès que le nombre d’interrupteurs est plus grand que 270, le nombre de configurations à tester est plus grand que le nombre d’atomes dans l’univers !
SAT est une abréviation pour boolean SATisfiability problem ou en français SATisfaisabilité de formules booléennes. En résumé, on nomme problème SAT un problème de décision visant à savoir s’il existe une solution à une série d’équations logiques données. Un algorithme qui résout le problème SAT est appelé un solveur SAT. Je suis un spécialiste de ces solveurs SAT.
SAT est un problème très branché en informatique. Pourquoi ? À quoi ça sert de le résoudre ?
La raison de sa popularité est qu’il sert de problème pivot pour résoudre beaucoup d’autres problèmes : on traduit le problème original en SAT, on utilise un solveur SAT pour obtenir une réponse, et ensuite on interprète ce résultat par rapport au problème original. Cela fait des solveurs SAT des outils de résolution de problèmes combinatoires génériques.
L’application la plus visible du problème SAT est la vérification de processeurs. C’est cette application qui a motivé à la fin des années 90 la conception des solveurs SAT modernes, capable de résoudre des problèmes avec des millions d’interrupteurs. Un autre problème a donné lieu à beaucoup de travaux en intelligence artificielle au début des années 1990, celui de la planification : choisir quelles actions effectuer pour atteindre un but étant données une situation initiale et une description des actions possibles. Des chercheurs ont montré qu’ils arrivaient à résoudre super efficacement le problème de planification avec des solveurs SAT. En fait, il y a tout un paquet de problèmes différents que l’on rencontre en pratique qui demandent des techniques semblables. On se rend compte pour une liste croissante de ces problèmes qu’une approche générique par traduction à SAT est plus efficace qu’une approche dédiée. Cela s’explique notamment par les performances impressionnantes des solveurs SAT actuels.
Le problème SAT est posé sur des variables qui valent 0 ou 1 (les positions des interrupteurs, on ou off). C’est simple un booléen et c’est facile à réaliser sur un ordinateur. Du coup, on peut réaliser des solveurs vraiment bien optimisés. On a par exemple inventé des structures de données super intelligentes pour mémoriser ce qu’on a déjà appris ou ce qu’il nous reste à apprendre du problème posé. Et cela compense largement le fait qu’au lieu de travailler directement sur le problème original, comme la planification, on bosse sur une représentation du problème avec SAT.
Le problème est finalement assez simple mais il faut se montrer très intelligent pour le résoudre rapidement. Il faut trouver des raisonnements plus intelligents que ceux consistant par exemple à vérifier l’une après l’autre les solutions possibles.
On fait même des trucs de plus en plus compliqués, comme de faire causer un solveur SAT qui cherche à trouver une solution et un autre qui essaie de montrer qu’il n’y en a pas.
Tu as reçu la médaille de l’innovation pour tes travaux sur le solveur SAT4j. Que fait ce solveur en particulier ?
SAT4j est mon troisième solveur SAT en Java, un langage de programmation très populaire chez les développeurs, mais pas dans la communauté SAT. Java n’est pas considéré comme particulièrement rapide alors que la rapidité est le cœur du sujet pour un solveur SAT, parce qu’il y a énormément de choses à calculer à l’intérieur. Alors, ça peut sembler une drôle d’idée de développer un solveur SAT en Java. Pourtant, Java est utilisé par des gens d’horizons divers. Il n’y a pas de raisons pour que les programmeurs Java, et c’est une énorme communauté, soient exclus de la technologie des SAT solveurs, que cette techno soit réservée aux programmeurs d’autres langages ! SAT4j a été conçu pour la communauté Java, pour y diffuser les avancées de la communauté SAT, et en appliquant les principes du génie logiciel que j’enseigne à mes étudiants. Depuis juin 2008, la plate-forme ouverte Eclipse, souvent connue comme un environnement de développement de logiciel mais encore plus utilisée par de nombreuses sociétés comme base de leurs outils, s’appuie d’ailleurs sur Sat4j pour résoudre « ses dépendances logicielles » : savoir quels composants sont nécessaires pour ajouter une fonctionnalité particulière, sachant qu’ils ne sont pas tous compatibles. Du coup, Sat4j est sans doute le solveur SAT le plus utilisé dans le monde.
J’ai juste mis les résultats d’une communauté scientifique à la portée d’un public très large.
Quand on parle d’IA aujourd’hui, on veut souvent dire apprentissage automatique ou réseaux de neurones. Ton IA à toi se situe ailleurs. Où ?
Mon labo est spécialisé en « Intelligence artificielle symbolique » : on formalise le raisonnement, en particulier le raisonnement mathématique. Cela nous permet de faire des outils qui obtiennent automatiquement des preuves. Les solveurs SAT permettent d’obtenir des raisonnements dans une logique très pauvre. Mais nous nous intéressons aussi à des raisonnements dans des logiques plus sophistiquées, en rajoutant des ingrédients aux fils et interrupteurs de départ. Nous sommes là en plein dans l’intelligence artificielle.
Un avantage par rapport aux approches d’apprentissage statistique, c’est qu’avec l’IA symbolique, on peut expliquer les résultats : on dispose des étapes du raisonnement, des preuves, ce qu’on n’a pas avec les résultat d’un réseau neuronal. Évidemment, quand on n’y arrive plus avec l’IA symbolique, on peut essayer avec de l’apprentissage automatique. Dans de nombreuses applications, on combine d’ailleurs ces deux types d’approches.
Quand j’étais en thèse je faisais un truc qui ne servait à personne, qui n’était pas du tout sexy à l’époque, car on ne pouvait résoudre que des problèmes avec quelques centaines d’interrupteurs. Cependant, chacun apportait sa contribution à l’enrichissement des connaissances, qu’elles soient théoriques ou pratiques. En 2001, à partir de toutes les connaissances accumulées jusque-là, des étudiants de master de Princeton ont fait progresser considérablement le domaine en construisant un solveur fondé sur un excellent compromis entre complexité et efficacité. Il y a vraiment eu un avant et un après ce solveur. Cela a permis de résoudre certains problèmes avec des dizaines de milliers d’interrupteurs, une vraie révolution pour l’informatique. L’apprentissage automatique a apporté une autre révolution, beaucoup plus médiatisée celle-là.
Mais l’intelligence artificielle a de nombreuses facettes. Attendez-vous à voir arriver d’autres révolutions en informatique.