152 citations · 204 across the 8 of their papers we have counts for
9 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…
-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…
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…