Curriculum Learning

• Formal Mathematics Statement Curriculum Learning
• neural theorem prover using GPT-f
• solve a curriculum of increasingly difficult problems out of a set of formal statements of sufficiently varied difficulty
• high-school Math Olympiad problems
• language model to find proofs of formal statements
• formal mathematics
• at same compute budget, expert iteration, by which they mean proof search interleaved with learning, dramatically outperforms proof search only
• expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs
• miniF2F
• automatically solving multiple challenging problems drawn from high school olympiads
• lack of self-play in the formal mathematics setup can be effectively compensated for by automatically as well as manually curated sets of formal statement
• cheaper to formalize than full proofs