Vers une IA d'Essaim explicable et fiable fondée sur la satisfiabilité (maximum) // Towards an Explainable and Reliable Swarm Intelligence Based on (Maximum) Satisfiability

Ce projet de thèse vise à développer des algorithmes robustes pour l'IA d'essaim en s'appuyant sur la satisfiabilité propositionnelle (SAT) et son extension naturelle en problème d'optimisation, la satisfiabilité maximum (MaxSAT). L'objectif est d'analyser, valider, synthétiser et optimiser des algorithmes distribués adaptés à des robots lumineux dotés de capacités limitées, tels que l'utilisation de signaux visuels pour la communication. En modélisant ces algorithmes sous forme de formules SAT, il devient possible de garantir leur correction formelle, en identifiant et corrigeant les éventuelles défaillances, tout en automatisant leur conception selon des spécifications précises. L'utilisation de Max-SAT peut également contribuer à simplifier et à optimiser les règles des algorithmes, en produisant des solutions non seulement efficaces et adaptées aux contraintes matérielles des robots, mais aussi hautement explicables. Cette explicabilité est essentielle pour comprendre les mécanismes sous-jacents des comportements collectifs des essaims de robots, permettant de rendre ces systèmes transparents et de renforcer la confiance dans leur déploiement et renforçant ainsi leur applicabilité dans divers domaines tels que la logistique, l'exploration et la surveillance.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

This project aims to develop robust algorithms for swarm AI based on propositional Satisfiability (SAT) and its natural optimization extension, Maximum Satisfiability (MaxSAT). The goal is to analyze, validate, synthesize, and optimize distributed algorithms designed for light-emitting robots with limited capabilities, particularly using visual signals for communication. By modeling these algorithms as SAT formulas, it becomes possible to ensure their formal correctness, identify and correct potential failures, and automate their design according to precise specifications. The integration of MaxSAT can further help simplify and optimize algorithmic rules, producing solutions that are not only efficient and adapted to the hardware constraints of the robots but also highly explainable. This explainability is crucial for understanding the underlying mechanisms of collective swarm behavior, ensuring greater transparency in these systems and strengthening trust in their deployment. It also enhances their applicability in various domains such as logistics, exploration, and surveillance.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2025

Financement d'une collectivité locale ou territoriale

Université de Picardie - Jules Verne

585 Sciences, Technologie, Santé

Le candidat doit être titulaire d'un Master en informatique (ou équivalent, obtenu avant le début du doctorat). De solides compétences en programmation (C/C++) ainsi qu'une maîtrise de l'anglais sont requises. Le candidat doit faire preuve de rigueur scientifique, de capacités de résolution de problèmes et de solides compétences analytiques. Une connaissance préalable de l'algorithmique distribuées et de la programmation par contraintes, en particulier de la satisfiabilité (SAT), serait fortement appréciée.
The candidate must hold a Master's degree in Computer Science (or equivalent, obtained before the start of the PhD). Strong programming skills (C/C++) and proficiency in English are required. The candidate should demonstrate scientific rigor, problem-solving abilities, and strong analytical skills. Prior knowledge of distributed algorithms and constraint programming, particularly satisfiability (SAT), would be highly appreciated.