Post-Doctorant Formally Verified Alignements For Better Interactive Proof Assistants H/F

INRIA

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

Type de contrat : CDD

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Post-Doctorant

A propos du centre ou de la direction fonctionnelle

The Inria Centre at Rennes University is one of Inria's nine centres and has more than thirty research teams. The Inria Centre is a major and recognized player in the field of digital sciences. It is at the heart of a rich R&D and innovation ecosystem: highly innovative PMEs, large industrial groups, competitiveness clusters, research and higher education players, laboratories of excellence, technological research institute, etc.

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 oer 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 ecient and easier to use by practitioners. The vision is to intertwine Formal Methods and AI to eciently design safe systems.

The project is driven by industrial use cases in the expertise of MERCE. We target the following four challenges: user-assisted factory automation code generation, correctness of C programs, safe and optimal system control, easier and more automated proof assistant.

Mission confiée

In interactive theorem proving, a single mathematical concept may have multiple representations, and proofs often involve reasoning across these. Without automated support such as proof transfer, theorems stated using dierent representations cannot be easily combined-requiring anything from light to substantial manual eort from the user.

A seamless and formally verified transfer of formal definitions and statements, that blurs irrelevant syntactic differences between semantically similar concepts has many potential benefits, for enhancing the productivity of user. In this project we will specifically address the two following applications :
- the discovery and validation of existing results in the available ecosystem of formal libraries of the prover, or even that of other provers based on similar foundations;
- the improvement and maintenance of existing code, enhancing its robustness and conciseness, via automated proof-repair.

While some existing prototypes already address this challenge, proof assistants based on dependent type theory still demand human intervention to establish such transfers, even when the equivalences are straightforward and left implicit in mathematical practice.

Recently, , a proof transfer framework based on a generalized form of , enabled by a novel formulation of type equivalence. Trocq is implemented in the Rocq prover assistant, using the Rocq-Elpi metaprogramming language.

The objective of this project is to make this framework scale, and accommodate the needs created by AI-generated formal code, e.g. by translation or by refactoring tools.

Principales activités

• Conduct basic research
• Write formal code, mostly in Rocq and its meta-programming facilities
• Write and submit scientific articles, deliver talks that describe the obtained contributions

Compétences

Knowledge of French is not required.

Avantages

• Restauration subventionnée
• Transports publics remboursés partiellement
• Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
• Possibilité de télétravail (après 6 mois d'ancienneté) et aménagement du temps de travail
• Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
• Prestations sociales, culturelles et sportives (Association de gestion des oeuvres sociales d'Inria)
• Accès à la formation professionnelle

Rémunération

Monthly gross salary amounting to 2788 euros