Post-Doctorant F/H Formally verified alignements for better interactive proof assistants

Contexte et atouts du poste

This project is part of the FRAIME joint project between Inria and Mitsubishi Research Europe (MERCE).

The widespread adoption of AI in many fields of society calls for techniques making AI safer and more trustworthy. Systems based on AI show impressive performance but their opacity makes them unreliable for industrial applications, since they do not offer any guarantee. In contrast, Formal Methods excel at logical reasoning, can prove properties of programs or detect bugs, but are often limited in their scalability.

In this project, we propose to explore on the one hand how Formal Methods can provide guarantees on AI systems, and on the other hand how AI can help Formal Methods to be more efficient and easier to use by practitioners. The vision is to intertwine Formal Methods and AI to efficiently design safe systems.

The project is driven by industrial use cases in the expertise of MERCE. We target th...