Thèse de doctorat: Génération assistée par LLM de modèles matériels fonctionnels et formels

Technologies micro et nano Thèse de doctorat: Génération assistée par LLM de modèles matériels fonctionnels et formels H/F « Rejoignez le CEA pour donner du sens à votre activité, mener ou soutenir des projets de R&D nationaux et internationaux, cultiver et faire vivre votre esprit de curiosité. »EN SYNTHESE, QU’EST-CE QUE NOUS VOUS PROPOSONS ?Nous cherchons à pourvoir une offre de thèse. Ce poste est basé sur le site Nano-Innov de Paris-Saclay, Essonne (91). Ce poste est à pourvoir pour septembre 2026.CONTEXTELes systèmes matériels modernes, tels que les processeurs RISC-V, les accélérateurs et les systèmes sur puce hétérogènes, reposent fortement sur des simulateurs fonctionnels et des modèles de vérification formelle afin de garantir la correction, la fiabilité et la sécurité. Toutefois, la construction et la maintenance manuelles de ces modèles à partir des spécifications de conception sont lentes et deviennent de plus en plus complexes à mesure que les architectures se complexifient. Cet effort manuel constitue aujourd’hui un goulet d’étranglement majeur dans les flots contemporains de conception et de vérification matérielles.OBJECTIFS DE LA THESEL’objectif de cette thèse est de développer une méthodologie unifiée, pilotée par l’IA, pour la co-génération automatique de modèles matériels fonctionnels et formels directement à partir des spécifications de conception. Les travaux porteront sur la génération de modèles fonctionnels exécutables, tels que des simulateurs au niveau jeu d’instructions, ainsi que de modèles de vérification formelle capturant précisément la sémantique architecturale.La thèse développera des chaînes de génération basées sur les LLMs, combinant l’apprentissage par renforcement avec des boucles de retour pilotées par les outils, afin d’affiner itérativement une représentation intermédiaire inspirée des prompts et de guider la génération des modèles vers la correction, la cohérence et le succès de la vérification formelle. L’objectif à long terme est de proposer un environnement de co-génération correcte par construction permettant de réduire significativement l’effort de modélisation manuelle tout en assurant un fort alignement entre les vues fonctionnelles et formelles de l’architecture.La méthodologie développée sera évaluée sur des cas d’étude matériels réalistes et open-source, avec un accent particulier sur les architectures RISC-V, leurs extensions et les accélérateurs matériels. Les résultats expérimentaux permettront d’évaluer la précision des modèles générés, leur cohérence mutuelle, leur capacité à passer à l’échelle, ainsi que les gains de productivité obtenus par rapport aux approches de modélisation manuelle. Retrouvez cette offre sur le site de l'INSTN : https://instn.cea.fr/these/generation-assistee-par-llm-de-modeles-materiels-fonctionnels-et-formels  #CEA-List ; #PhD ; #Researcher ; #Chercheur Master en architecture des ordinateurs, génie informatique, systèmes embarqués ou informatiqueSolides compétences en programmation en Python et en C et/ou C++Intérêt marqué pour l’architecture matérielle, l’EDA ou la vérificationUne bonne base en apprentissage automatique est attendueUne expérience ou une familiarité avec les méthodes formelles est un plus Conformément aux engagements pris par le CEA en faveur de l'intégration des personnes handicapées, cet emploi est ouvert à toutes et à tous. Le CEA propose des aménagements et/ou des possibilités d'organisation pour l'inclusion des travailleurs handicapés.