arXiv:2502.00212v1 交叉公告类型 摘要：通过大规模语言模型（LLM）进行形式定理证明的基本挑战之一是高质量训练数据的缺乏。虽然强化学习或专家迭代在交替进行LLM生成证明和在正确生成的证明上微调时部分缓解了这一问题，但性能很快会停滞不前，原因是缺少正确证明（稀疏奖励）。为了在有限的数据下持续改进模型，我们从数学家身上汲取灵感，他们不断开发新的成果，部分通过提出新的猜想或练习题（通常是已知结果的变体），并尝试解决它们。我们设计了自我博弈定理证明器（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）上的表现达到了整体证明生成方法的最新水平。