Advanced Research Position – Intelligence artificielle pour les mathématiques formelles : qualité, évaluation et traduction des preuves générées par les modèles de langage

Lead the language-model research strand of the BELLE project in the ARGO team. Work covers evaluation and improvement of AI-generated formal proofs, expert preference datasets, Lean/Mathlib code quality, reinforcement learning and translation between proof assistants. Responsibilities include research leadership, supervision and reproducible open-source training and evaluation. The renewable appointment is initially 12 months, with a planned start of 1 December 2026.

Relevant doctorate and established machine-learning research experience; expertise in LLM training and evaluation, Python and GPU workflows, strong mathematics and supervision skills. Scientific English at C1 level and ability to work in French are requested. Restricted-area authorization may apply.