Méthodologie de vérification pour les logiciels de systèmes synchrones
Le greffon Synchrone de Frama-C est dédié à l'analyse de programmes Lustre. Il combine les capacités des greffons WP et Eva et communique avec le solveur GaTeL pour prouver diverses propriétés à propos des programmes sous analyse. Les travaux de ce postdoc visent à améliorer l'usage global de Synchrone à travers cet ensemble de challenges scientifiques:
- développer une méthodologie de vérification qui tire parti de la combinaison de techniques disponibles au sein de l'outil, notamment en l'appliquant à des cas représentatifs de l'usage réel de Synchrone,
- pour supporter cette méthodologie, améliorer l'outillage disponible au sein de synchrone, notamment en ce qui concerne la génération des obligations de preuves, et leur optimisation pour les solveurs automatiques, comme le solveur Colibri2 développés au sein du laboratoire,
- améliorer le lien entre ce qui est vérifié et le modèle mathématique qui spécifie le système, par l'extension du langage LustreSpec et le développement de l'outillage associé, cela comprend notamment les aspects liés à la gestion des filtres numériques,
- développement de l'outillage pour la visualisation et le déboggage des obligations de preuve.
Ce postdoc est donc plutôt orienté vers un travail d'ensemble visant des publications orientées méthodologie de vérification dans un contexte industiel.
Développement d'approches pour l'intelligence artificielle à base de bruit
Les approches actuelles de l'IA sont largement basées sur la multiplication matricielle. Dans le de ce projet postdoccadre toral, nous aimerions poser la question suivante : quelle est la prochaine étape ? Plus précisément, nous aimerions étudier si le bruit (stochastique) pourrait être la primitive computationnelle sur laquelle la nouvelle génération d'IA est construite. Nous répondrons à cette question en deux étapes. Tout d'abord, nous explorerons les théories concernant le rôle computationnel du bruit microscopique et au niveau du système dans les neurosciences, ainsi que la façon dont le bruit est de plus en plus exploité dans l'intelligence artificielle. Nous visons à établir des liens concrets entre ces deux domaines et, en particulier, nous explorerons la relation entre le bruit et la quantification de l'incertitude.
Sur cette base, le chercheur postdoctorant développera ensuite de nouveaux modèles qui exploitent le bruit pour effectuer des tâches cognitives, dont l'incertitude est une composante intrinsèque. Cela ne servira pas seulement comme une approche d'IA, mais aussi comme un outil informatique pour étudier la cognition chez les humains et aussi comme un modèle pour des zones spécifiques du cerveau connues pour participer à divers aspects de la cognition, de la perception à l’apprentissage, la prise de décision et la quantification de l'incertitude.
Les perspectives du projet postdoctoral devraient informer sur la manière dont l'imagerie IRMf et les enregistrements électrophysiologies invasifs et non invasifs peuvent être utilisés pour tester les théories de ce modèle. En outre, le candidat devra interagir avec d'autres activités du CEA liées au développement d'accélérateurs d'IA analogiques basés sur le bruit.
Étude des spécificités des architectures très distribuées pour les besoins de décision et de contrôle
Nos infrastructures électriques ont connu et connaîtront encore de profondes mutations dans les prochaines décennies.
La croissance rapide de la part des énergies renouvelables dans la production d'électricité nécessite de trouver des solutions pour sécuriser les systèmes énergétiques notamment en ce qui concerne les aspects de variabilité, de stabilité et d'équilibrage du système électrique et de protection de l'infrastructure du réseau elle-même.
L'objet de cette étude est d'aider à concevoir de nouvelles méthodes de décision, spécialement adaptées aux architectures de contrôle hautement distribuées pour les réseaux d'énergie. Ces nouvelles méthodes devront être évaluées en terme de performance, de résilience, de robustesse et éprouvées en présence de différents aléas et même de byzantins.
Hybridation de LLMs pour l’ingénierie des exigences
Le développement de systèmes physique ou numériques est un processus complexe mêlant des défis techniques et humains. La première étape consiste à donner corps aux idées en rédigeant des spécifications ou un cahier des charges du système en devenir. Généralement écrits en langage naturel par des analystes fonctionnels (business analysts), ces documents sont des pièces maîtresses qui lient toutes les parties prenantes pendant toute la durée du projet et facilite le partage et la compréhension de ce qu’il faut faire. L’ingénierie des exigences propose diverses techniques (revues, modélisation, formalisation, etc.) pour réguler ce processus et améliorer la qualité (cohérence, complétude, etc.) des exigences produites, dans le but de détecter et corriger les défauts avant même l’implémentation du système.
Dans le domaine de l’ingénierie des exigences, l’arrivée récente des réseaux de neurones à très grands modèles (LLM) a la capacité de « changer la donne » [4]. Nous proposons de soutenir le travail de l’analyste fonctionnel avec un outil qui facilite et fiabilise la rédaction du référentiel d'exigences. L’outil exploitera un agent conversationnel de type transformeur/LLM (tels que ChatGPT ou Lama) combiné à des méthodes rigoureuses d'analyse et de conseil. Il proposera des options de réécriture des exigences dans un format compatible avec les normes INCOSE ou EARS, analysera les résultats produits par le LLM, et fournira un audit de qualité des exigences.
Moonshot robotique : jumeau numérique d’un procédé de découpe laser et mise en œuvre avec un robot auto-apprenant
Un des principaux challenges au déploiement de la robotique dans l’industrie est de proposer des robots intelligents, capables de comprendre le contexte dans lequel ils évoluent et facilement programmables sans compétences avancées en robotique et en informatique. Afin de permettre à un opérateur non expert de définir des tâches réalisées ensuite par un robot, le CEA développe différents outils : interface de programmation intuitive, apprentissage par démonstration, skill-based programming, interface avec la simulation interactive …
Lauréat de l’appel à projet « moonshot » des Missions Numériques du CEA le projet « Robot auto-apprenant » propose d’apporter des ruptures très significatives pour la robotique du futur en lien avec la simulation. Un démonstrateur intégrant ces briques technologiques est attendu sur plusieurs cas d’usages dans différents centres CEA.
Cette offre de post-doc concerne la mise en œuvre du démonstrateur CEA/DES (Direction des Energies)sur le cas d’usage de la découpe laser sous contraintes pour l'A&D au Laboratoire de Simulation et des Techniques de Démantèlement (LSTD) au CEA Marcoule.
Accélération par GPU d'un code de dynamique des gaz préexistant.
Le code Triclade, développé au CEA-DAM, est un code DNS tridimensionnel écrit en C++ MPI résolvant les équations de Navier-Stockes compressibles pour un mélange binaire de gaz parfaits sur des maillages cartésiens. Il est utilisé, en particulier, pour simuler le mélange turbulent se produisant aux interfaces entre fluides sous l'effet d'instabilités hydrodynamiques.
Le(a) candidat(e) aura pour tâche l'amélioration des performances de l'application en mettant en place un nouveau degré de parallélisme basé sur une programmation sur carte graphique (GPU). Le code ainsi produit devra réduire au mieux la divergence entre les approches CPU et GPU, en permettant notamment d'unifier les appels aux fonctions calculatoires de manière à masquer l'utilisation explicite des accélérateurs. Pour ce faire, il (elle) pourra se baser sur une API existante (telle que Kokkos), ou, suivant les besoins, des directives de précompilations (telles que OpenMP). Le(a) candidat(e) sera amené(e) à collaborer fortement avec plusieurs autres équipes travaillant autour de l'accélération GPU.
Une bonne connaissance de la programmation C/C++, des systèmes distribués (calculateurs) ainsi que de la programmation sur carte graphique seront nécessaires à la concrétisation de ces objectifs. Des connaissances en mécanique des fluides seraient appréciées.
Développement et optimisation de techniques de rafinement de maillage adaptatif (AMR) pour des problèmes d'intéraction fluide/structure dans un contexte de calcul haute performance
Le CEA développe actuellement un nouveau code de simulation pour la mécanique des structures et des fluides compressibles : Manta. Ce code a pour double objectif d'unifier les fonctionnalités des codes historiques implicite et explicite du CEA et d'être nativement orienté vers le calcul intensif. Grâce à de nombreuses méthodes numériques (éléments finis, volumes finis, résolutions de problèmes implicites ou explicites, ...), Manta permet de simuler différents types de problèmes mécaniques dynamiques ou statiques pour la structure et le fluide, ainsi que l'interaction fluide-structure.
Dans le cadre de la recherche d'optimisation et de gain en temps de calcul, une des techniques incontournables pour améliorer la précision des solutions tout en maîtrisant les coûts de calcul est l'adaptation dynamique du maillage (ou AMR pour « Adaptive Mesh Refinement »).
Ce postdoc s'attache à la définition et à la mise en œuvre d'algorithmes d'AMR dans un contexte de calcul haute performance pour des problèmes faisant intervenir des fluides et des structures en intéraction.
Une tâche préliminaire consistera à implémenter des fonctionnalités de raffinement de maillage hiérarchique dans Manta (sous-découpage/fusion de cellules, transferts des champs, critères de raffinement, création de liaisons pour les « hanging-nodes »). Ces travaux se feront si possible en s'appuyant sur des librairies externes.
Dans un second temps, il s'agira d'optimiser les performances des calculs parallèles à mémoire distribuée. En particulier, il sera essentiel de définir une stratégie d'équilibrage de charge entre les processus MPI, en particulier dans le cadre de problèmes d'intéraction fluide/structure.
Enfin, en particulier pour des calculs explicites, il faudra définir et mettre en œuvre des techniques d'adaptation du pas de temps en fonction du niveau de raffinement.
Ces deux derniers points donneront lieu à une ou plusieurs publications dans des revues spécialisées.
Sûreté et assurance des systèmes basés Intelligence Artificielle
Le poste est lié à l’évaluation de la sûreté et à l’assurance des systèmes basé IA (Intelligence Artificielle). Actuellement, pour un système n’utilisant pas des composants d’apprentissage automatique, la sûreté fonctionnelle est évaluée avant le déploiement du système et les résultats de cette évaluation sont compilés dans un dossier de sécurité qui reste valable pendant toute la durée de vie du système. Pour les nouveaux systèmes intégrant des composants d’IA, en particulier les systèmes auto-apprenants, une telle approche d’ingénierie et d’assurance n’est pas applicable car le système peut présenter un nouveau comportement face à des situations inconnues pendant son fonctionnement.
L’objectif du post-doc sera de définir une approche d’ingénierie pour effectuer une évaluation de la sûreté des systèmes basés IA. Un deuxième objectif est de définir les artefacts du dossier d’assurance (objectifs, preuves, etc.) pour obtenir et préserver une confiance justifiée dans la sûreté du système tout au long de sa durée de vie, en particulier pour les systèmes basés IA à apprentissage opérationnel. L’approche sera mise en œuvre dans un framework open-source qui sera évaluée sur des applications industrielles.
Le titulaire du poste rejoindra une équipe de recherche et développement dans un environnement très stimulant avec des opportunités uniques de développer un solide portefeuille technique et de recherche. Il devra collaborer avec des partenaires académiques et industriels, contribuer et gérer des projets nationaux et européens, préparer et soumettre du matériel scientifique pour publication, fournir des conseils aux doctorants.
Tâches d’assemblages industrielles robotisées de haute précision avec apprentissage par renforcement basé sur le transfert sim2real
La manipulation et l’assemblage robotique de haute précision pour saisir ou construire des objets est un enjeu majeur pour l’industrie. Cependant, la flexibilité et l’agilité des systèmes actuels sont encore trop limitées pour répondre efficacement aux besoins d’adaptation rapide à un nouvel environnement ou à une nouvelle production.
L’objectif de ce post-doc est de lever ce verrou en développant un outil qui permet de réaliser des tâches industrielles d’insertion fine de haute précision en se basant sur un apprentissage par renforcement basé sur le transfert sim2real.
Pour fixer le cadre, nous nous limitons dans cette étude aux tâches d’assemblage de produits industriels à partir de pièces dont on dispose de la CAO. On commencera par le World Robot Challenge avant de proposer une généralisation vers d’autre types de tâches d’assemblage proposées par des industriels automobiles et aéronautiques avec qui le CEA-LIST collabore actuellement.
Application d’une approche IDM à la planification basée sur l’IA pour les systèmes robotiques et autonomes
La complexité de la robotique et des systèmes autonomes ne peut être gérée qu’avec des architectures logicielles bien conçues et des chaînes d’outils intégrées qui supportent l’ensemble du processus de développement. L’ingénierie dirigée par les modèles (IDM) est une approche qui permet aux développeurs de la robotique et des systèmes autonomes de passer d’un paradigme centré implémentation à un paradigme centré connaissances du domaine ce qui permet d’améliorer l’efficacité, la flexibilité et la séparation des préoccupations des différents acteurs du développement de ce type de système. L’un des principaux objectifs des approches IDM est d’être intégré aux infrastructures de développement disponibles de la communauté robotique et systèmes autonomes, telles que le middleware ROS, ROSPlan pour la planification des tâches robotiques, BehaviorTree.CPP pour leur exécution et suivi et Gazebo pour la simulation.
L’objectif de ce postdoc est d’étudier et de développer des architectures logicielles modulaires, composables et prédictibles ainsi que des outils de conception interopérables basés sur des approches basées sur des modèles, au lieu d’être centrées sur le code. Le travail sera réalisé dans le cadre de projets européens tels que RobMoSys (www.robmosys.eu), ainsi que dans d’autres initiatives pour les systèmes robotiques et autonomes sur la planification des tâches basée sur l’IA et leur exécution. Le principal objectif est de réduire les efforts des ingénieurs et de permettre ainsi le développement de systèmes robotiques autonomes plus avancés et plus complexes à un coût abordable. Pour ce faire, le post-doctorant contribuera à la mise en place et à la consolidation d’un écosystème, d’une chaîne d’outils et d’une communauté dynamique qui offriront un cadre unifié de conception, de planification et simulation, d’évaluation de la sécurité et un environnement formel de validation et de vérification.