CV

Education

PhD in Computer science - University of Cambridge, Exp. 2028
PhD on automated conjecture generation and theorem proving with AI systems.
Supervisor: Prof. Mateja Jamnik, Professor of Artificial Intelligence at the University of Cambridge.

MSc in Mathematics - Paris Cite University, 2024
Master’s degree in mathematical logic, with a thesis on automated theorem proving.
Grade: Incoming.

MSc in Mathematics - Sorbonne University, 2023
Master’s degree in machine learning, with a thesis on automated theorem proving.
Grade: First Class Honours (16.0/20).

Experience

Researcher - Project Numina, since 2024
Part of the Model and RL teams, where I build an interaction pipeline with Lean4, implement Monte Carlo tree search and train models for theorem proving in Lean4.

Research intern - University of Cambridge, 2023
Research internship on automated theorem proving with Isabelle, using Monte Carlo tree search combined with LLaMA and GPT-2.
Supervisor: Dr. Wenda Li, Research Associate at the University of Cambridge.

Research intern - OpenAI, 2022
Research internship on automated theorem proving and auto-formalisation with Lean3, using GPT-3.5 trained with expert iteration on synthetic data.
Supervisor: Stanislas Polu, Research Engineer at OpenAI.

Publications

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
Numina & Kimi Team (Core contributor)
Preprint.
📄 Paper | 🤗 Models

Llemma: An Open Language Model For Mathematics
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, Sean Welleck
ICLR 2024 (poster) and MATH-AI Workshop at NeurIPS 2023 (poster).
📄 Paper | 🤗 Model | 🤗 Dataset | Code

OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text
Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, Jimmy Ba
ICLR 2024 (poster) and MATH-AI Workshop at NeurIPS 2023 (oral & poster).
📄 Paper | 🤗 Dataset | Code

Research impact

Llemma has been cited over 300 times. It was the best open-source model in mathematics when it was released, and it has been downloaded more than 300k times on Hugging Face. The model and its training dataset have been used by:

• Mistral AI to evaluate the long context performance of their Mixtral of Experts model on the Proof-Pile-2 dataset;
• DeepSeek as a baseline to compare their DeepSeekMath model;
• The Qwen team from Alibaba Group as an inspiration to train their Qwen2.5-Math models;
• several academic researchers as a baseline and inspiration for their models (e.g., MetaMath and TinyLlama).

OpenWebMath has been cited over 70 times. It was the #1 trending dataset on Hugging Face when it was released. The dataset has been used by:

• DeepSeek to build the continued pre-training dataset for DeepSeekMath and DeepSeek-Prover models;
• Microsoft to continuously pre-train their Rho-1 model;
• The Kimi team from Moonshot AI to train their Kimi k1.5 model;
• several academic researchers to build reasoning models (e.g., Quiet-STaR by Stanford researchers).

Awards and honours

EleutherAI Scholarship, 2024
Awarded a $265k scholarship by EleutherAI to fully support my PhD on AI for mathematics.

École normale supérieure Data Challenge, 2023
1st place out of 107 participants at the École normale supérieure Data challenge organised by Inria. Invited to the awards ceremony at Collège de France to present my solution.