Postdoctoral Research Position (M/F) – Towards Reliable Translation of Natural Language into Formal Specifications for Smart Contracts
New
- Researcher in "Contrat de projet"
- 12 months
- Doctorate
This offer is available in English version
This offer is open to people with a document recognizing their status as a disabled worker.
Offer at a glance
The Unit
Laboratoire d'Informatique de Paris-Nord
Contract Type
Researcher in "Contrat de projet"
Working hHours
Full Time
Workplace
93430 VILLETANEUSE
Contract Duration
12 months
Date of Hire
01/03/2027
Remuneration
From 3131€ gross per month
Apply Application Deadline : 19 November 2026 23:59
Job Description
Missions
The candidate will contribute to the following research activities:
- Design of semantic translation methods: Develop approaches for translating natural language instructions into formal logical formulas.
- Development of a Controlled Natural Language: Investigate the design of a language tailored to the application domain, incorporating variables, function calls, and information extracted from the Abstract Syntax Trees (ASTs) of smart contracts.
- Syntactic and semantic parsing: Design parsing methods to identify relevant linguistic structures and construct the corresponding semantic representations.
- AI-based approaches: Explore and compare different methods, including pretrained language models, reinforcement learning, and latent-variable models.
- Integration of symbolic and neural methods: Investigate the complementarity between formal grammatical and semantic approaches and machine learning techniques, with the aim of improving the reliability of translations.
- Experimental evaluation: Design and implement evaluation protocols to assess semantic fidelity, logical correctness, robustness, and usability of the proposed methods.
Depending on the needs and progress of the project, the research may also explore extending the developed methods to less constrained natural language texts, as well as techniques for ambiguity resolution and interactive clarification of specifications.
Activity
.
Your Profil
Skills
Applicants should hold a PhD, or be close to completing a PhD, in Computer Science, Natural Language Processing (NLP), Computational Linguistics, Artificial Intelligence, Logic, Formal Methods, or a related discipline.
Research experience in one or more of the following areas will be particularly appreciated:
Natural Language Processing, particularly natural language understanding, semantic analysis, or semantic parsing.
Formal semantics and computational grammar, including syntax-semantics interfaces.
Formal logic, particularly temporal logic, typed categorial grammars, or related formalisms.
Machine learning applied to structured prediction, language modelling, or the construction of semantic representations.
Automated reasoning and formal verification, or the translation of natural language specifications into formal representations.
Knowledge of smart contracts, programming language semantics, reinforcement learning, or latent-variable models will be considered an additional asset.
Applications from candidates with backgrounds in either artificial intelligence and NLP or logic and formal methods are encouraged. A strong interest in combining statistical, neural, and symbolic approaches will be particularly valued.
Your Work Environment
This postdoctoral position is part of the French National Research Agency (ANR) project BBSYTER (Blockchain-Based SYsTem vERification), which focuses on the verification of blockchain-based systems, with particular emphasis on the reliability and correctness of smart contracts.
Blockchain technology has experienced considerable growth across a wide range of application domains, including finance, healthcare, traceability, and digital asset management. Smart contracts, which are programs executed on a blockchain to automate rules and transactions, play a central role in this development. However, their deployment raises significant security and reliability challenges. Vulnerabilities can lead to substantial financial losses or compromise the operation of the systems concerned, while the immutability of blockchain technology often makes corrections particularly difficult.
In this context, formal methods provide essential tools for specifying, analysing, and rigorously verifying the expected behaviour of smart contracts.
The ANR BBSYTER project aims to contribute to the development of verification methods tailored to blockchain-based systems. A key challenge is to facilitate the expression of the properties these systems are expected to satisfy and to translate them into formal specifications that can be processed by verification tools.
The proposed postdoctoral research will address this challenge at the intersection of artificial intelligence, natural language processing (NLP), and formal methods. It will focus on developing methods for translating requirements expressed in natural language into temporal logic formulas, particularly Linear Temporal Logic (LTL), in order to formalise the expected behaviour of smart contracts.
The research will notably investigate the use of a Controlled Natural Language (CNL) designed to express smart contract specifications clearly and unambiguously. It will draw on syntactic and semantic parsing techniques, machine learning methods and, where appropriate, approaches combining neural models with symbolic methods.
The objective is to contribute to the development of a processing pipeline that translates user requirements into precise logical representations, while investigating the conditions necessary to ensure semantic fidelity, translation correctness, and effective integration into a formal verification process.
Depending on the progress of the project, the research may also explore the extension of the proposed methods to less constrained natural language formulations, as well as ambiguity resolution and interactive clarification mechanisms for user requirements.
Constraints and risks
.
Compensation and benefits
Compensation
From 3131€ gross per month
Annual leave and RTT
44 jours
Remote Working practice and compensation
Pratique et indemnisation du TT
Transport
Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€
About the offer
| Offer reference | UMR7030-MANZAR-001 |
|---|---|
| CN Section(s) / Research Area | Information sciences: bases of information technology, calculations, algorithms, representations, uses |
About the CNRS
The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. Its unique position as a multi-specialist allows it to bring together different disciplines to address the most important challenges of the contemporary world, in connection with the actors of change.
Create your alert
Don't miss any opportunity to find the job that's right for you. Register for free and receive new vacancies directly in your mailbox.