About me

I am a PhD student at the Cambridge Computer Laboratory, supervised by Professor Mateja Jamnik. I also work closely with Yuhuai Wu and Wenda Li.

I go by Albert. You can also call me 乔楚 (Qiaochu). (They look very different, but a name is nothing more than a lambda variable)

You can find my CV here.

Research

I study how to learn abstract mathematical reasoning, with large (>20B) and small (<1B) language models.

• I worked on the autoformalization of theorems and proofs.
• I worked on integrating and improving premise selection tools with language models.
• I am working on mathematical conjecturing. A foretaste of what I want to do here.

Experiences

Between July and October 2022, I was a research scientist intern at FAIR supervised by Guillaume Lample.

News and publications

• Magnushammer: A Transformer-based Approach to Premise Selection

  arXiv

• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

  ICLR 2023 Oral

  Nov 2022 - I gave a talk in the Cambridge AI Research Group Seminar on it.

• Autoformalization with Large Language Models

  NeurIPS 2022

  Feb 2023 - The paper was featured on the Quanta Magazine.

  Dec 2022 - The paper was featured on the Cambridge Computer Laboratory website.

  June 2022 - The paper was reported by New Scientist.

• Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

  NeurIPS 2022

  Nov 2022 - I gave a talk in the Google N2Formal team on it.

• Peterhouse Graduate Studentship

  Oct 2021 - I received the prestigious studentship in science to pursue my PhD.

• Can Network Flatness Explain the Training Speed-Generalisation Connection?

  NeurIPS 2021 Bayesian Deep Learning Workshop

  Oct 2021 - My master thesis made it into a workshop!

• INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving

  ICLR 2021

  May 2021 - My first ever work on AI for Maths materialised into a paper!

• Jardine Foundation Graduate Scholarship

  Oct 2020 - I received the generous scholarship to do my Master in Computer Science at Oxford.

• Vector Institute Research Grant

  Sept 2019 - I received a grant to conduct research in Toronto with Jimmy Ba.

Contact

qj213 AT cam DOT ac DOT uk

Random meetings

If you want to talk about research or anything else, feel free to schedule a meeting: https://calendly.com/aqj. Please include your name and a meeting link if it’s virtual.

Resources for writing the PhD application research proposal

This section of Sharon Goldwater’s homepage.