超越DeepSeek推理，效率更高！斯坦福马腾宇新作：有限数据，无限迭代

原标题：超越DeepSeek推理，效率更高！斯坦福马腾宇新作：有限数据，无限迭代
文章来源：新智元
内容字数：5932字

斯坦福大学提出自博弈定理证明器STP：解决大型语言模型推理能力瓶颈

大型语言模型（LLM）的推理能力是当前自然语言处理领域的核心难题，其主要瓶颈在于缺乏高质量的训练数据。现有方法如强化学习和专家迭代，虽然能够提升模型推理能力，但存在通过率低、计算资源浪费严重等问题。斯坦福大学研究人员提出了一种名为自博弈定理证明器（STP）的新方法，有效解决了这些问题。

1. STP的核心思想：模仿数学家的学习方式

   STP模仿数学家学习和发展数学的方式，让模型同时扮演“猜想者”和“证明者”两个角色，通过互相提供训练信号，在有限的数据下实现无限自我改进。猜想者提出新的猜想，证明者尝试证明，验证器选择正确的证明用于训练，从而形成一个闭环的自我迭代过程。

2. STP的训练流程：五个步骤

   STP的训练流程包含五个步骤：1. 使用监督微调（SFT）初始化模型；2. 猜想者生成新的猜想；3. 证明者尝试证明猜想和未证明命题；4. 验证器验证证明的正确性并分配奖励；5. 基于验证结果重新训练模型。其中，奖励函数的设计是STP的核心技术难点，旨在激励猜想者生成多样化、具有挑战性但可行的猜想。

3. STP的优势：显著提升证明成功率和推理速度

   实验结果表明，STP在Lean和Isabelle验证器上的表现显著优于现有方法。在LeanWorkbook数据集上，STP的证明成功率达到26.3%，是专家迭代方法的两倍。在miniF2F-test、ProofNet-test和PutnamBench等公共基准测试中，STP也实现了最先进的性能，显著提升了推理速度。

4. STP的创新点：无限自我改进和高效利用数据

   STP的核心创新在于其自博弈机制，它能够在有限的数据集上不断生成新的猜想和证明，从而实现无限自我改进。这种机制有效解决了现有方法中数据稀缺和计算资源浪费的问题，并能够逐渐提升猜想和证明的难度。

5. STP的未来展望：推动LLM推理能力发展

   STP为解决LLM推理能力瓶颈提供了一种新的思路，其高效的数据利用方式和强大的自我改进能力，有望推动LLM在数学推理等领域的应用发展。未来的研究可以进一步探索STP在其他领域（例如，程序验证、知识图谱推理）的应用，并改进奖励函数设计，提升模型的性能和鲁棒性。

联系作者

文章来源：新智元
作者微信：
作者简介：智能+中国主平台，致力于推动中国从互联网+迈向智能+新纪元。重点关注人工智能、机器人等前沿领域发展，关注人机融合、人工智能和机器人对人类社会与文明进化的影响，领航中国新智能时代。