MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving

📄 arXiv: 2503.03205v3 📥 PDF

作者: Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu, Tong Zhang

分类: cs.CL, cs.AI

发布日期: 2025-03-05 (更新: 2025-05-27)

💡 一句话要点

MA-LoT：模型协作的长链式思考提升Lean形式化定理证明

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化定理证明 Lean4 长链式思考 模型协作 大型语言模型 迁移学习 错误分析

📋 核心要点

  1. 现有方法依赖单一LLM生成完整证明或进行树搜索，无法有效平衡证明生成和错误分析任务。
  2. MA-LoT框架通过模型协作分离认知任务，利用长链式思考实现LLM与Lean4验证器的结构化交互。
  3. 实验表明，MA-LoT在Lean4 MiniF2F-Test数据集上显著优于现有方法，准确率达到61.07%。

📝 摘要（中文）

本研究针对使用Lean等计算机可验证语言解决数学问题的方法，提出了一种名为MA-LoT（Model-CollAboration Lean-based Long Chain-of-Thought）的框架，用于Lean4定理证明。该框架通过模型协作方法分离了通用自然语言的认知任务（用于生成完整证明）和错误分析任务（用于证明修正），从而平衡了这些任务。通过LLM和Lean4验证器在长链式思考（Long CoT）中的结构化交互来实现。此外，提出了LoT-Transfer Learning训练-推理流程，使LLM具备长链式思考能力，而无需特殊的数据标注。实验结果表明，该框架在MiniF2F-Test数据集的Lean4版本上达到了61.07%的准确率，显著优于DeepSeek-V3 (33.61%)、单模型树搜索(InternLM-Step-Prover, 50.70%)和完整证明生成(Godel-Prover, 55.33%)等基线方法。研究结果表明，将长链式思考与形式化验证相结合，有望在更广泛的视角下实现更具洞察力的生成。

🔬 方法详解

问题定义：现有方法在形式化定理证明中，依赖单个大型语言模型（LLM）完成所有任务，包括生成完整证明和进行错误分析。这种方式难以平衡两个任务的需求，导致性能瓶颈。尤其是在复杂的数学问题中，需要更精细的推理和验证过程。

核心思路：MA-LoT的核心在于将证明过程分解为两个不同的认知任务：一是利用LLM进行通用自然语言的推理，生成完整的证明草案；二是利用LLM进行错误分析，根据Lean4验证器的反馈修正证明。通过模型协作，使不同的模型专注于不同的任务，从而提高整体性能。

技术框架：MA-LoT框架包含以下几个主要模块：1) 证明生成模块：利用LLM生成初始的Lean4证明代码。2) Lean4验证模块：使用Lean4验证器对生成的证明代码进行验证，并返回错误信息。3) 错误分析模块：利用LLM分析Lean4验证器返回的错误信息，并提出修正建议。4) 证明修正模块：根据错误分析模块的建议，对证明代码进行修正。5) 长链式思考（Long CoT）模块：通过多次迭代上述过程，逐步完善证明。

关键创新：该论文的关键创新在于提出了模型协作的框架，将证明生成和错误分析任务分离，并利用长链式思考进行迭代优化。此外，还提出了LoT-Transfer Learning训练-推理流程，使LLM具备长链式思考能力，而无需特殊的数据标注。

关键设计：LoT-Transfer Learning训练-推理流程是关键设计之一。该流程利用已有的数据进行预训练，然后通过少量数据进行微调，使LLM具备长链式思考能力。此外，在错误分析模块中，使用了特定的提示工程（Prompt Engineering）技术，引导LLM更准确地分析错误信息并提出修正建议。具体的参数设置和损失函数等技术细节在论文中未详细说明，属于未知信息。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

MA-LoT框架在Lean4版本的MiniF2F-Test数据集上取得了显著的性能提升，准确率达到61.07%，大幅超过了DeepSeek-V3 (33.61%)、单模型树搜索(InternLM-Step-Prover, 50.70%)和完整证明生成(Godel-Prover, 55.33%)等基线方法。这表明模型协作和长链式思考能够有效提升形式化定理证明的性能。

🎯 应用场景

MA-LoT框架可应用于形式化定理证明、程序验证、智能合约安全审计等领域。通过结合LLM的推理能力和形式化验证的严谨性，可以提高软件系统的可靠性和安全性，并加速数学研究的进程。未来，该框架有望扩展到更广泛的逻辑推理和知识发现领域。

📄 摘要（原文）

Solving mathematical problems using computer-verifiable languages like Lean has significantly impacted the mathematical and computer science communities. State-of-the-art methods utilize a single Large Language Model (LLM) to generate complete proof or perform tree search, but they fail to balance these tasks. We propose MA-LoT: Model-CollAboration Lean-based Long Chain-of-Thought, a comprehensive framework for Lean4 theorem proving to solve this issue. It separates the cognition tasks of general NL for whole-proof generation and error analysis for proof correction using the model-collaboration method. We achieve this by structured interaction of the LLM and Lean4 verifier in Long CoT. To implement the framework, we propose the novel LoT-Transfer Learning training-inference pipeline, which enables the Long CoT thinking capability to LLMs without special data annotation. Extensive experiment shows that our framework achieves a 61.07% accuracy rate on the Lean4 version of the MiniF2F-Test dataset, largely outperforming DeepSeek-V3 (33.61%), single-model tree search (InternLM-Step-Prover, 50.70%), and whole-proof generation (Godel-Prover, 55.33%) baselines. Furthermore, our findings highlight the potential of combining Long CoT with formal verification for a more insightful generation in a broader perspective.