LLM2D
STP: 自我博弈LLM定理证明器与迭代猜想与证明
STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
作者: Kefan Dong, Tengyu Ma
发布日期: 2/12/2025
arXiv ID: oai:arXiv.org:2502.00212v3

摘要

arXiv:2502.00212v3 公告类型:替换-交叉 摘要:形式定理证明中使用大规模语言模型(LLM)所面临的根本挑战之一是高质量训练数据的缺乏。尽管强化学习或专家迭代部分缓解了这一问题,通过交替进行LLM生成证明和在正确生成的证明上精细调整模型,但性能很快 plateau,原因在于正确证明样品的稀少性(稀疏奖励)。为了在有限的数据下持续改进模型,我们从数学家那里汲取了灵感,数学家们通过不断提出新的猜想或练习题(这些往往是已知结果的变体)并尝试解决它们,不断开发新的结果。我们设计了自我对弈定理证明器(STP),它同时承担猜想者和证明者的角色,每个角色为另一个提供训练信号。猜想者通过迭代训练于当前证明者几乎无法证明的先前生成的猜想,这激励它随着时间的推移生成越来越具有挑战性的猜想。证明者试图使用标准的专家迭代来证明这些猜想。我们使用Lean和Isabelle形式验证器评估了STP。在Lean的训练过程中生成了198亿个令牌后,STP成功证明了LeanWorkbook数据集中26.3%的陈述,这是通过专家迭代方法实现的前最好结果13.2%的两倍。最终模型在miniF2F-test(61.7%,pass@3200)、Proofnet-test(23.1%,pass@3200)和PutnamBench(8/644,pass@3200)上达到最先进的性能。