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