arXiv 2503.032052025-05-27cs.CLcs.AI

MA-LoT：基于模型协作的Lean长思维链推理增强形式化定理证明

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

NVIDIA（英伟达）；University of Wisconsin-Madison（威斯康星大学麦迪逊分校）

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

阅读 PDF

arXiv 页面 ↗HTML 原文 ↗

AI总结：

提出MA-LoT框架，通过模型协作分离整体证明生成与错误分析任务，结合长思维链与Lean4验证器交互，并引入LoT-迁移学习流水线，在MiniF2F-Test上取得61.07%准确率，超越多个基线。

摘要：

使用Lean等计算机可验证语言解决数学问题，对数学和计算机科学界产生了重大影响。现有最先进的方法利用单一大型语言模型（LLM）生成完整证明或执行树搜索，但无法平衡这两项任务。我们提出**MA-LoT**：*基于模型协作的Lean长思维链*，这是一个面向Lean4定理证明的综合性框架，以解决该问题。它通过模型协作方法，将针对整体证明生成的通用自然语言认知任务与针对证明纠错的错误分析任务分离开来。我们通过在长思维链中实现LLM与Lean4验证器的结构化交互来达成这一目标。为实施该框架，我们提出了新颖的*LoT-迁移学习*训练-推理流水线，使LLM无需特殊数据标注即可获得长思维链思考能力。大量实验表明，我们的框架在MiniF2F-Test数据集的Lean4版本上达到了**61.07%**的准确率，大幅超越了DeepSeek-V3（33.61%）、单模型树搜索（InternLM-Step-Prover，50.70%）以及整体证明生成（Godel-Prover，55.33%）等基线方法。此外，我们的研究结果凸显了将长思维链与形式化验证相结合，以在更广阔视角下实现更具洞察力生成的潜力。

英文摘要：

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.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。