LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
作者: Suozhi Huang, Peiyang Song, Robert Joseph George, Anima Anandkumar
发布时间: 2025-02-27
来源: arxiv
研究方向: 自动化定理证明与形式化验证
主要内容
本文提出了LeanProgress，一种通过预测证明进度来指导神经网络定理证明的方法。该方法结合了Large Language Models (LLMs) 和Lean证明助手，旨在解决LLMs在长证明和复杂数学形式化中的困难。LeanProgress通过预测证明的剩余步骤，提供了全局的证明进度视图，从而提高了自动化定理证明的效率。
主要贡献
1. 提出了LeanProgress框架，通过预测证明的剩余步骤来指导证明搜索。
2. 构建了一个平衡的数据集，包含约80k条Lean证明轨迹，并通过数据平衡策略处理了证明长度的偏斜分布。
3. 微调了DeepSeek Coder V1 1.3b模型，用于预测剩余步骤，并在测试集上达到了75.1%的预测准确率。
4. 将步骤预测模型集成到best-first search框架中，显著提高了Mathlib4上的证明通过率。
5. 开发了与LeanCopilot集成的工具，提供了用户友好的证明进度反馈和战术建议。
研究方法
1. 使用best-first search (BFS) 和Reprover模型生成证明树和轨迹。
2. 通过数据平衡策略调整证明长度的分布，确保数据集的代表性。
3. 微调DeepSeek Coder模型，使用Mean Squared Error (MSE) 损失函数进行训练。
4. 将步骤预测模型与log probabilities结合，用于best-first search框架中的状态扩展。
5. 开发了predict steps with suggestion工具，集成到LeanCopilot中，提供战术建议和证明进度反馈。
实验结果
实验结果表明，LeanProgress在预测剩余步骤的准确率上达到了75.1%，并且在Mathlib4数据集上，与仅使用log probabilities的baseline相比，证明通过率提高了3.8%。特别是在长证明中，LeanProgress表现出了显著的改进。
未来工作
未来的研究方向包括：1) 将Tree-of-Thought (ToT) 和Chain-of-Thought (CoT) 方法集成到LeanProgress中，以提供更结构化的推理方式；2) 将LeanProgress与Reinforcement Learning (RL) 技术结合，利用连续奖励信号改进证明搜索；3) 开发更轻量级的实现，降低计算资源需求，使其更易于集成到现有的定理证明工作流中。