Research

I am broadly interested in formal proofs and building artificially intelligent theorem provers.

In joint work with Jason Rute, Yuhuai Wu, Ed Ayers, and Stanislas Polu, I developed PACT, a methodology for extracting abundant self-supervised data from kernel-level proof artifacts. We apply this to Lean and show that co-training large Transformer language models on these data significantly boosts theorem proving performance.

With Daniel Selsam, Leonardo de Moura, and Patrice Godefroid, I recently helped develop a new programming paradigm called oracle-guided decision programming, including a Scheme dialect with a primitive for non-deterministic choice whose interpreter queries a neural oracle.

I have worked on using graph neural networks to accelerate SAT solvers, with improvements to state-of-the-art CDCL solvers (paper, code) and the cube-and-conquer paradigm (paper, code).

With Floris van Doorn, I completed the Flypitch project, producing a formal proof of the independence of the continuum hypothesis in Lean.

Papers and preprints

• Unsupervised neural machine translation with generative language models only. Joint with Igor Babuschkin, Harrison Edwards, Arvind Neelakantan, Tao Xu, Stanislas Polu, Alex Ray, Pranav Shyam, Aditya Ramesh, Alec Radford, and Ilya Sutskever.

• MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. Joint with Kunhao Zheng and Stanislas Polu.

• Contrastive finetuning of generative language models for informal premise selection. Joint with Tao Xu, Stanislas Polu, Arvind Neelakantan, and Alec Radford. Accepted to AITP 2021.

• Proof artifact co-training for theorem proving with language models. Joint with Jason Rute, Yuhuai Wu, Ed Ayers, and Stanislas Polu.

• Universal policies for software-defined MDPs. Joint with Daniel Selsam, Leonardo de Moura, and Patrice Godefroid.

• Automatically building diagrams for Olympiad geometry problems. Joint with Ryan Krueger and Daniel Selsam.

• Enhancing SAT solvers with glue variable predictions.

• Learning cubing heuristics for SAT from DRAT proofs. Accepted to AITP 2020.

• A formal proof of the independence of the continuum hypothesis. Joint with Floris van Doorn. Accepted to CPP 2020.

• A formalization of forcing and the unprovability of the continuum hypothesis. Joint with Floris van Doorn. Accepted to ITP 2019.

• Reconstruction problems for first-order theories (master’s thesis)

Talks and conferences

• A formal proof of the independence of the continuum hypothesis. (Talk at CPP 2020).

• A formal proof of the independence of the continuum hypothesis. (Talk at Lean Together 2020).

• A formalization of forcing and the unprovability of the continuum hypothesis. (Talk at ITP 2019).

• I co-organized the Hanoi Lean 2019 workshop. Exercises and slides are available here.

• Strong conceptual completeness for ℵ₀-categorical theories (notes for Feb. 2018 talk at Harvard Logic seminar)

• Strong conceptual completeness for Boolean coherent toposes (slides for talks given at McGill, CMU, CUNY, UMCP)

• Ultraproduct definability criteria for ω-categorical theories (poster for 2017 model theory meetings in Wrocław and Będlewo)

• Model-theoretic Galois theory (slides for an expository talk at the 2016 GSCL at Notre Dame)

Notes

• An introduction to abelian sheaf cohomology

• Theories, interpretations, and pretoposes (an introduction to first-order categorical logic, meant as a revised version of Chapter 1 of my master’s thesis)

• Automorphic forms and the Langland’s program (notes I helped write on Kevin Buzzard’s 2017 course at the MSRI)

• Definable categories (research from 2016 on internal covers and categories internal to Def (T), including a general adjoint functor for internal anafunctors)