Joshua Ong

PhD Student @ Imperial College London.

prof_pic.jpg

I am a first-year PhD student at Imperial College London, fortunate to be advised by Eleonora Giunchiglia, Shay Cohen and Wenda Li, and am currently a visiting researcher at the Institute of Foundation Models, part of the Mohamed bin Zayed University of Artificial Intelligence (MBZUAI). Prior to joining Imperial College London, I was a visiting researcher at the University of Edinburgh, where I also obtained my BSc in Mathematics and Statistics.

My research focuses on Large Language Model (LLM) Reasoning and theorem proving, with a particular interest in understanding and improving the mathematical reasoning capabilities of LLMs. Currently, my interests lie in generating verifiable synthetic data for LLMs [1], and training reasoning models for both formal and informal mathematics [2]. I am also part of the AI for Math Grant, where our main focus lies in advancing theorem proving autoformalisation within LLMs.

PhD and Masterโ€™s applications and stepping into research can be overwhelming. As such, Iโ€™d love to dedicate time to helping anyone who wants to chat or seek advice about the process. Feel free to reach out if youโ€™d like to discuss research, explore collaboration opportunities, or just talk through your questions, Iโ€™m more than happy to help!

I am actively looking for internship opportunities for 2027. Feel free to reach out to me if there are any interesting or suitable positions!

news

Sep 25, 2026 SCOPE: Self-Play via Co-Evolving Policies for Open-Ended Tasks has been accepted at NeurIPS 2026.
Sep 11, 2026 ๐Ÿš€๐Ÿš€๐Ÿš€ We are pleased to release Magenta, an end-to-end formal-informal self-correction pipeline that achieves 100% mathematical benchmarks, marking the first time a fully open-source model has achieved a perfect score. In addition, when using a 7B model for informal reasoning, the pipeline achieved a perfect score on IMO 2026, making it the smallest model to date to do so. For more details, please see our recent work, Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification๐Ÿ”ฅ.
Jun 12, 2026 ๐Ÿš€๐Ÿš€๐Ÿš€ We are pleased to release Pythagoras-Prover, a family of theorem-proving models (4B and 32B). It includes the smallest model to date for theorem proving (4B), as well as the first diffusion-based model capable of theorem proving. For more details, please see our recent work, Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation๐Ÿ”ฅ.
Jun 01, 2026 I will be attending ICML 2026 in Seoul ๐Ÿ‡ฐ๐Ÿ‡ท. Feel free to reach out if youโ€™d like to meet or discuss interesting topics!
May 01, 2026 Can I Have Your Order? Monte-Carlo Tree Search for Slot Filling Ordering in Diffusion Language Models has been accepted at ICML 2026.
Apr 07, 2026 PiCSAR: Probabilistic Confidence Selection And Ranking for Reasoning Chains has been accepted at ACL 2026 (Findings).
Feb 16, 2026 Do check out our recent work on Can I Have Your Order? Monte-Carlo Tree Search for Slot Filling Ordering in Diffusion Language Models๐Ÿ”ฅ
Feb 01, 2026 I am excited to announce that I will be joining MBZUAI as a visiting student, working on Theorem Proving with LLMs. Feel free to reach out if you are interested in discussing potential collaborations!
Jan 26, 2026 Neural Theorem Proving For Verification Conditions: A Real-World Benchmark has been accepted at ICLR 2026 (Poster).
Oct 25, 2025 I will be going to EMNLP 2025 in Suzhou, China. Feel free to reach out if youโ€™d like to meet or discuss interesting topics!