arXiv:2502.00212v2 宣告类型：交叉 摘要：形式定理证明中通过大型语言模型（LLM）所面临的一个基本挑战是在高质量训练数据方面存在不足。尽管强化学习或专家迭代部分缓解了这一问题，通过对LLM生成证明和在正确生成的证明上进行微调交替进行，但由于正确的证明（稀疏奖励）稀缺，性能很快就会达到 Plateau。为了在有限的数据下继续改进模型，我们从数学家获得启发，数学家们通过提出新的猜想或练习题（这些往往是已知结果的变体）并尝试解决它们，不断开发新的成果。我们设计了Self-play Theorem Prover（STP），该系统同时承担着猜想作家和证明者两个角色，各自为对方提供训练信号。猜想作家通过迭代训练，对那些当前证明者勉强能够证明的先前生成的猜想进行训练，这激励它随着时间推移生成越来越具有挑战性的猜想。证明者尝试使用标准专家迭代来证明猜想。我们使用Lean和Isabelle的形式验证器来评估STP。在Lean的训练过程中生成了198亿个令牌后，STP在LeanWorkbook数据集中证明了26.3%的陈述，这一成果是通过专家迭代之前的最佳结果13.2%的两倍。最终模型在miniF2F-test（61.1%，pass@3200）、Proofnet-test（23.1%，pass@3200）和PutnamBench（8/644，pass@64）上的性能达到了同类方法中的最佳水平。