Les missions du poste
A propos d'Inria
Inria est l'institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l'interface d'autres disciplines. L'institut fait appel à de nombreux talents dans plus d'une quarantaine de métiers différents. 900 personnels d'appui à la recherche et à l'innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'eorce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.
Engineer for Generative Formal Code Annotations
Contrat renouvelable : Oui
Niveau de diplôme exigé : Thèse ou équivalent
Fonction : Ingénieur scientifique contractuel
Niveau d'expérience souhaité : De 3 à 5 ans
A propos du centre ou de la direction fonctionnelle
Le centre Inria de l'Université de Rennes est l'un des huit centres d'Inria et compte plus d'une trentaine d'équipes de recherche. Le centre Inria est un acteur majeur et reconnu dans le domaine des sciences numériques. Il est au coeur d'un riche écosystème de R&D et d'innovation : PME fortement innovantes, grands groupes industriels, pôles de compétitivité, acteurs de la recherche et de l'enseignement supérieur, laboratoires d'excellence, institut de recherche technologique.
Contexte et atouts du poste
The Epicure team at Inria Rennes is looking for an engineer with a strong background in Artificial Intelligence (AI). The engineer will join a collaboration between Inria and Mitsubishi Electric R&D Centre Europe (MERCE) on formal reasoning applied to AI for software engineering.
Epicure is a team with a longstanding experience on formal methods, proof assistants, program semantics, static analysis and abstract interpretation.
Mission confiée
We are looking for an engineer doc candidate with a strong experience in Large Language Models (LLMs) or Reinforcement learning (RL) to propose new AI techniques to generate correct and informative formal code annotations from program source. In particular, we want to evaluate the potential of Large Language Models and Reinforcement Learning for improving the process of engineering verified software. In deductive verification, properties on the software are stated in a specific program logic and proven by automatic provers. For the proofs to be completed, the user is generally required to annotate the code with program invariants, i.e., additional logic formulas to help the automatic prover to carry out the proof. Finding an invariant that unlocks a stuck proof is a tedious, time-consuming and non-trivial. This problem is one of the main obstacle for a wider adoption of deductive verification techniques for the formal verification of programs.
Principales activités
We first want to evaluate the capabilities of existing LLMs to produce relevant code annotations, given a program source and a final property to prove on this program. We plan to compare with what can be obtained using traditional program verification techniques such as abstract interpretation. The target language is C and Frama-C code annotations (https://frama-c.com/). MERCE has an extensive knowledge and corpus of industrial C programs. A possible stepping stone is the WhyML language with Why3 code annotations (https://www.why3.org/).
LLMs have proved successful in guessing simple invariants [5, 2, 3, 1, 4], but it remains to be determined how good they are to infer more complex invariants. This is due to the small size of the available corpus of verified/annotated programs. To overcome this limitation, the second step of the project will investigate the potential for training an ML model for generating invariants using an RL loop.
- Sub-task A: Implement invariant guessing on program logic tools (e.g. Frama-C, Why3) with existing LLMs and investigate their strengthes and weaknesses.
- Sub-task B: Building an RL loop for training a dedicated ML model to infer invariants. Generated invariants will be analyzed by automatic provers for positive scoring and counterexample generators for negative scoring. Mutation of the verified code will be used to detect and reject the weakest properties (e.g., useless tautologies).
[1] Sandra Greiner, Noah B¨uhlmann, Manuel Ohrndorf, Christos Tsigkanos, Oscar Nierstrasz, and Timo Kehrer. Automated generation of code contracts: Generative ai to the rescue? In Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, pages 1-14, 2024.
[2] A. Kamath, N. Mohammed, A. Senthilnathan, S. Chakraborty, P. Deligiannis, S.-K. Lahiri, A. Lal, A. Rastogi, S. Roy, and R. Sharma. Leveraging LLMs for Program Verification. In FMCAD'24, pages 107-118. IEEE, 2024.
[3] X. Si, A. Naik, H. Dai, M. Naik, and L. Song. Code2inv: A deep Learning Framework for Program Verification. In CAV'20, volume 12225 of LNCS, pages 151-164. Springer, 2020.
[4] Samuel Teuber and Bernhard Beckert. Next steps in llm-supported java verification. arXiv preprint arXiv:2502.01573, 2025.
[5] Haoze Wu, Clark Barrett, and Nina Narodytska. Lemur: Integrating large language models in automated program verification. arXiv preprint arXiv:2310.04870, 2023.
Compétences
Skills:
* Strong experience in artificial intelligence
* Solid background in software development
* Good writing skills in english
* Familiarity with functional programming is a plus
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
- Sécurité sociale
Rémunération
A partir de2695€ brut ou selon diplomes et expériences