My work is featured in Quanta Magazine!

Two oral awards at ICLR2023.

Releasing Draft, Sketch, and Prove: Autoformalize the entire natural language proofs [arxiv]!

I gave a talk on autoformalization at FLAIM conference.

I gave a guest lecture on autoformalization at UIUC proof automation class.

8 papers accepted to NeurIPS 2022.

We are organizing the second MATHAI workshop at NeurIPS 2022.

I gave a talk at AITP 2022.

Releasing Minerva: a language model that solves MATH with 51% acc, which was predicted to happen in 2025! See [arXiv][Google AI Blog][Sample Explorer].

Sharing a systematic study on synthetic pre-training [arXiv]. Understanding pre-training via synthetic tasks!

I gave a talk at the University of Cambridge [Link].

I gave a talk at UC Berkeley Center for Human-Compatible AI (CHAI).

I gave a talk at Covariant.ai.

We used LLMs to turn natural language mathematics into formal specifications [arXiv], and achieved SOTA on miniF2F. See media coverage on NewScientist!

We released Thor [arXiv]. Integrate symbolic tools to neural theorem provers for premise selection!

We released a stronger version of Subgoal search. Introduce Adaptive Subgoal Search (AdaSubS) [arXiv]: improve search with transformers by variable planning horizons.

We released STaR [arXiv]. Bootstrapping Reasoning with Reasoning!

We released Block-Recurrent Transformer [arXiv]. Recurrence is coming back!

Gave a talk at the University of Oxford.

Gave a talk at Harvard University.

Three papers accepted to ICLR 2022.

Subgoal search algorithm accepted to NeurIPS 2021.

Co-organized the MATHAI4ED workshop at NeurIPS 2021: Math AI for education: Bridging the gap between research and smart education.

Led the Reasoning section in the Foundation Model white paper.

Two posters in ICML 2021.

Co-organized the first MATH-AI workshop at ICLR 2021: On The Role of Mathematical Reasoning in General Artificial Intelligence.

INT accepted to ICLR 2021: An Inequality Benchmark for Evaluating Generalization in Theorem Proving!

IsarStep accepted to ICLR 2021: A Benchmark for High-level Mathematical Reasoning!

Neuro# accepted to AAAI 2021: A neural network #SAT solver that generalizes to problems of much larger sizes, achiving improvements over SOTA by orders of magnitude.

Releasing LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning!

Releasing SCL: a neural architecture that discovers compositional structures in analogical reasoning, generalizing to novel analogies.

One poster in ICML 2020.

AlphaStar published in Nature Cover!

Released OPRE: a hierarchical agent that generalizes to novel opponent strategy.

Organized a seminar on Machine Reasoning, including reasoning in theorem proving, natural language understanding, program synthesis: [paper list]. The meeting time is every Wednesday 3-4pm EST, Vector Institute. Welcome to attend if you're around Toronto.

Finished an internship at Deepmind from June 2018 - April 2019, working on hierarchical reinforcement learning and StarCraft 2.

One poster in NeurIPS 2018.

Two posters in ICLR 2018.

Two posters and two workshops in NIPS 2017.

Released ACKTR: a far more sample-efficient reinforcement learning algorithm than TRPO and A2C! [code]. This is also covered by [OpenAI Blog].

I'm very honoured to receive the Google PhD fellowship in machine learning!

One journal paper accepted to appear in Neural Computation.

3 co-first-authored papers accepted to appear at NIPS 2016.

Our submission to ICLR: On the Quantitative Analysis of Decoder-Based Generative Models [arxiv] was accepted as a poster presentation. Now we are able to quantitatively measure performances of GANs.