Laurent Simon

Professeur des Universités (Bordeaux INP / Univ. Bordeaux / LaBRI)
(Page Professionnelle)

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....

Explications (avec les mains) pendant une présentation

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 l’équipe Méthodes Formelles au laboratoire d’informatique de Bordeaux, le (laBRI) à l’Université de Bordeaux, depuis 2013.

Des drones lors de la célébration des 100 ans de l'ENSEIRB-MATMECA

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.

⊆ Departement Info ⊆ ENSEIRB-MATMECA ⊆ Bordeaux-INP ⊆ Réseau INP ⊆

Photo de l'école d'ingénieurs Bordeaux-INP

Du point de vue animation de la recherche, mes principales occupations actuelles peuvent se résumer ainsi :

⊆ Axe IA ⊆ LaBRI ⊆ Université de Bordeaux / Bordeaux INP / CNRS ⊆

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

Picture of the LaBRI Computer Science Laboratory

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

Médailles de notre solveur SAT Glucose obtenues lors de la compétition 2017

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 .