Job opportunities
Centres Inria associés
Type de contrat
Contexte
<p class="p1">The Epicure team at Inria Rennes is looking for a post-doc candidate with a strong background in either Artificial Intelligence (AI) or in formal methods (FM). The post-doc will join a collaboration between Inria and Mitsubishi Electric R&D Centre Europe (MERCE) on formal reasoning applied to AI for software engineering.</p>
<p class="p1">Epicure is a team with a longstanding experience on formal methods, proof assistants, program semantics, static analysis and abstract interpretation.</p>
<p class="p1">Epicure is a team with a longstanding experience on formal methods, proof assistants, program semantics, static analysis and abstract interpretation.</p>
Mission confié
<p class="p1">We are looking for a post-doc candidate with a strong experience in formal methods or 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.</p>
Principales activités
<p class="p1">In a preliminary step, we will 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/).</p>
<p class="p1">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.</p>
<p class="p1">• Sub-task A: Experimental study of invariant generation by LLMs using program logic tools (e.g. Frama-C, Why3) as a means to separate correct and incorrect program properties. Separation will be tested using both automatic provers and counterexample generators.</p>
<p class="p1">• 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).</p>
<p class="p1"><strong>References</strong><br />[1] Sandra Greiner, Noah Bühlmann, Manuel Ohrndorf, Christos Tsigkanos,<br />Oscar Nierstrasz, and Timo Kehrer. Automated generation of code<br />contracts: Generative ai to the rescue? In Proceedings of the 23rd ACM<br />SIGPLAN International Conference on Generative Programming: Concepts and<br />Experiences, pages 1–14, 2024.<br /><br />[2] A. Kamath, N. Mohammed, A. Senthilnathan, S. Chakraborty, P.<br />Deligiannis, S.-K. Lahiri, A. Lal, A. Rastogi, S. Roy, and R. Sharma.<br />Leveraging LLMs for Program Verification. In FMCAD’24, pages 107–118.<br />IEEE, 2024.<br /><br />[3] X. Si, A. Naik, H. Dai, M. Naik, and L. Song. Code2inv: A deep<br />learning Framework for Program Verification. In CAV’20, volume 12225 of<br />LNCS, pages 151–164. Springer, 2020.</p>
<p class="p1">[4] Samuel Teuber and Bernhard Beckert. Next steps in llm-supported java<br />verification. arXiv preprint arXiv:<span id="OBJ_PREFIX_DWT693_com_zimbra_phone" class="Object"><a href="callto:2502.01573, 2025">2502.01573, 2025</a></span>.<br /><br />[5] Haoze Wu, Clark Barrett, and Nina Narodytska. Lemur: Integrating<br />large language models in automated program verification. arXiv preprint<br />arXiv:<span id="OBJ_PREFIX_DWT694_com_zimbra_phone" class="Object"><a href="callto:2310.04870, 2023">2310.04870, 2023</a></span>.</p>
<p class="p1">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.</p>
<p class="p1">• Sub-task A: Experimental study of invariant generation by LLMs using program logic tools (e.g. Frama-C, Why3) as a means to separate correct and incorrect program properties. Separation will be tested using both automatic provers and counterexample generators.</p>
<p class="p1">• 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).</p>
<p class="p1"><strong>References</strong><br />[1] Sandra Greiner, Noah Bühlmann, Manuel Ohrndorf, Christos Tsigkanos,<br />Oscar Nierstrasz, and Timo Kehrer. Automated generation of code<br />contracts: Generative ai to the rescue? In Proceedings of the 23rd ACM<br />SIGPLAN International Conference on Generative Programming: Concepts and<br />Experiences, pages 1–14, 2024.<br /><br />[2] A. Kamath, N. Mohammed, A. Senthilnathan, S. Chakraborty, P.<br />Deligiannis, S.-K. Lahiri, A. Lal, A. Rastogi, S. Roy, and R. Sharma.<br />Leveraging LLMs for Program Verification. In FMCAD’24, pages 107–118.<br />IEEE, 2024.<br /><br />[3] X. Si, A. Naik, H. Dai, M. Naik, and L. Song. Code2inv: A deep<br />learning Framework for Program Verification. In CAV’20, volume 12225 of<br />LNCS, pages 151–164. Springer, 2020.</p>
<p class="p1">[4] Samuel Teuber and Bernhard Beckert. Next steps in llm-supported java<br />verification. arXiv preprint arXiv:<span id="OBJ_PREFIX_DWT693_com_zimbra_phone" class="Object"><a href="callto:2502.01573, 2025">2502.01573, 2025</a></span>.<br /><br />[5] Haoze Wu, Clark Barrett, and Nina Narodytska. Lemur: Integrating<br />large language models in automated program verification. arXiv preprint<br />arXiv:<span id="OBJ_PREFIX_DWT694_com_zimbra_phone" class="Object"><a href="callto:2310.04870, 2023">2310.04870, 2023</a></span>.</p>
Compétences
<ul>
<li>Strong background in either formal methods (FM) or artificial intelligence (AI)</li>
<li>Interest and curiosity in formal methods if your background is AI </li>
<li>Interest and curiosity in artificial intelligence if your background is FM</li>
<li>Solid background in software development</li>
<li>Familiarity with functional programming is a plus</li>
<li>Good writing skills in english</li>
</ul>
<li>Strong background in either formal methods (FM) or artificial intelligence (AI)</li>
<li>Interest and curiosity in formal methods if your background is AI </li>
<li>Interest and curiosity in artificial intelligence if your background is FM</li>
<li>Solid background in software development</li>
<li>Familiarity with functional programming is a plus</li>
<li>Good writing skills in english</li>
</ul>
Référence
2025-09680
Thème
Domaine d'activité