[h/f] ingénieur de recherche - développement d’une nouvelle génération d’assistants à la preuve

Informations générales

Intitulé de l'offre : [H/F] ingénieur de recherche - développement d’une nouvelle génération d’assistants à la preuve
Référence : UMR8243-JEMSAM0-016
Nombre de Postes : 1
Lieu de travail : PARIS 13
Date de publication : vendredi 28 mars 2025
Type de contrat : IT en contrat CDD
Durée du contrat : 36 mois
Date d'embauche prévue : 1 juin 2025
Quotité de travail : Complet
Rémunération : à partir de 3557 € brut et plus selon experience
Niveau d'études souhaité : Doctorat
Expérience souhaitée : Plus de 10 années
BAP : E - Informatique, Statistiques et Calcul scientifique
Emploi type : Chef-fe de projet ou expert-e en Ingéniérie logicielle

Missions

Le projet a pour objectif de participer au développement d’une nouvelle génération d’assistants à la preuve, qui intègrent dans leurs noyaux une couche linguistique et des outils d'assistance automatisée pour guider le scientifique et faciliter la construction de documents mathématiques certifiés, depuis le choix des concepts et des définitions, jusqu’à l'élaboration des théorèmes et des démonstrations.

Activités

• Conception, implémentation et expérimentation d’une couche linguistique dans un assistant à la preuve,
• Développement d’outils d’extraction de paramètres (feature extraction) de larges corpus de mathématiques formalisées
• Gestion incrémentale de ces larges corpus de mathématiques formalisées
• Développement d'un environnement de type Gym pour permettre à l’IA d’interagir avec l’assistant à la preuve
• Intégration d'un éditeur de code et d’une interface graphique pour permettre à un utilisateur humain d’interagir avec l’assistant à la preuve et l’IA

Compétences

• Expert en programmation OCaml et Python
• Bonne connaissance d’un assistant de preuve tel que Agda, Isabelle, Lean ou Rocq sur les aspects formalisation et implémentation interne
• Expérience de développement d’interface utilisateur, notamment avec les éditeurs de code moderne tels que VSCode et Jupyter
• Bonne connaissance de l’apprentissage machine, idéalement appliqué à la preuve formelle
• Bonne connaissance des systèmes de build de OCaml et Rocq
• Maîtrise de la gestion de gros corpus de données

• Anglais : B2 (Cadre européen de référence)
• Capacité de conceptualisation
• Sens critique
• Sens de l'organisation
• Aptitude au travail en équipe

Contexte de travail

Travail au sein de l'unité mixte de recherche 8243 IRIF

Contraintes et risques

Pas de risque