Engineer for Generative Formal Code Annotations

Engineer for Generative Formal Code Annotations

Renewable contract: Yes

Level of qualifications required: PhD or equivalent

Fonction: Temporary scientific engineer

Level of experience: From 3 to 5 years

About the research centre or Inria department

Context

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 longstanding experience on formal methods, proof assistants, program semantics, static analysis and abstract interpretation.

Assignment

We are looking for an engineer 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 LLMs and RL 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 obstacles for a wider adoption of deductive verification techniques for the formal verification of programs.

Main activities

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 (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 (why3.org).

LLMs have proved successful in guessing simple invariants, but it remains to be determined how good they are to infer more complex invariants. 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 strengths 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).

Skills

• Strong experience in artificial intelligence
• Solid background in software development
• Good writing skills in English
• Familiarity with functional programming is a plus

Instruction to apply

Defence Security: This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. relating to the protection of national scientific and technical potential (PPST). Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.

Recruitment Policy: As part of its diversity policy, all Inria positions are accessible to people with disabilities.

Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.

Remuneration

Warning: you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.