Postdoctoral Researcher

AI and Formal Methods for Intent Contractualization

AI4I · PRAXISTurin, ItalyFull time · Two years

Call upcoming

Investigate how agents can turn goals and constraints into precise, understood agreements.

Your role

You will investigate how human intent can become a trustworthy basis for autonomous action. When requirements are incomplete or ambiguous, producing a precise specification is only part of the problem: it is also essential to establish whether it captures the decisions and restrictions that matter to the people it represents. The position offers a research agenda at the boundary of AI and formal methods, centred on specification, reasoning and validation.

You will develop new foundations and methods for specification using learning methods: how should a system represent competing interpretations, discover what is missing, and use interaction to improve its understanding? The agenda brings together formal analysis, synthesis, algorithms and empirical investigation, with distinct research questions across these areas. The position offers scope for theoretically oriented research in formal methods as well as systems using learning methods, with ownership of an identifiable research direction.

Within PC2, these questions arise when agents turn informal requirements into candidate contracts and actively test their meaning. Research directions include clarification, synthesis guided by examples and counterexamples, and adversarial specification testing: searching for behaviour that satisfies a written contract but conflicts with the intended requirement. Such interactions can reveal unintended permissions, unnecessary restrictions or choices that require further input from the principal.

You will work with the ML research engineer to develop and train agents that improve at these processes, and with the calculus researchers on their formal representations. The agenda includes selecting informative clarification questions, using feedback from counterexamples and learning across repeated refinement. Evaluation will distinguish formal acceptance from fidelity to intended requirements, with realistic and held out cases developed alongside the empirical team. Prior expertise in training large models or a specific proof assistant is not required.

Your contribution to the field

Your contribution will advance intent contractualization as a research area connecting formal specification, synthesis and learning. You will develop methods for exposing ambiguity, testing the consequences of alternative specifications and using interaction to refine contracts, together with evidence about their fidelity to intended requirements. The resulting algorithms, formal analyses and evaluation methods will establish a distinctive contribution to how autonomous systems acquire the rules they are expected to follow.

An initial research or development direction

An example starting point is to investigate how counterexamples and targeted questions help an agent resolve ambiguity, comparing an interactive method with direct contractualization. The analysis will examine agreement with independently reviewed requirements, unintended permissions, omissions and review effort.

Essential background

A PhD in computer science, mathematics or a closely related field; the required stage of completion and formal eligibility will be specified in the final call.
Research experience in formal methods, including dependent type theory and relevant work in specification, synthesis, verification or automated reasoning.
Ability to formulate a precise research question and develop rigorous methods or analyses; profiles focused on foundations or implementation are both welcome.
Interest in using learning and interaction to improve specification and reasoning, and in collaborating with researchers developing and training agents.

Additional relevant experience

Methods guided by counterexamples, program synthesis, interactive specification or formal analysis of requirements.
Language models, active learning, agent training or evaluation of generated specifications.
Practical experience with proof assistants or research software. Expertise in Lean is welcome but is not the only relevant background.

Candidates with depth in a relevant area and an interest in connecting it to others are encouraged to apply. Evidence of your contribution can include research papers, formal developments, substantial software or a clear account of technical work that cannot be shared publicly.

Research environment and development

Your primary supervisor will be Carlo Ciliberto. PC2 is a joint effort involving PRAXIS at AI4I, the REAL team at Bocconi and STAMP at Inria. The role requires close collaboration with the other participating groups, including opportunities for extended visiting periods at their laboratories, bringing your work into close contact with complementary expertise in machine learning, formal methods and systems.

The position is based in Turin, Italy. Remote working arrangements can be agreed when working from another laboratory in the PC2 collaboration. The timing and practical arrangements for research visits will be discussed with you and the participating hosts.

Computational resources. AI4I's HPC infrastructure provides approximately 150 NVIDIA GPUs (80 Blackwell B200 and 68 Hopper H200) and 5 PB of storage, supporting this project in agentic AI training, testing and validation.

Application materials

Please prepare:

Your CV, including relevant research or technical experience.
A short statement of fit and interests, explaining what attracts you to the role, the experience you would bring and directions you would be interested in exploring. A full research proposal is not required.
One or two representative contributions, such as papers, formal developments or software. Briefly explain your own contribution. An account of work that cannot be shared publicly is welcome; a public repository is not required.

Submission instructions and the application deadline will be published here when the call is finalised.