Création de dataset et entrainement de modèles de traduction entre outils de preuve formelle
Type de contrat : Stage
Niveau de diplôme exigé : Bac + 4 ou équivalent
Fonction : Stagiaire de l'ingénierie
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 cœur 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
Coq/Rocq et Lean sont logiciels, appelés prouveurs interactifs, 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.
Dans le cadre du projet européen (ERC) FRESCO, ce stage a pour objectif d’explorer la traduction automatique d’énoncés de preuves entre deux de ces systèmes (de Lean vers Coq) à l’aide de Large Language Models (LLM). Nous nous concentrerons plus particulièrement sur deux grandes bibliothèques : mathlib pour Lean, et Mathematical Components (ou mathcomp ) pour Coq. Ces deux bibliothèques partagent un socle théorique commun et sont guidées par des principes similaires en termes de structure et de pratiques. L’objectif du stage sera de traduire les énoncés mathématiques présents dans mathlib, mais absents de mathcomp, en veillant à maintenir la précision des notations mathématiques lors de la traduction. La traduction des scripts de preuve pourra être abordée dans une phase ultérieure.
Atouts du poste:
- stage-projet rémunéré au SMIC
- possiblité d’embauche sur CDD (2 ans) au terme du stage
Mission confiée
Bien que des datasets existent en Lean et en Coq, il n’existe pas de corpus parallèle pour la traduction entre ces deux systèmes. Le stagiaire aura pour missions :
- Évaluer les performances d’un modèle de traduction Lean -> Coq sur des énoncés de preuves mathématiques.
- Créer un dataset parallèle pour permettre le fine-tuning des LLM si nécessaire.
- Entraîner un LLM pour effectuer la traduction automatique d’énoncés de preuve de Lean vers Coq.
Le stagiaire sera encadré par une chercheuse spécialiste des prouveurs interactifs (Coq, Lean) ainsi que par un ingénieur en machine learning.
Principales activités
- Effectuer une recherche bibliographique sur l’état de l’art de la traduction automatique pour les langages disposant de peu de données.
- Construire un dataset parallèle à partir des énoncés disponibles dans mathlib et mathcomp.
- Fine-tuning et évaluation d’un modèle LLM pour la traduction d’énoncés mathématiques entre Lean et Coq.
Compétences
- Langages de programmation : Python
- Expérience avec des modèles et librairies de deep learning.
- une expérience avec un outil de preuve formelle (Coq, Lean, ) serait un atout mais n’est pas obligatoire
- Langue : Candidats maîtrisant l’anglais à un niveau B1 minimum avec une bonne compréhension du français (ou inversement).
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 œuvres sociales d'Inria)
- Accès à la formation professionnelle
- Sécurité sociale
Informations générales
- Ville : Rennes
- Centre Inria : Centre Inria de l'Université de Rennes
- Date de prise de fonction souhaitée : 2025-01-06
- Durée de contrat : 6 mois
- Date limite pour postuler : 2024-11-17
Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.
Consignes pour postuler
Sécurité défense :
Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.
Politique de recrutement :
Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.
Contacts
- Équipe Inria : SED-RBA
-
Recruteur :
Mahboubi Assia / Assia.Mahboubi@inria.fr
L'essentiel pour réussir
Se sentir à l'aise dans un environnement de dynamique scientifique, aimer apprendre et écouter sont des qualités essentielles pour réussir cette mission.
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'efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.