STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

大型语言模型（LLMs）在形式化定理证明中的一个基本挑战是缺乏高质量的训练数据。尽管强化学习或专家迭代通过交替进行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）的完整证明生成方法中达到了最先进的性能。

该论文试图解决大型语言模型（LLM）在形式定理证明中因缺乏高质量训练数据而导致性能快速饱和的问题。这是一个现有问题，但通过引入新的自我训练机制来改善。

关键思路是设计了一个名为Self-play Theorem Prover (STP)的系统，其中包含两个角色：猜想者和证明者。猜想者生成新的猜想，而证明者尝试证明这些猜想，两者相互提供训练信号，从而实现迭代改进。这与传统方法不同，因为它模仿了数学家的工作方式，即通过提出新问题并尝试解决它们来推动进步。

实验表明，在Lean环境中使用198亿个生成标记后，STP能够证明LeanWorkbook数据集中26.3%的陈述，几乎是之前最佳结果（13.2%）的两倍。此外，它还在miniF2F-test、Proofnet-test和PutnamBench等基准测试中取得了最先进的成绩。论文使用了Lean和Isabelle两种形式验证器进行评估，并且提供了开源代码以供进一步研究。

最近的相关研究包括利用强化学习或专家迭代来增强LLM的定理证明能力。例如，《Reinforcement Learning for Theorem Proving》探讨了如何通过强化学习提升自动定理证明的效果；《Expert Iteration in Probabilistic Logic Models》则研究了专家迭代在概率逻辑模型中的应用。