MA-LoT：基于模型协作的 Lean 长链式思维推理增强形式化定理证明
计算与语言
2025-05-28 v3 人工智能
摘要
使用 Lean 等计算机可验证语言求解数学问题，对数学和计算机科学界产生了深远影响。最先进的方法利用单一大型语言模型（LLM）生成完整证明或执行树搜索，但无法在这两项任务之间取得平衡。我们提出 **MA-LoT**：*Model-CollAboration Lean-based Long Chain-of-Thought*，一个用于 Lean4 定理证明的综合性框架，以解决此问题。它通过模型协作方法，将通用自然语言的全证明生成认知任务与证明修正的错误分析认知任务分离。我们通过 LLM 与 Lean4 验证器在长链式思维中的结构化交互来实现这一点。为实现该框架，我们提出了新颖的 *LoT-Transfer Learning* 训练-推理流水线，使 LLM 无需特殊数据标注即可具备长链式思维能力。大量实验表明，我们的框架在 Lean4 版 MiniF2F-Test 数据集上达到了 **61.07%** 的准确率，大幅优于 DeepSeek-V3（33.61%）、单模型树搜索（InternLM-Step-Prover，50.70%）和全证明生成（Godel-Prover，55.33%）等基线方法。此外，我们的研究结果揭示了将长链式思维与形式化验证相结合，以在更广阔的视角下实现更具洞察力的生成的潜力。
引用
@article{arxiv.2503.03205,
title = {MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving},
author = {Ruida Wang and Rui Pan and Yuxin Li and Jipeng Zhang and Yizhen Jia and Shizhe Diao and Renjie Pi and Junjie Hu and Tong Zhang},
journal= {arXiv preprint arXiv:2503.03205},
year = {2025}
}