Réduire la fracture entre spécification expressive et vérification efficace pour l'apprentissage automatique
La vérification formelle de réseaux de neurones se heurte à une double tension entre d’une part,
la capacité à exprimer des spécifications compactes, expressives et décrivant des
propriétés de haut-niveau de systèmes comprenants des composants IA et, d’autre part, la possibilité
effective de traduire ces spécifications aux prouveurs états de l’art.
L'état de l'art présente un ensemble de propriétés dites « globales » qui décrivent des comportements généraux sur le composant IA.
Ces propriétés sont partiellement formalisées mais ne sont à l'heure actuelle pas exprimables dans les langages de spécification standards au sein de la communauté. Elles restent donc pour la plupart théoriques.
Cette thèse se propose de réduire cette tension en proposant une formalisation au sein du langage WhyML de ces propriétés. La compilation efficace de ces propriétés via des techniques de réécriture de graphe automatique seront ensuite investiguées, exploitant des encodages avancés de réseaux de neurones pour la vérification. L'état de l'art n'offrant à l'heure actuelle que peu de travaux sur la comparaison des performances de prouveurs, cette thèse investiguera également ce volet, en s'inspirant des approches de portfolio de prouveurs.
Monitoring long terme et non-invasif des végétaux par spectroscopie dans le MIR
Le LCO (Laboratoire des Capteurs Optiques) développe à la fois des composants de photonique intégrée sur silicium du visible au moyen-infrarouge (sources, guides d'onde, détecteurs), et des capteurs et systèmes innovants. De la recherche technologique amont jusqu'aux transferts industriels, ces capteurs trouvent des applications dans les domaines de l'environnement, de la santé et du domaine sécurité/défense.
Une des thématiques de recherche du laboratoire est l'analyse d'échantillons denses par spectroscopie dans le Moyen Infrarouge par une modalité de détection photoacoustique. Forts de résultats encourageant pour le suivi de paramètres physiologiques sur l'humain, nous souhaitons adapter et étendre ces capteurs au domaine du végétal. Des premières mesures en laboratoire donnent des résultats encourageants, mais leur interprétation, de par la complexité de la mesure et de l'objet d'étude, reste à réaliser. C'est l'objet du travail de thèse que nous proposons.
Pour y parvenir, le candidat établira un programme expérimental avec le support de spécialistes en instrumentation et en biologie végétale. Il aura accès aux ressources matérielles et informatiques du laboratoire, et les capacités de prototypage du CEA-Grenoble.
Au terme du travail de thèse, un résultat possible serait la proposition d'un cas d'application du capteur au suivi des végétaux. Le cas d'application comprendrait un protocole expérimental pour la mise en oeuvre de la mesure, et un modèle permettant de remonter à des paramètres physiologiques du végétal pertinents pour les biologistes.
GenPhi : IA Générative 3D conditionnée par la géométrie, la structure et la physique
L’objectif de la thèse est de concevoir de nouveaux générateurs de modèles 3D basés sur l’intelligence artificielle générative (IAG), capables de produire des formes fidèles, cohérentes et physiquement viables. Alors que la génération 3D est devenue essentielle dans de nombreux domaines, les approches actuelles de génération automatique souffrent de limites en termes de respect des contraintes géométriques, structurelles et physiques. L’objectif est de développer des méthodes permettant d’intégrer, dès la génération, des contraintes liées à la géométrie, à la topologie, à la structure interne, ainsi qu’aux lois physiques, tant stationnaires (équilibre, statique) que dynamiques (cinématique, déformation). L’étude combinera des approches de perception géométrique, d’enrichissement sémantique et de simulation physique afin de produire des modèles 3D robustes, réalistes et directement exploitables sans intervention humaine.
Vers une coordination fiable et autonome des workflows dans les systèmes d’IA agentique
L’émergence des grands modèles de langage (LLMs) et des systèmes d’IA agentique transforme en profondeur la manière dont les workflows complexes sont conçus et pilotés. Contrairement aux approches traditionnelles d’orchestration centralisée, les workflows modernes doivent intégrer des agents autonomes et distribués, opérant à travers le cloud, l’edge et les environnements locaux. Ces agents collaborent avec des humains et d’autres systèmes, s’adaptent à des objectifs évolutifs, et franchissent des frontières organisationnelles et de confiance. Ce changement de paradigme est particulièrement pertinent dans des domaines comme la cybersécurité ou la réponse d’urgence en santé, où les workflows doivent être construits et exécutés dynamiquement dans des contextes incertains. Dans de tels environnements, l’automatisation rigide est insuffisante : les workflows agentiques nécessitent une orchestration décentralisée, sécurisée et traçable.
Cette thèse explore comment rendre de tels systèmes possibles, en posant la question : comment assurer une orchestration distribuée, sécurisée et auditable dans des environnements où l’IA agentique opère de manière autonome ? Elle proposera un cadre formel de modélisation des workflows agentiques distribués, des protocoles de coordination traçable et respectueuse de la vie privée, ainsi qu’une architecture de référence illustrée par des cas d’usage réels en cybersécurité et en santé.
Apprentissage Fédéré Robuste et Sécurisé
L’Apprentissage Fédéré (FL) permet à plusieurs clients d’entraîner ensemble un modèle global sans partager leurs données brutes. Bien que cette approche décentralisée soit particulièrement adaptée aux domaines sensibles à la vie privée, comme la santé ou la finance, elle n’est pas intrinsèquement sécurisée : les mises à jour de modèle peuvent révéler des informations privées, et des clients malveillants (Byzantins) peuvent corrompre l’apprentissage.
Pour faire face à ces défis, deux grandes stratégies sont employées : l’Agrégation Sécurisée, qui préserve la confidentialité en masquant les mises à jour individuelles, et l’Agrégation Robuste, qui filtre les contributions malveillantes. Cependant, ces objectifs peuvent entrer en conflit : les mécanismes de confidentialité peuvent masquer les signes de comportements malveillants, tandis que la robustesse peut nécessiter un accès à des informations sensibles.
De plus, la majorité des travaux se concentrent sur les attaques au niveau des modèles, négligeant les menaces au niveau du protocole, comme les délais de message ou les mises à jour perdues — des comportements fréquents dans des réseaux réels et asynchrones.
Cette thèse vise à explorer le compromis entre confidentialité et robustesse en FL, à identifier des modèles de sécurité réalistes, et à concevoir des protocoles pratiques, sûrs et robustes. L’approche combinera une analyse théorique des garanties possibles et une implémentation de prototypes s’appuyant sur des outils comme le calcul multipartite sécurisé, des primitives cryptographiques et la confidentialité différentielle.
Radiothérapie VHEE avec des faisceaux d'électrons issus d'un accélérateur laser-plasma
Les programmes de recherche menés au sein du Laboratoire Interactions et Dynamique des Lasers (Lidyl) du Commissariat à l’Énergie Atomique (CEA) visent à comprendre les processus fondamentaux impliqués dans les interactions lumière-matière et leurs applications. Au sein du CEA-LIDYL, le groupe Physique à Haute Intensité (PHI) étudie les interactions laser-matière à des intensités extrêmes, pour lesquelles la matière se transforme en plasma ultra-relativiste. À l'aide de la théorie, de simulations et d'expériences, les chercheurs développent et testent de nouveaux concepts pour contrôler l'interaction laser-plasma dans le but de produire de nouvelles sources d'électrons relativistes et de lumière attoseconde X-UV, pouvant avoir des applications en recherche fondamentale, médecine ou pour l'industrie.
En collaboration avec le Lawrence Berkeley National Laboratory (LBNL), le groupe contribue fortement au développement du code WarpX utilisé pour la modélisation haute fidélité des interactions laser-matière. Il est également à l'origine de l'étude et du contrôle de composants optiques remarquables appelés "miroirs - plasma", qui peuvent être obtenus en focalisant un laser de forte puissance avec un contraste élevé sur une cible initialement solide. Au cours des cinq dernières années, le groupe PHI a développé des concepts fondamentaux exploitant les miroirs plasma pour manipuler la lumière extrême afin de repousser les frontières de la science à haut champ. L'un de ces concepts utilise les miroirs plasma comme injecteurs de haute charge pour augmenter la charge produite dans les accélérateurs laser-plasma (LPA) afin de permettre leur utilisation pour des études médicales, telles que la radiothérapie par électrons de très haute énergie (VHEE). Ce concept est mis en œuvre au CEA sur l'installation laser UHI100 100 TW en 2025 pour délivrer des faisceaux d'électrons de 100 MeV - 200 MeV avec 100 pC de charge/impulsion pour l'étude du dépôt à haut débit de dose d'électrons VHEE sur des échantillons biologiques.
Dans ce contexte, le doctorant utilisera notre outil de simulation WarpX pour optimiser les propriétés du faisceau d'électrons produit par les LPA pour les études VHEE (qualité du faisceau d'électrons et énergie finale). Il étudiera ensuite la manière dont le faisceau d'électrons des LPA dépose son énergie dans des échantillons d'eau (en tant que milieu biologique) à l'aide de Geant4. Cela permettra d'évaluer le dépôt de dose à un débit de dose très élevé et de développer de nouvelles techniques de dosimétrie pour les faisceaux d'électrons LPA VHEE. Enfin, la production et le devenir des espèces réactives de l'oxygène (ROS) dans l'eau seront étudiés à l'aide de la boîte à outils Geant4-DNA. Ce module dispose principalement de données tabulées à des énergies d'électrons inférieures à 10 MeV et nécessitera donc des mesures de la section transversale des processus d'ionisation de l'eau à partir d'expériences à 100 MeV. Ces mesures seront effectuées sur le laser UHI100 100 TW par le groupe DICO du CEA-LIDYL, en collaboration avec le groupe PHI.
Cadre MBSE augmenté par l’Intelligence Artificielle pour l’analyse conjointe de la sureté et de la sécurité des systèmes critiques
Les systèmes critiques doivent respecter simultanément des exigences de Sureté de fonctionnement (prévenir les défaillances involontaires pouvant entraîner des dommages) et de Sécurité (protéger contre les attaques malveillantes). Traditionnellement, ces deux domaines sont traités séparément, alors qu’ils sont interdépendants : Une attaque (Sécurité) peut déclencher une défaillance (Sureté), et une faille fonctionnelle peut être exploitée comme vecteur d’attaque.
Les approches MBSE permettent une modélisation rigoureuse du système, mais elles ne capturent pas toujours les liens explicites entre la Sureté [1] et Sécurité [2] ; les analyses de risques sont manuelles, longues et sujettes à erreurs. La complexité des systèmes modernes rend nécessaire l’automatisation de l’évaluation des compromis Sureté-Securité.
La modélisation MBSE conjointe sureté/sécurité a été largement abordé dans plusieurs travaux de recherche tels que [3], [4] et [5]. Le verrou scientifique de cette thèse consiste à utiliser l’IA pour automatiser et améliorer la qualité des analyses. Quel type d’IA devrons nous utiliser pour chaque étape d’analyse ? Comment détecter les conflits entre les exigences de sécurité et de sureté ? Quelle sont les critères pour évaluer l’apport de l’IA dans l’analyse conjointe sureté/sécurité…
Justification visuelle du raisonnement spatio-temporel dans les modèles multimodaux vision-langage
Les modèles vision-langage (VLMs) récents, comme BLIP, LLaVA et Qwen-VL, ont montré de bonnes performances sur des tâches multimodales, mais présentent encore des lacunes en raisonnement spatio-temporel. Les benchmarks actuels confondent souvent raisonnement visuel et connaissances générales, et ne sollicitent que peu de raisonnement complexe. De plus, ces modèles peinent à interpréter les relations spatiales fines et les scènes dynamiques, en raison d’une mauvaise exploitation des caractéristiques visuelles. Pour y remédier, des travaux récents (SpatialRGPT, SpaceVLLM, VPD, ST-VLM) ont introduit des innovations telles que l’intégration de graphes 3D, des requêtes spatio-temporelles ou l’apprentissage par instructions cinématiques. Cette thèse s’inscrit dans cette lignée en proposant une nouvelle approche pour améliorer le raisonnement spatio-temporel des VLMs grâce à des techniques avancées de représentation des données et d’architecture, avec des applications en robotique, analyse vidéo et compréhension d’environnements dynamiques.
Détection d'anomalies dans les vidéos adaptative et explicable
La détection d'anomalies dans les vidéos (VAD) vise à identifier automatiquement les événements inhabituels dans des séquences vidéo qui s’écartent des comportements normaux. Les méthodes existantes reposent souvent sur l'apprentissage One-Class ou faiblement supervisé : le premier n'utilise que des données normales pour l'entraînement, tandis que le second s'appuie sur des labels au niveau de la vidéo. Les récents progrès des modèles Vision-Langage (VLM) et des grands modèles de langage (LLM) ont permis d’améliorer à la fois les performances et l’explicabilité des systèmes VAD. Malgré des résultats prometteurs sur des jeux de données publics, plusieurs défis subsistent. La plupart des méthodes sont limitées à un seul domaine, ce qui entraîne une baisse de performance lorsqu'elles sont appliquées à de nouveaux jeux de données avec des définitions d’anomalies différentes. De plus, elles supposent que toutes les données d'entraînement sont disponibles dès le départ, ce qui est peu réaliste dans des contextes d’utilisation réels où les modèles doivent s’adapter continuellement à de nouvelles données. Peu d’approches explorent l’adaptation multimodale en utilisant des règles en langage naturel pour définir les événements normaux ou anormaux. Or, cela permettrait une mise à jour plus intuitive et flexible des systèmes VAD sans nécessiter de nouvelles vidéos.
Ce sujet de thèse a pour objectif de développer des méthodes de détection d’anomalies vidéo adaptables, capables de traiter de nouveaux domaines ou types d’anomalies en s’appuyant sur peu d’exemples vidéo et/ou des règles textuelles.
Les axes de recherche principaux seront les suivants :
• Adaptation interdomaines en VAD : améliorer la robustesse face aux écarts de domaine via une adaptation Few-Shot ;
• Apprentissage continu en VAD : enrichir le modèle en continu pour traiter de nouveaux types d’anomalies ;
• Apprentissage multimodal en Few-Shot : faciliter l’adaptation du modèle à l’aide de règles en langage naturel.
Un cadre théorique pour la conception et la réalisation de robots sériels modulaires et reconfigurables axés sur les tâches, en vue d'un déploiement rapide.
Les innovations qui ont donné naissance aux robots industriels remontent aux années soixante et soixante-dix. Elles ont permis un déploiement massif de robots industriels qui ont transformé les ateliers, du moins dans certains secteurs de l'industrie tels que la construction automobile et certaines chaînes de production de masse.
Néanmoins, ces robots ne répondent pas totalement à d’autres applications qui sont apparues et se sont développées dans des domaines tels que la recherche en laboratoire, la robotique spatiale, la robotique médicale, l'inspection et la maintenance, la robotique agricole, la robotique de service et, bien sûr, les humanoïdes. Un petit nombre de ces secteurs ont connu un déploiement et une commercialisation à grande échelle de systèmes robotiques, mais la plupart avancent de manière lente et incrémentale.
Une question que l’on peut se poser est de savoir à quoi cela est dû ? Est-ce parce que le matériel n’est pas adapté (capacités physiques insuffisantes pour générer les forces et effectuer les mouvements nécessaires), parce que le logiciel n’est pas suffisamment performant (contrôle commande, perception, décision, apprentissage, etc.), ou parce qu’on ne dispose pas de paradigmes de conception capables de répondre aux besoin de ces applications (possibilités de conception rapide et sur mesure de nouveaux robots) ?
L'explosion sans précédent de la science des données, de l'apprentissage automatique et de l'IA dans tous les domaines de la science, de la technologie et de la société est souvent perçue comme une solution évidente pour répondre au problème, et une évolution radicale se profile ou est anticipée avec la promesse d'autonomiser les prochaines générations de robots grâce à l'IA (à la fois prédictive et générative). En conséquence, on a souvent tendance à apporter une attention particulière à l'aspect logiciel (apprentissage, aide à la décision, codage etc.), sans doute au détriment de capacités physiques améliorées (matériel) et de nouveaux concepts (paradigmes de conception). Il est pourtant clair que les aspects cognitifs de la robotique, notamment l'apprentissage, le contrôle et l'aide à la décision, ne pourront apporter une solution que si des dispositifs adaptés sont disponibles pour répondre aux besoins des diverses tâches que l’on souhaite robotiser, ce qui suppose des méthodologies de conception et un matériel adaptés.
L'objectif de cette thèse est ainsi de se concentrer sur les paradigmes de conception et le hardware, et plus spécifiquement sur la conception optimale de robots série utilisant une famille de « modules » standardisés dont l’agencement sera optimisé pour des familles de tâches données qui ne peuvent pas être accomplies par un robot industriel du marché. L’ambition de ce travail est de permettre de passer d’un catalogue donné de robots à la conception très rapide de solutions robotisées sur mesure.
Le candidat ou la candidate retenu(e) s'inscrira à l’Ecole Doctorale Mathématiques, STIC, de Nantes Université (ED-MASTIC) et sera accueilli(e) pendant trois ans au Service de Robotique Interactive du CEA-LIST à Palaiseau. Les professeurs Clément Gosselin (Laval) et Yannick Aoustin (Nantes) assureront l'encadrement académique de cette thèse qui sera co-encadrée par le Dr Farzam Ranjbaran du CEA-LIST.
Nous envisageons l’opportunité de poursuivre cette collaboration grâce à une bourse postdoctorale d’un an à laquelle le candidat pourrait candidater, une fois les prérequis du doctorat validés. Cette bourse serait hébergée au Centre de recherche en robotique, vision et intelligence artificielle (CeRVIM) de l’Université Laval, au Canada.