Ce sujet de thèse a pour objectif de créer un pont entre des solutions d’intelligence artificielle (IA) et des techniques formelles de la logique propositionnelle classique. Il vise à développer des méthodes génériques pour transformer des modèles d’IA en formules propositionnelles, en se focalisant sur le problème de cohérence, connu sous le nom de SAT (Satisfiability Problem). Cette approche cherche à tirer parti des progrès significatifs réalisés dans le domaine des solveurs SAT. Un aspect clé de ce travail est l’identification des caractéristiques importantes des modèles d’IA qui peuvent être efficacement traduites en représentations SAT. L’intérêt se porte particulièrement sur des traductions qui abordent des enjeux fondamentaux, comme renforcer la confiance dans les décisions algorithmiques, augmenter la transparence et intégrer efficacement des connaissances issues des domaines étudiés. Le but principal est de mettre en place un cadre explicatif pour des modèles d’IA, qui aide à détecter les biais potentiels et fournit des explications claires et accessibles aux utilisateurs finaux.

    Plus de détails sur ADUM