I.A. de Confiance : Encadrement de Décisions issues De l’Apprentissage Automatique par des Preuves Formelles

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


Sujet du stage

Dans le but d’atteindre la meilleure précision possible, les systèmes de décisions/recommandations construits à l’aide d’apprentissage automatique agissent principalement sur un levier : la complexité calculatoire des fonctions apprises (e.g. le nombre de paramètres appris). Il est ainsi d’usage de bâtir des systèmes de recommandations mettant en jeu des millions de calculs conduisant à une décision, ce qui a pour effet immédiat de rendre, par construction, l’inspection de leur comportement impossible en termes simples et compréhensibles. Viser uniquement la précision peut avoir d’immenses intérêts applicatifs mais dès lors que leur mise en œuvre requiert de comprendre, justifier, expliquer, ou garantir certaines décisions, on voit que seule la précision ne suffit pas.

Comment est-il possible d’avoir confiance dans une décision dont le calcul est par construction impossible à résumer en termes compréhensibles ?

Ce constat a entraîné la multiplication de travaux d’un nouveau sous-domaine de l’intelligence artificielle, en lien avec la problématique de confiance dans les décisions autonomes (ainsi, de nombreux workshops spécialisés sont proposés en marge de toutes les plus grandes conférences en IA).

Suivant les applications visées, la confiance peut revêtir différentes formes. Dans l’approche que nous proposons, la confiance est exprimée en termes de garanties prouvées. Pour cela, nous nous appuierons sur les progrès réalisés ces dernières années par les méthodes formelles (notamment grâce à l’emploi de solveurs SMT / SAT) de manière à encadrer des systèmes décisionnels “boîte noire” par des systèmes plus simples permettant d’exprimer les garanties visées dans des langages accessibles. Si les méthodes formelles ont également fait d’immenses progrès ces dernières années, tenter de les utiliser directement sur les systèmes ayant des milliards de paramètres semble vain. Nous proposons dans cette approche d’encadrer ces systèmes par d’autres systèmes plus simples, et de garantir les propriétés sur les fonctions encadrant ces systèmes.

Ainsi, étant donné par exemple un réseau de neurones RNNA prédisant “Oui” ou “Non” sur une entrée quelconque, nous proposons de construire deux formules logiques Up et Down permettant d’encadrer au mieux les décisions de RNNA (Up pour les “Oui”, Down pour les “non”) et offrant des garanties d’explicabilité ou permettant la preuve de certaines propriétés désirées. Le point clé est que les langages Up et Down sont définis sur des langages logiques permettant la preuve formelle (logiques propositionnelles, logiques temporelles, …) tout en capturant un maximum de précision depuis RNNA.

Cette approche pose de nombreux problèmes. La difficulté principale consiste à construire Up et Down à partir de A. Il conviendra donc d’étudier comment le langage avec lequel RNNA, Up et Down sont exprimés permettra de réécrire A en minimisant les pertes de précision des fonctions Up et Down. Des approches issues des Réseaux de Neurones Binarisés, ainsi que les approches à base de Compilation de base de connaissances pourront être étudiées. Suivant les connaissances du stagiaire, il pourra également être étudié comment l’apprentissage en lui-même peut être modifié pour viser directement l’apprentissage des fonctions RNNA, Up et Down plutôt que de les calculer a posteriori.

Suite du stage

Vu la richesse du sujet, le stage est associé à une bourse de 3 ans de thèses, co-financée par la Chaire IA Digne de Confiance et le projet RobSYS.

Candidat

Le candidat devra avoir un excellent niveau scientifique et une bonne connaissance des méthodes de raisonnement basés sur la logique. De plus, il est également attendu un très bon niveau de programmation.

Le stage pourra commencer dès février 2023.

Contact: Laurent Simon

Le PDF décrivant ce sujet de stage + thèse est disponible ici