Offre de postdoctorat (H/F) - Vers une traduction fiable du langage naturel en spécifications formelles pour les contrats intelligents

Description du Poste

Les Missions

La personne recrutée contribuera notamment aux activités suivantes :

Conception de méthodes de traduction sémantique : développer des approches permettant de traduire des instructions en langage naturel en formules logiques formelles.

Développement d'un langage naturel contrôlé : étudier la définition d'un langage adapté au domaine, intégrant notamment des variables, des appels de fonctions et des éléments issus des arbres de syntaxe abstraite (Abstract Syntax Trees, AST) des contrats intelligents.

Analyse syntaxique et sémantique : concevoir des méthodes de parsing permettant d'identifier les structures linguistiques pertinentes et de construire les représentations sémantiques correspondantes.

Approches fondées sur l'intelligence artificielle : explorer et comparer différentes méthodes, notamment les modèles de langue préentraînés, l'apprentissage par renforcement et les modèles à variables latentes.

Articulation entre méthodes symboliques et neuronales : étudier la complémentarité entre les approches grammaticales et sémantiques formelles et les méthodes d'apprentissage automatique, afin d'améliorer la fiabilité des traductions.

Évaluation expérimentale : définir et mettre en œuvre des protocoles d'évaluation portant sur la fidélité sémantique, la correction logique, la robustesse et l'utilisabilité des méthodes proposées.

Selon les besoins du projet, les travaux pourront également porter sur l'extension des méthodes développées à des textes en langage naturel moins contraint, ainsi que sur la résolution des ambiguïtés et la clarification interactive des spécifications.

L'Activité

Conception de méthodes de traduction sémantique : traduire les exigences exprimées en langage naturel en formules logiques formelles, notamment en logique temporelle linéaire (LTL).
Développement d'un langage naturel contrôlé : définir un langage adapté à la spécification des contrats intelligents, intégrant les variables, les appels de fonctions et les arbres de syntaxe abstraite (AST).
Analyse syntaxique et sémantique : concevoir des méthodes de parsing pour identifier les structures linguistiques et générer des représentations logiques.
Développement de méthodes d'intelligence artificielle : explorer les modèles de langue préentraînés, l'apprentissage par renforcement et les approches à variables latentes.
Combinaison des approches neuronales et symboliques : améliorer la fiabilité et la correction des traductions par l'intégration de contraintes formelles.
Évaluation expérimentale : mesurer la fidélité sémantique, la correction logique, la robustesse et l'utilisabilité des méthodes développées.
Désambiguïsation et clarification interactive : étendre les méthodes au langage naturel libre et résoudre les ambiguïtés des exigences.
Valorisation scientifique : contribuer aux publications et aux travaux de recherche du projet ANR BBSYTER sur la vérification formelle des contrats intelligents.

Votre Profil

Compétences

La personne candidate devra être titulaire d'un doctorat, ou être en voie de l'obtenir, en informatique, traitement automatique des langues, linguistique computationnelle, intelligence artificielle, logique, méthodes formelles ou dans une discipline proche.

Une expérience de recherche dans un ou plusieurs des domaines suivants sera particulièrement appréciée :

Traitement automatique des langues, notamment compréhension du langage, analyse sémantique ou parsing sémantique.

Sémantique formelle, grammaires computationnelles ou interface entre syntaxe et sémantique.

Logique formelle, notamment logique temporelle, grammaires catégorielles typées ou formalismes apparentés.

Apprentissage automatique appliqué à la prédiction structurée, à la modélisation du langage ou à la construction de représentations sémantiques.

Raisonnement automatisé, vérification formelle ou traduction de spécifications en langage naturel vers des représentations formelles.

Des connaissances en contrats intelligents, sémantique des langages de programmation, apprentissage par renforcement ou modèles à variables latentes constitueront des atouts supplémentaires.

Les candidatures de personnes issues aussi bien de l'intelligence artificielle et du TAL que de la logique et des méthodes formelles sont encouragées. Un intérêt marqué pour l'articulation entre approches statistiques, neuronales et symboliques sera particulièrement apprécié.

Votre Environnement de Travail

Contexte scientifique et objectifs

Ce postdoctorat s'inscrit dans le cadre du projet ANR BBSYTER (Blockchain-Based SYsTem vERification), consacré à la vérification des systèmes fondés sur la blockchain, avec un intérêt particulier pour la fiabilité et la correction des contrats intelligents (smart contracts).

La technologie blockchain connaît un développement considérable dans de nombreux domaines, notamment la finance, la santé, la traçabilité et la gestion d'actifs numériques. Les contrats intelligents, programmes exécutés sur une blockchain afin d'automatiser des règles et des transactions, jouent un rôle central dans cette évolution. Toutefois, leur déploiement soulève des enjeux majeurs de sécurité et de fiabilité : une vulnérabilité peut entraîner des pertes financières importantes ou compromettre le fonctionnement des systèmes concernés, tandis que l'immuabilité de la blockchain rend souvent les corrections particulièrement difficiles.

Dans ce contexte, les méthodes formelles constituent une approche essentielle pour spécifier, analyser et vérifier rigoureusement le comportement attendu des contrats intelligents.

Le projet ANR BBSYTER vise à contribuer au développement de méthodes de vérification adaptées aux systèmes fondés sur la blockchain. Un enjeu important consiste à faciliter l'expression des propriétés que ces systèmes doivent respecter, puis à les traduire en spécifications formelles exploitables par des outils de vérification.

Le postdoctorat proposé portera sur cet enjeu à l'interface de l'intelligence artificielle, du traitement automatique des langues et des méthodes formelles. Il visera à développer des méthodes permettant de traduire des exigences exprimées en langage naturel en formules de logique temporelle, notamment en logique temporelle linéaire (Linear Temporal Logic, LTL), afin de formaliser le comportement attendu des contrats intelligents.

Les travaux s'appuieront notamment sur l'étude d'un langage naturel contrôlé (Controlled Natural Language, CNL), conçu pour exprimer les spécifications des contrats intelligents de manière claire et non ambiguë. Ils mobiliseront des techniques d'analyse syntaxique et sémantique, des méthodes d'apprentissage automatique et, lorsque cela sera pertinent, des approches combinant modèles neuronaux et méthodes symboliques.

L'objectif est de contribuer au développement d'une chaîne de traitement permettant de passer des exigences formulées par les utilisateurs à des représentations logiques précises, en étudiant les conditions nécessaires à la fidélité sémantique, à la correction des traductions et à leur exploitation dans un processus de vérification formelle.

Selon l'avancement du projet, les travaux pourront également examiner la possibilité de traiter des formulations plus libres en langage naturel, ainsi que des mécanismes de désambiguïsation et de clarification interactive des exigences.

Rémunération et avantages

Rémunération

3131€

Congés et RTT annuels

44 jours

Pratique et Indemnisation du TT

Pratique et indemnisation du TT

Transport

Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€

À propos de l’offre

À propos du CNRS

Le CNRS est un acteur majeur de la recherche fondamentale à une échelle mondiale. Le CNRS est le seul organisme français actif dans tous les domaines scientifiques. Sa position unique de multi-spécialiste lui permet d’associer les différentes disciplines pour affronter les défis les plus importants du monde contemporain, en lien avec les acteurs du changement.

Le CNRS

Les métiers de la recherche