Vérification formelle pour la compilation de programmes quantiques

L'informatique quantique est aujourd'hui un domaine hautement prometteur, avec des applications décisives dans de nombreux domaines clés (biologie, chimie, cryptographie, optimisation, apprentissage machine, etc).

Un des défis les plus importants dans ce champ émergeant est la validation des programmes.
En s'inspirant des meilleures techniques existantes pour la vérification formelle de programmes classiques -- vérification déductive, raisonnement en logique de premier ordre -- notre récent développement de Qbricks permet la spécification formelle -- bonne formation des circuits, comportement fonctionnel, complexité -- et la vérification de programmes quantiques opérant sur des qubits idéaux.

Le but de cette thèse est d’étendre l’usage de cette pratique dans la chaîne de compilation quantiques.
Les possibilités sont notamment les développement (1) d'un langage de représentation intermédiaire formellement vérifié pour l'implémentation tolérantes aux fautes, (2) d'outils de raisonnement pour la certification de fonctions de transformations de circuits quantiques et/ou hybrides classiques/quantiques, (3) d'outils automatiques de vérification de propriétés sur des relations d'équivalence et/ou de proximité entre circuits quantiques.

Définition d’un modèle asynchrone de compression de données à la volée sur accélérateurs pour le HPC

Cette thèse porte sur le calcul haute performance pour la simulation numérique de phénomènes physiques complexes.
Le CEA met à disposition les ressources matérielles et logicielles permettant d'atteindre la puissance de calcul requise.
Nous avons assisté à l’avènement des accélérateurs, entraînant de nouveaux défis. En particulier, la gestion de la mémoire devient essentielle pour atteindre des performances exascale, car le rapport taille mémoire par nombre d'unités de calcul diminue.
Ce problème touche tous les domaines nécessitant un volume de données important. Ainsi, de nombreux aspects de cette thèse seront généraux et d’intérêt mondial.

Cette thèse aura pour objectif de proposer un modèle asynchrone de mise à disposition de données via des techniques de compression/décompression. Il doit être suffisamment efficace pour être utilisé « à la volée » (pendant les calculs sans les ralentir), permettant de relâcher les contraintes mémoire.
Les codes ciblés sont itératifs et séquencent différentes phases. Idéalement, tous les calculs seront effectués sur des accélérateurs, laissant les ressources CPU inoccupées. Le modèle proposé devrait tirer parti de ces spécificités. L'objectif final sera l'intégration des travaux dans un code représentatif pour évaluer les gains dans un contexte industriel.

Raffinement de maillage adaptatif multi-architecture pour la simulation des équations de l’hydrodynamique compressible multi-matériaux

Le CEA DAM développe activement des outils de calcul scientifique en mécanique des fluides pour la simulation numérique d'écoulements de fluides compressibles et multi-matériaux. Ces logiciels utilisent des modèles de programmation adaptés à l'utilisation efficace des supercalculateurs et mettent en oeuvre des méthodes de résolution numérique des équations de l'hydrodynamique compressible en utilisant la stratégie du raffinement de maillage adaptatif, AMR (Adaptive Mesh Refinement) qui permet de réduire le coût de calcul de certaines simulations, en réduisant le nombre de cellules (donc l'empreinte mémoire) et de concentrer les calculs sur les zones d'intérêt (discontinuités, chocs, interfaces multi-fluides, ...).

Depuis une quinzaine d'année, avec l'apparition des processeurs graphiques (GPU), les architectures matérielles utilisées dans le domaine du calcul haute performance ont profondément évoluées. La thèse proposée vise à concevoir une implantation parallèle des techniques AMR pour le cas des écoulements multi-matériaux dans le but d'utiliser efficacement un supercalculateur utilisant massivement les processeurs graphiques (GPU). Après vérification et validation du code développé, on pourra l'exploiter pour simuler l'effet d'une onde de souffle et son interaction avec les structures environnantes.

Apprentissage fédéré sur des données verticalement partitionnées provenant de participants hétérogènes

