Tag: formal mathematics
All the talks with the tag "formal mathematics".
Formal Mathematics Statement Curriculum Learning
Rahul VishwakarmaPublished: at 02:00 PMIn this talk, we explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at the same compute budget, expert iteration, which means proof search interleaved with learning, dramatically outperforms proof search only. We 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.