OpenAI 用 expert iteration 让 formal prover 在没有 ground-truth proofs 的情况下自建难度递增课程

Polu 等研究 language-model-based formal mathematics 中的 expert iteration：证明搜索与学习交替进行，模型把自己找到的 proofs 加入训练数据，并在多样化 formal statements 上逐步发现更难问题。论文显示这种自生成 curriculum 在相同 compute 下显著优于纯 proof search，并在 miniF2F 上达到当时 state of the art。