L'apprentissage fédéré permet à plusieurs participants d'entraîner en collaboration un modèle global, sans partager leurs données, mais seuls les paramètres du modèle sont échangés entre les participants et le serveur. Dans l'apprentissage fédéré vertical (VFL), les données des participants partagent des échantillons similaires, mais ont des attributs différents. Par exemple, des entreprises de différents domaines possédant des données avec des attributs différents collaborent pour résoudre une tâche d'apprentissage automatique. Bien que les données soient privées, VFL reste vulnérable aux attaques telles que les attaques de type Feature/Label Inference Attack. Différentes méthodes de protection (par exemple, la confidentialité différentielle, le chiffrement homomorphe) ont été étudiées pour protéger la confidentialité du VFL. Le choix des méthodes appropriées est un défi car il dépend de l'architecture de VLF et du niveau de confidentialité souhaité (par exemple, modèles locaux, résultats intermédiaires, modèles appris). La variabilité du système de chaque participant peut également entraîner une latence élevée et des mises à jour asynchrones, ce qui affecte la performance du modèle et l'efficacité de l’entraînement.

L'objectif de cette thèse est de proposer des méthodes pour effectuer VFL de manière confidentielle, en tenant compte de l'hétérogénéité des participants. Premièrement, le candidat étudiera les architectures des modèles VFL et les mesures de confidentialité afin de proposer des protocoles d’entraînement sécurisés et confidentiels pour VFL. Deuxièmement, le candidat étudiera les impacts de l'hétérogénéité du système des participants, tels que les ressources de calcul et de communication, afin de concevoir des solutions pour rendre les protocoles proposés robustes à ce type d’hétérogénéité. Troisièmement, les compromis entre la performance, la confidentialité et l’efficacité du VFL seront étudiés afin de proposer un cadre pratique permettant de piloter les protocoles en fonction des caractéristiques d'un problème d'apprentissage automatique donné.

Découverte de nouvelles sondes chromogéniques pour les toxiques par Chemistry-Trained Machine Learning

