Cadre formel pour la spécification et la vérification de flots de communication de processus distribués dans le Cloud
Les clouds sont constitués de serveurs interconnectés via internet, sur lesquels on peut implémenter des systèmes faisant usages d’applications et de bases de données déployées sur les serveurs. L’informatique basée sur les clouds gagne considérablement en popularité, y compris pour y déployer des systèmes critiques. De ce fait, disposer d’un cadre formel pour raisonner sur ce type de systèmes devient une nécessité. Une exigence sur un tel cadre est qu’ils permettent de raisonner sur les concepts manipulés dans un cloud, ce qui inclue naturellement la capacité à raisonner sur des systèmes distribués, composés de sous-systèmes déployés sur différentes machines et interagissant par passage de messages pour réaliser des services. Dans ce contexte, la facilité à raisonner sur les flots de communications est un élément central. L'objectif de cette thèse est de définir un cadre formel outillé dédié à la spécification et la vérification de systèmes déployés sur des clouds. Ce cadre capitalisera sur le cadre formel des "interactions". Les interactions sont des modèles dédiés à la spécification des flots de communications entre différents acteurs d'un système. Les travaux de thèse étudieront comment définir des opérateurs de structuration (enrichissement, composition) et de raffinement pour permettre de mettre en œuvre des processus de génie logiciel classique en se basant sur les interactions.
Co-conception de convertisseurs intégrés ultra-compacts exploitant des micro-batteries tout solide
L’amélioration des performances des systèmes de conversion d’énergie DC-AC ou AC-DC est un enjeu majeur pour réduire la masse des dispositifs, prolonger leur autonomie et améliorer leur compacité. Ce projet de thèse vise à explorer de nouvelles topologies de convertisseurs intégrés innovants en s’appuyant sur un composant émergent : la micro-batterie tout solide.
Après une phase d’analyse système sur deux cas d’application représentatifs — l’un en conversion AC-DC, l’autre en DC-AC — le doctorant identifiera la topologie de conversion la plus adaptée pour des puissances de l’ordre du milliwatt. Cette topologie sera co-optimisée avec une matrice de micro-batteries tout solide disponible, afin de tirer pleinement parti des caractéristiques de ces composants. Le candidat mènera ensuite la conception du circuit, sa fabrication éventuelle et la validation expérimentale de l’approche.
Encadrée par Gaël Pillonnet (CEA-Leti) et Patrick Mercier (University of California), cette thèse s’inscrit dans un environnement de recherche de pointe sur les circuits intégrés pour la gestion de l’énergie (PMIC). Le projet comporte une forte dimension applicative, centrée sur la co-optimisation entre l’électronique de puissance et les composants de micro-stockage dans des dispositifs ultra-compacts, dédiés à l’actionnement de micromoteurs ou à la micro-alimentation à partir du secteur.
Rejoindre notre équipe, c’est participer au développement de technologies de rupture ayant un fort impact potentiel dans les domaines de la santé, de la défense ou de la maintenance prédictive.
Approches anisotropes en traitement du signal sur graphe. Application aux réseaux de neurones sur graphe.
Le traitement du signal sur graphe repose sur les propriétés d'un opérateur élémentaire généralement associé à une notion de marche aléatoire / processus de diffusion. Une limite de ces approches est que l'opérateur est systématiquement isotrope, propriété qui est transmise à toute notion de filtrage basée dessus. En traitement du signal multidimensionnel (images, vidéo, etc), on utilise au contraire énormément les filtres non-isotropes (voire qui ne prennent en compte qu'une seule direction) ce qui augmente très fortement les possibilités. Ces filtres non-isotropes sont en particulier l'élément de base des réseaux de neurones convolutionnels dont on se doute qu'ils seraient moins performants avec uniquement des filtres isotropes (i.e. réponse impulsionnelle à symétrie circulaire/sphérique). L'isotropie des filtres est à l'heure actuelle aussi considérée comme un frein majeur à l'expressivité des réseaux de neurones convolutionnels sur graphe, qui pourrait être levé à l'aide de constructions non-isotropes de traitement du signal sur graphe. Au-delà des graphes homogènes, les opérateurs utilisés pour le traitement du signal ou les réseaux de neurones sur des graphes bipartites ou plus généralement hétérogènes ont aussi cette propriété d'isotropie où les voisins d'un nœud sont traités de manière identique. Bien qu'il n'y ait pas cette fois de lien évident avec des approches classiques, la notion d'opérateur anisotrope ou directionnel semble là aussi pertinente pour différencier le traitement selon les multiples facettes qui peuvent contribuer à une relation donnée.
Pour aborder la notion de directionnalité dans les graphes, on s'appuiera notamment sur le fait qu'un graphe peut bien souvent être vu comme la discrétisation d'une variété Riemanienne. On étudiera aussi une extension aux graphes bipartites, qui présentent des similarités avec une relation entre deux variétés, ainsi qu'aux graphes hétérogènes qui sont formés de plusieurs relations. Des applications aux réseaux de neurones sur graphes seront envisagées afin d'explorer le gain de flexibilité apporté par la directionnalité.
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.
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é…
Apprentissage profond informé par la physique pour le contrôle non destructif
Ce projet de thèse s’inscrit dans le domaine du contrôle non destructif (CND), un ensemble de techniques qui permettent de détecter des défauts dans des structures (câbles, matériaux, composants) sans les endommager. Le diagnostic repose sur des mesures physiques (réflectométrie, ultrasons…), dont l’interprétation nécessite de résoudre des problèmes inverses souvent mal posés.
Les approches classiques par algorithmes itératifs sont précises mais coûteuses en calcul et difficiles à embarquer pour un traitement proche du capteur. Le travail proposé vise à dépasser ces limites en explorant des approches de deep learning informé par la physique notamment :
* des réseaux neuronaux inspirés des algorithmes classiques (méthode d’unrolling),
* des PINNs (Physics-Informed Neural Networks) qui intègrent directement les lois physiques dans l’apprentissage,
* des modèles différentiables simulant la mesure (réflectométrie notamment).
L’objectif est de développer des modèles profonds interprétables dans un cadre modulaire pour le CND, capables de fonctionner sur des systèmes embarqués. Le cas d’étude principal concernera les câbles électriques (TDR/FDR), avec une ouverture possible vers d'autres modalités comme les ultrasons. Cette thèse combine optimisation, apprentissage et modélisation physique, et s'adresse à un profil motivé par l’interdisciplinarité entre sciences de l’ingénieur, mathématiques appliquées et intelligence artificielle.