152 citations · 235 across the 10 of their papers we have counts for
5 papers · 1 filter
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…