152 citations · 235 across the 10 of their papers we have counts for
11 papers
Formal Mathematics Statement Curriculum Learning
Stanislas Polu, Jesse Michael Han, Kunhao Zheng +3
We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean pr…
Text and Code Embeddings by Contrastive Pre-Training
Arvind Neelakantan, Tao Xu, Raul Puri +22
Text embeddings are useful features in many applications such as semantic search and computing text similarity. Previous work typically trains models customized for different use c…
Unsupervised Neural Machine Translation with Generative Language Models Only
Jesse Michael Han, Igor Babuschkin, Harrison Edwards +8
We show how to derive state-of-the-art unsupervised neural machine translation systems from generatively pre-trained language models. Our method consists of three steps: few-shot a…
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, Stanislas Polu
We present miniF2F, a dataset of formal Olympiad-level mathematics problems statements intended to provide a unified cross-system benchmark for neural theorem proving. The miniF2F…
-Equivalence Relations and Associated Algorithms
Daniel Selsam, Jesse Michael Han
Lines and circles pose significant scalability challenges in synthetic geometry. A line with points implies collinearity atoms, or alternatively, when lines are…
A Formal Proof of the Independence of the Continuum Hypothesis
Jesse Michael Han, Floris van Doorn
We describe a formal proof of the independence of the continuum hypothesis () in the Lean theorem prover. We use Boolean-valued models to give forcing arguments for bo…
Proof Artifact Co-training for Theorem Proving with Language Models
Jesse Michael Han, Jason Rute, Yuhuai Wu +2
Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specia…
Universal Policies for Software-Defined MDPs
Daniel Selsam, Jesse Michael Han, Leonardo de Moura +1
We introduce a new programming paradigm called oracle-guided decision programming in which a program specifies a Markov Decision Process (MDP) and the language provides a universal…
Automatically Building Diagrams for Olympiad Geometry Problems
Ryan Krueger, Jesse Michael Han, Daniel Selsam
We present a method for automatically building diagrams for olympiad-level geometry problems and implement our approach in a new open-source software tool, the Geometry Model Build…
Enhancing SAT solvers with glue variable predictions
Jesse Michael Han
Modern SAT solvers routinely operate at scales that make it impractical to query a neural network for every branching decision. NeuroCore, proposed by Selsam and Bjorner, offered a…
A formalization of forcing and the unprovability of the continuum hypothesis
Jesse Michael Han, Floris van Doorn
We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order lo…