Création d'Outils Interactifs pour le Développement de Preuves Formelles en Rocq et Interfaçage avec des Llms H/F - INRIA

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.

Création d'outils interactifs pour le développement de preuves formelles en Rocq, et interfaçage avec des LLMs

Type de contrat : CDD

Niveau de diplôme exigé : Bac +5 ou équivalent

Fonction : Ingénieur scientifique contractuel

A propos du centre ou de la direction fonctionnelle

Le centre Inria de l'Université de Rennes est un des neuf 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

estlogiciel, appelé prouveur interactif, conçus pour écrire et valider des preuves de propriétés mathématiques grâce à une interaction entre utilisateurices et machine. Par exemple, ils sont utilisés dans le monde académique ainsi que dans l'industrie pour prouver la correction de programmes critiques et sophistiqués dans des domaines variés (cybersécurité, compilation, architecture, etc.). L'une des forces de ce type de méthodes formelles est son expressivité, qui permet en fait de formaliser et de vérifier des théories mathématiques arbitrairement sophistiquées. De fait, ces prouveurs interactifs sont aussi utilisés par des chercheurs en mathématiques aussi bien que par des chercheurs en méthodes formelles.

Un des grands défi de ce domaine est de démocratiser la production des bibliothèques de code de ces prouveurs, et de leur concevoir un environnement de développement moderne et productif. Le contexte général de ce poste est d'explorer comment exploiter les récentes capacités des LLMs généraliste à générer des preuves formelles en Rocq avec un accent mis sur les interfaces utilisateur.

Dans le cadre du défi FRAIME avec MERCE (Mitsubishi Electric R&D Centre Europe), la mission de ce poste est plus particulièrement de mettre en place une interface entre Rocq, VSCode et des LLMs généralistes pour obtenir un environnement de développement unifié et efficace pour l'utilisateur.

Mission confiée

La personne recrutée aura pour missions :

- De reprendre les propositions d'interface utilisateur basées sur VSCode (Rocqlsp et VSRocq) et de fournir une version robuste et unifiée.
- De fournir une interface MCP (Model Context Protocol) pour permettre l'interfaçage avec des LLMs.
- De faire un travail de veillle et de réponse à la communauté d'utilisateur qui cherche à utiliser les outils proposés.

L'ingénieur sera encadré pardes chercheurs spécialistes des prouveurs interactifs (Rocq et Lean). Les expérimentations seront menées en collaboration avec une équipe élargie de chercheurs Inria travaillant sur la question des interfaces utilisateurs et l'intégration d'outils de machine learning.

Principales activités

- Mise en place d'un serveur permettant l'éxecution parallèle et stable de plusieurs processus `rocq`. Ceci avec pour but à la fois l'utilisation multi-agentique avec des LLMs, mais aussi permettre une meilleure stabilité pour les interfaces utilisateurs en ayant toujours un processus pouvant prendre le relai en cas de problème.
- intégration de ce nouveau seveur avec une extension Rocq pour VS code et éventuellement d'autres plateformes
- mise en place d'une veille sur les retours utilisateurs pour atteindre une facilité d'installation et d'utilisation qui reste pour le moment encore insuffisante.

Compétences

- Langages de programmation :OCaml
- Expérience avec un outil de preuve formelle (Rocq, Lean ou Agda).
- Langue : Candidats maîtrisant l'anglais à un niveau B1 minimum avec une bonne compréhension du français (ou inversement).
- Travail en équipe en distanciel
- Une expérience avec les protocoles LSP et MCP serait un atout mais n'est pas obligatoire.

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

Selon expériences