L’actualité nationale et internationale justifie l’intérêt croissant porté à la détection des toxiques et des polluants (nommés analytes dans ce qui suit) par virage chromogénique. Pour les analytes déjà connus et étudiés, il est nécessaire d’améliorer les capacités de détection, notamment par augmentation des contrastes et de la sélectivité. Pour de potentiels nouveaux analytes, il est également pertinent de se préparer à une sélection rapide de sondes chromogéniques spécifiques. Les objectifs de la thèse seront de découvrir de nouvelles sondes chromogéniques en utilisant la chimie computationnelle.
Première étape de la thèse : Entraînement du modèle (ML/AI) sur les données disponibles. Le début du travail de thèse se focalisera sur l’établissement d’un modèle performant, précis et robuste de classification des nombreuses données expérimentales disponibles, issues des précédents travaux de notre laboratoire. Il s’agit de croiser les résultats colorimétriques de cette base avec les structures des molécules et leurs propriétés chimiques décrites par des méthodes de l’état de l’art (e.g., https://pubs.acs.org/doi/10.1021/acs.chemrev.1c00107). À la fin de cet apprentissage, nous devrions disposer d’un prédicteur validé sur nos données.
Seconde étape : Utilisation du prédicteur pour cribler in-silico plusieurs centaines de milliers de molécules sondes candidates issues de chimiothèques commerciales (et autres…), elles aussi croisées avec leurs structures et propriétés chimiques, décrites comme dans la première étape. À la suite d’un premier tri, la prédiction des virages chromogéniques par DFT pourra être utilisée pour affiner l’évaluation du potentiel virage colorimétrique des meilleures molécules candidates.
Troisième étape : Définition et réalisation d’une campagne de tests chimiques expérimentaux. Une plateforme de synthèse organique HTE (Expérimentation à Haut Débit), basée sur la miniaturisation et la parallélisation de réactions chimiques pour optimiser la mise en œuvre des réactions de synthèse et les tests, permettra un gain de temps considérable, tout en augmentant significativement le nombre de combinaisons possibles. Le HTE permet également la synthèse de librairies de composés analogues. À la suite de ces tests massifs, une seconde version de l’IA pourra être entraînée, permettant la découverte d’une nouvelle génération de molécules chromogéniques.

Élaboration d'un modèle numérique de l’irradiateur POSEIDON pour sa qualification en radiostérilisation au Co-60

Le CEA/Saclay dispose d’irradiateurs gamma au 60Co dédiés à la réalisation de prestations d’irradiation à façon, d’une part, pour le CEA dans le cadre de ses propres études de R&D, et d’autre part, pour les industriels des secteurs de l’électronucléaire, de la défense, de l’électronique, du spatial et de la santé.

Dans le domaine plus particulier de la santé, un irradiateur est employé pour radiostériliser, i.e. inactiver les contaminants microbiologiques (comme les bactéries, virus, microbes, spores) par rayonnements ionisants, de dispositifs médicaux tels que des prothèses de hanche, des vis ou plaques orthopédiques, pour le compte de leurs fournisseurs. Le grand intérêt de la stérilisation par rayonnements gamma, comparativement aux autres alternatives de stérilisation (au gaz ou à froid par immersion dans des produits chimiques liquides), est que les dispositifs médicaux n’ont pas à être extraits de leur carton et/ou de leur sachet étanche ; ils sont traités directement au travers de leur emballage.

La radiostérilisation de dispositifs médicaux présente un haut niveau d’exigence, en accord avec les prescriptions des normes ISO 13485 et ISO 11137. D’une part, les doses délivrées ne doivent être ni trop faibles, pour assurer la stérilité des produits, ni trop fortes, pour ne pas altérer leur intégrité. D’autre part, trois étapes de qualification sont nécessaires afin de garantir la validation des procédés de stérilisation par irradiation. Les deux premières, dites d’installation et opérationnelle, ont respectivement pour but de démontrer que l’équipement de stérilisation est installé conformément à ses spécifications et fonctionne correctement en délivrant des doses appropriées dans les limites de critères d’acceptation définis. La qualification opérationnelle consiste plus particulièrement à caractériser l’irradiateur en termes de distribution et de reproductibilité de la dose, en considérant les volumes à irradier remplis d’un matériau homogène, de masses volumiques enveloppes représentatives des produits à traiter. Enfin, la troisième étape de qualification, dite des performances, doit démontrer, spécifiquement pour les produits médicaux à traiter, que l’équipement fonctionne de façon constante, conformément aux critères prédéterminés, et délivre des doses comprises dans la plage des doses spécifiées, donnant par conséquent un produit qui satisfait à l’exigence spécifiée pour la stérilité.

De manière générale, les cartons à irradier sont, selon les fournisseurs, remplis de divers produits médicaux différents et correspondent ainsi à un large éventail de tailles et de poids. Il convient par conséquent d’examiner les effets, sur la distribution spatiale de dose, de toutes les configurations possibles de chargements des produits, y compris pour différents taux de remplissage des balancelles, contenant les cartons, du convoyeur dynamique de l’irradiateur. Enfin, il est à noter que les processus de qualifications doivent être réitérés suite à toute modification susceptible d’affecter la dose ou la distribution de dose, et donc à chaque réapprovisionnement des sources. Ces processus sont actuellement réalisés exclusivement par mesures, à l’aide d’une multitude de dosimètres pertinemment répartis au sein et en surface des emballages.

Le Laboratoire des Rayonnements Appliqués (DRMP/SPC/LABRA), en charge de l’irradiateur gamma POSEIDON dédié à la radiostérilisation de matériels médicaux au CEA/Saclay, souhaite disposer d’un outil numérique permettant de réaliser par simulations ces processus de validation. Un des intérêts majeurs attendus par l’utilisation de cet outil est de réduire considérablement les durées d’indisponibilité de l’irradiateur POSEIDON, imposées par les phases expérimentales de validation.

Le sujet de thèse proposé a pour objet la mise en œuvre d’un modèle numérique de l’irradiateur POSEIDON permettant de reproduire par simulations les phases de validation, aussi rapidement que possible, tout en assurant l’exactitude des résultats, à la précision souhaitée. Ce travail sera effectué dans le laboratoire DM2S/SERMA/CP2C (CEA/Saclay), spécialisé entres autres dans les études de radioprotection par simulations numériques, avec des échanges réguliers avec le LABRA.

Ainsi, le sujet de la thèse, découpé en trois étapes, explorera une approche de validation alternative à celle réalisée expérimentalement :

• La première étape aura pour objet le développement d’un modèle numérique de l’irradiateur POSEIDON intégrant le caractère dynamique des traitements de radiostérilisation. Ce modèle numérique reposera sur une méthodologie de calcul qui sera arrêtée au cours de la thèse (méthode Monte-Carlo ou déterministe), avec un compromis entre la qualité des résultats obtenus et la rapidité d’exécution des calculs. Pour cette étape, le code de transport des rayonnements dans la matière de type Monte-Carlo TRIPOLI-4® sera utilisé comme référence avec des comparaisons réalisées à l’aide d’autres outils numériques tels que MCNP®, PENELOPE, GEANT4, NARMER-1, etc. ;

• La deuxième étape portera successivement sur la validation du modèle numérique retenu par confrontation à des mesures expérimentales, à définir et à réaliser au cours de la thèse, et sur son application au calcul des processus de qualification opérationnelle et des performances pour différentes familles de cartons de fournisseurs. Concernant la validation des calculs, l’instrumentation utilisée pour les mesures de doses gamma sera modélisée numériquement et analysée, en considérant tous les phénomènes physiques en jeu concernant la dose absorbée (doses photons et électrons). L’objectif est de consolider les comparaisons calculs/mesures pour les expériences réalisées au cours de la thèse.

• Enfin, la dernière étape concernera l’analyse de l’apport du modèle numérique par rapport à l’approche expérimentale. Cette approche calculatoire nécessitera néanmoins d’être optimisée en termes de temps de calcul afin notamment d’en faciliter les analyses de sensibilité à réaliser.

Au cours de thèse, diverses voies de recherches seront investiguées telles que l’amélioration de la modélisation des réflexions lors du transport des photons dans un milieu fermé (casemate de l’irradiateur PAGURE ; utilisation de techniques de deep learning pour les codes déterministes), la mise en œuvre de géométries stochastiques pour modéliser le contenu des cartons, et l’amélioration des algorithmes pour réduire les durées de calcul.

Cas d'Assurance Dynamiques pour les Systèmes Autonomes Adaptatifs

Donner l'assurance que les systèmes autonomes fonctionneront de manière sûre et sécurisée est une condition préalable à leur déploiement dans des domaines d'application critiques en termes de mission et de sécurité. Généralement, les assurances sont fournies sous la forme de cas d'assurance, qui sont des arguments vérifiables et raisonnés démontrant qu'une revendication de haut niveau (concernant généralement la sécurité ou d'autres propriétés critiques) est satisfaite compte tenu d'un ensemble de preuves relatives au contexte, à la conception et à la mise en œuvre d'un système. L'élaboration de cas d'assurance est traditionnellement une activité analytique, réalisée hors ligne avant le déploiement du système, et sa validité repose sur des hypothèses/prédictions concernant le comportement du système (y compris ses interactions avec son environnement). Cependant, il a été avancé que cette approche n'est pas viable pour les systèmes autonomes qui apprennent et s'adaptent en cours de fonctionnement. Cette thèse abordera les limites des approches d'assurance existantes en proposant une nouvelle catégorie de techniques d'assurance de la sécurité fondées sur la sécurité qui évaluent et font évoluer en permanence le raisonnement de sécurité, en même temps que le système, afin de fournir une assurance de la sécurité tout au long de son cycle de vie. En d'autres termes, l'assurance de la sécurité sera fournie non seulement au cours du développement et du déploiement initiaux, mais aussi en cours d'exécution, sur la base de données opérationnelles.

Modélisation et simulation du comportement humain pour des jumeaux numériques centrés sur l'humain

Grâce à une représentation virtuelle synchronisée, les jumeaux numériques sont un moyen pour produire des analyses, prédictions et optimisations de systèmes du monde réel. Or certains de ces systèmes interagissent étroitement avec les humains de sorte que le rôle de ces derniers est déterminant dans le fonctionnement du système. C’est par exemple le cas dans des contextes comme l’industrie 5.0 ou la gestion du pilotage de systèmes critiques, où la qualité de la collaboration entre les humains et les machines dépendra de l’anticipation de leurs actions, interactions et décisions respectives. Ainsi, pour améliorer la précision des prédictions et étendre l’applicabilité dans divers domaines, il est nécessaire, en s’appuyant sur les connaissances issues des sciences humaines et sociales, de développer des jumeaux numériques qui prennent en compte la complexité et la richesse des comportements humains (processus décisionnels, interactions, émotions…). Ces modèles comportementaux pourront notamment s’appuyer sur l’apprentissage automatique, l’exploration de données, la modélisation basée sur des agents et l’ingénierie des connaissances. Après avoir identifié les modèles de comportements humains utiles, il s’agira d’étudier leur articulation conceptuelle et leur intégration technique avec les modèles des entités cyber-physiques dans le système de jumeau numérique. De plus, nous explorerons comment les services de jumeaux numériques sont impactés et peuvent être révisés pour prendre en compte ces aspects centrés sur l’humain. Enfin, nous évaluerons l’efficacité des jumeaux numériques centrés sur l’humain dans diverses applications en mettant en œuvre des expériences sur des cas réels représentatifs.
Ce travail de recherche ambitionne les contributions suivantes :
• Le développement d'une approche basée sur des modèles de comportement humain pour obtenir des jumeaux numériques centrés sur l'humain.
• Des connaissances nouvelles sur l'impact du comportement humain sur le contrôle d'un système et inversement.
• Des applications pratiques et des recommandations sur l’usage de jumeaux numériques centrés sur l'humain dans des scénarios du monde réel.
Cette thèse se déroulera à Grenoble.

Analyses statiques avancées basées sur les types pour la vérification de systèmes d'exploitations

Dans des travaux récents [RTAS 2021], nous avons démontré l'intérêt d'une analyse statique guidée
par un système de types dépendants avancé pour analyses des programmes systèmes bas-niveau, allant
jusqu'à pouvoir vérifier automatiquement l'absence d'escalade de privilège dans un noyau de système
d'exploitation embarqué comme conséquence de la type-safety du code du noyau. La gestion de la
mémoire est un problème particulièrement ardu lors de l'analyse de programmes systèmes, ou plus largement,
de programmes écrits en C, et l'analyse basée sur les types fournit une solution satisfaisante à
applicabilité large (par exemple, code de gestion de structures de données [VMCAI 2022], runtime de
langage dynamique, code applicatif orienté performance, etc.)

Le but de la thèse est d'étendre le applications qui peuvent être faites de l'utilisation d'une analyse
statique basée sur les types.

[RTAS’21] No Crash, No Exploit: Automated Verification of Embedded Kernels. O. Nicole, M. Lemerre,
S. Bardin, X. Rival (Best paper)
[VMCAI’22] Lightweight Shape Analysis based on Physical Types, O. Nicole, M. Lemerre, X. Rival
[POPL’23] SSA Translation Is an Abstract Interpretation, M. Lemerre (Distinguished paper).

Conception d’algorithmes d’optimisation de contrôle de faisceau RADAR

L’arrivée sur le marché d’une nouvelle génération de Radars appelés « Imaging Radars 4D » apporte de nouvelles opportunités et de nouveaux challenges pour le développement d’algorithmes de traitement des données. Ces nouveaux capteurs, tournés vers le marché du véhicule autonome, permettent une meilleure résolution grâce à un grand nombre d’antennes. Cependant, cela implique une augmentation de la quantité de données à traiter qui nécessite des ressources de calcul importantes.
L’objectif de cette thèse est de développer des algorithmes permettant d’optimiser la résolution du Radar tout en limitant les coûts calculatoires, afin d’embarquer le traitement au plus proche du Radar. Pour cela, des techniques permettant de contrôler la forme et la direction du faisceau Radar seront utilisées, de manière à concentrer l’énergie dans les régions jugées pertinentes. Un des enjeux est donc de réaliser une boucle de rétroaction performante permettant de contrôler les antennes Radar en fonction de la scène observée lors des mesures précédentes.
Cette thèse privilégiera une approche expérimentale grâce à l’utilisation d’un radar possédé par le laboratoire. Des outils de simulation seront également utilisés pour tester les hypothèses et dépasser les possibilités offertes par le matériel.

Top