Haonan Li
About
I am a Senior Research Scientist at the Institute of Foundation Models (IFM), MBZUAI, where I lead a team working on LLM post-training, reasoning, agents, and inference. I am the tech lead of Jais 3 and a core contributor to IFM's K2 models, including K2 Horizon, K2-Think, K2-V2, and K2 Think V2.
My research focuses on LLM post-training (SFT and RL), reasoning and agents, AI for mathematics with Lean verification, and the evaluation and safety of LLMs, including for Arabic and Chinese.
Previously, I was a Postdoctoral Research Fellow at MBZUAI and co-founder and CTO of LibrAI, working on LLM evaluation and safety. I received my Ph.D. from the University of Melbourne, supervised by Timothy Baldwin, Martin Tomko, and Maria Vasardani.
Highlights
- Tech lead of Jais 3: six open Arabic-centric agentic models (0.9B–375B) adapted from K2 Horizon through continual pre-training, SFT, and RL; first author of the technical report (models).
- Core contributor to K2 Horizon, IFM’s fully open model fleet (0.9B–375B), working on inference and the open-weight release.
- AI for math: Magenta closes the loop between LLM reasoning and Lean 4 verification, reaching 100% on AIME 2025, AIME 2026, and HMMT Feb 2026 and solving all six IMO 2026 problems with K2-Horizon-7B; Pythagoras-Prover won the Best Paper Award at the MathNLP Workshop at EMNLP 2026.
- Co-led RL training for K2-Think and data curation for K2-V2; proposed the DALU algorithm, which enables RL training with 2× longer context and improves reasoning benchmarks such as AIME25 and LiveCodeBench by ~10%.
- Led the evaluation of Jais, an Arabic-centric open LLM, and contributed to LM Evaluation Harness.
- Built widely used benchmarks and tools, including CMMLU, Do-Not-Answer (featured in the Stanford AI Index Report 2024), Libra-Leaderboard, and Loki (1,000+ GitHub stars).
News
| Nov 2026 | We released the Jais 3 technical report, describing how we adapted the K2 Horizon fleet into Arabic-centric agentic models. |
| Oct 2026 | Pythagoras-Prover, our efficient Lean theorem prover, won the Best Paper Award at the MathNLP Workshop at EMNLP 2026. |
| Oct 2026 | We released Jais 3 (news), six open Arabic-centric agentic models (0.9B–375B) built on K2 Horizon, together with an Arabic speech recognition model and 24 Arabic benchmarks. I am the tech lead of the project. |
| Sept 2026 | We released Magenta, a training-free pipeline that pairs LLM reasoning with Lean 4 verification. It reaches 100% on AIME 2025, AIME 2026, and HMMT Feb 2026, and solves all six IMO 2026 problems with K2-Horizon-7B. |
| Sept 2026 | We released K2 Horizon, six fully open models from 0.9B to 375B parameters, with weights, code, training data, and methodology released under Apache 2.0. |
| Jan 2026 | We released K2 Think V2, a 70B reasoning system built on K2-V2 and open end to end, from pre-training data to post-training and evaluation. |
| Dec 2025 | We released K2-V2, our most capable fully open model to date, and one of the strongest open-weight models in its class. X. |
| Sept 2025 | We released K2-think, the world’s fastest open-source AI model and the most advanced open-source AI reasoning system ever created. |
Selected Publications
IFM Technical Report 2026 First author
TL;DR: Six open Arabic-centric agentic models (0.9B–375B) adapted from the fully open K2 Horizon fleet through continual pre-training, SFT, and RL.
Preprint 2026
TL;DR: A training-free agent pipeline that turns a math problem into an answer, a Lean 4 statement, and a machine-checked proof; 100% on AIME 2025/2026 and HMMT Feb 2026, and all six IMO 2026 problems with K2-Horizon-7B.
[Paper]
Technical report, 2026 · MathNLP 2026 workshop at EMNLP (non-archival) Best Paper Award
TL;DR: Compute-efficient open Lean theorem provers trained with curriculum fine-tuning and Augmented Lean Formalisation, with strong results on MiniF2F and PutnamBench.
[Paper]
Preprint 2025
TL;DR: A 32B parameter-efficient reasoning system that matches or beats much larger open models on math, code, and science reasoning.
AAAI 2026
TL;DR: LLMs do not reliably follow system-over-user instruction priority, even for simple formatting conflicts; social framings such as authority or consensus sway them more than role separation.
ICML 2025
TL;DR: Overly difficult preference examples exceed a model's capacity and hurt alignment; Selective DPO filters them out and improves alignment.
ICLR 2025
TL;DR: Represents each tool as a unique token so the LLM retrieves and calls tools by generation, scaling to tens of thousands of tools without a separate retriever.
Findings of ACL 2024 First author
TL;DR: A Chinese multitask benchmark spanning 67 subjects; at release, most LLMs struggled to reach 50% average accuracy.
Findings of EACL 2024 Co-first author
TL;DR: An open dataset of instructions that responsible LLMs should refuse, with annotated responses from six LLMs; small BERT-like classifiers rival GPT-4 as safety judges.
* Equal contribution. Full publication list →
Contact
Feel free to reach out by email about research or collaboration.