This paper explores the use of expert iteration in the context of language modeling applied to formal mathematics. And show that at same compute budget, expert iteration, which mean proof search interleaved with learning, dramatically outperforms proof search only. Authors also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs.
Additional resources: https://arxiv.org/abs/2202.01344
No slides are available for this talk.