Seventy3：借助NotebookLM的能力进行论文解读，专注人工智能、大模型、机器人算法方向，让大家跟着AI一起进步。

进群添加小助手微信：seventy3_podcast

备注：小宇宙

今天的主题是：STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

Summary

本文件介绍了一种名为自玩定理证明器 (STP) 的新型大型语言模型 (LLM)，它通过模拟数学家进行定理证明的方式来提升性能。STP 系统包含两个相互协作的角色：猜想生成器和证明器。猜想生成器根据现有定理及其证明提出新的相关猜想，而证明器则尝试证明这些新生成的猜想以及现有数据集中的语句。通过迭代训练，猜想生成器学习生成对当前证明器具有挑战性但又可证明的猜想，从而为证明器提供持续的训练信号。在 Lean 和 Isabelle 验证器上的实验表明，STP 在 LeanWorkbook 数据集上显著提高了定理证明通过率，并在 miniF2F-test、ProofNet-test 和 PutnamBench 等基准测试中达到了先进水平。STP 通过自给自足的猜想生成过程，克服了传统基于专家迭代方法中数据稀缺和性能瓶颈的限制，展现了在大语言模型中增强推理能力的潜力。

原文链接：https://arxiv.org/abs/2502.00212