Starting Research Position

**Type de contrat**: CDD

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

**Fonction**: Chercheur contractuel

**A propos du centre ou de la direction fonctionnelle**:
Le centre Inria de Lyon est le 9ème centre de recherche Inria. Créé en janvier 2022, il regroupe environ 300 personnes au sein de 17 équipes de recherche et des services supports à la recherche.

Ses équipes sont localisées à Villeurbanne, à Lyon Gerland, ainsi qu’à Saint-Etienne.

Le centre de Lyon est présent dans les domaines du logiciel, du calcul distribué et haute performance, des systèmes embarqués, du calcul quantique et de respect de la vie privée dans le monde numérique, mais aussi de la santé et de la biologie numériques.

**Contexte et atouts du poste**:
**Le postdoc se déroulera dans le cadre d'une collaboration entre Guillaume Baudart, Marc Lelarge et Nicolas Tabareau,** dont **les objectifs sont d'appliquer des techniques d'apprentissage automatique à la génération automatique de code**, et en particulier pour les bibliothèques d'assistants de preuves, telles que des bibliothèques Rocq et Lean.

** La recherche sera menée dans le laboratoire LIP de l'ENS Lyon sous la supervision locale de Cyril Cohen,** au sein de l'équipe CASH et à **distance avec Guillaume Baudart, Marc Lelarge et Nicolas Tabareau**. Cependant, il y aura des réunions fréquentes, et des rencontres régulières en personne, avec les co-superviseurs et les participants du projet LLM4Code.

** Les frais de déplacement sont couverts dans les limites du barème en vigueur.**

**Mission confiée**:
**Mission**:
Avec l'aide des membres des projets et de leurs collaborateurs, la personne recrutée travaillera, en utilisant des techniques modernes d'IA, et en particulier des modèles de langue de grande taille (LLM), sur:

- les traductions automatisées à partir de, vers et entre les bibliothèques de mathématiques formalisées, entre assistants de preuves ou au sein du même assistant de preuve,
- l'automatisation de la documentation et de la recherche de théorème,
- la construction de preuve par collaboration entre plusieurs agents et des prouveurs.

Ces traductions peuvent nécessiter des modifications non triviales des assistants de preuve utilisés, telles que la création de plugins, l'utilisation de méta-programmation, ou la reformulation des bibliothèques de manière à mieux convenir à l'apprentissage automatique.

Il sera également nécessaire de mettre en place des techniques de programmation agentique, d'apprentissage supervisé (finetuning), et d'apprentissage par renforcement (reinforcement learning) sur des modèle existants, et d'évaluer la pertinence de chaque méthode.

Les résultats attendus de ce travail sont des publications de recherche, la production de logiciels et des présentations publiques en workshop

** Pour une meilleure connaissance du sujet de recherche proposé**:
L'état de l'art, la bibliographie et les références scientifiques évoluent rapidement. Nous suggérons de lire par exemple:

- Training Chain-of-Thought via Latent-Variable Inference
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
- Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
- Solving Formal Math Problems by Decomposition and Iterative Reflection
- Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
- Hilbert: Recursively Building Formal Proofs with Informal Reasoning

**Collaboration**:
La personne recrutée sera principalement en contact avec Cyril Cohen à Lyon, ainsi que Guillaume Baudart, Marc Lelarge et Nicolas Tabareau, mais travaillera également à distance avec d'autres membres de LLM4Code.

** Responsabilités**:
La personne recrutée sera responsable de la mise en place de l'infrastructure logicielle pour mener les expériences et prendre des initiatives pour les choix de logiciels et de matériel disponible, dans les limites permises par Inria.

**Principales activités**:
**Activités principales**:

- Déterminer comment entraîner (finetuning et/ou reinforcement learning), et programmer des agents sur des modèles existants et combiner ces méthodes pour remplir les missions énoncées ci-dessus.
- Mettre en place l'infrastructure pour implémenter et reproduire ces méthodes.
- Implémenter des extensions de Rocq ou Lean afin d'extraire des données pertinentes.
- Documenter les logiciels résultants.
- Collecter les résultats, exécuter des benchmarks et publier des articles scientifiques.

**Activités supplémentaires**:

- Concevoir des interfaces utilisateur pour rendre l'outil résultant plus largement utilisable.
- Déterminer un schéma de maintenance à long terme pour ceux-ci.
- Mise en place de scripts et process documentés à destination d'utilisateur-ices non spécialistes.

**Compétences**:
Compétences techniques et niveau requis:

- Connaître les bases d'au moins Lean et Rocq.
- Comprendre les différences e