Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving

📄 arXiv: 2506.17104v1 📥 PDF

作者: Chuxue Cao, Mengze Li, Juntao Dai, Jinluan Yang, Zijian Zhao, Shengyu Zhang, Weijie Shi, Chengzhong Liu, Sirui Han, Yike Guo

分类: cs.AI, cs.CL, cs.LO

发布日期: 2025-06-20

💡 一句话要点

提出DREAM以解决LLMs在复杂数学推理中的不足问题

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

关键词: 大型语言模型 一阶逻辑 数学推理 定理证明 自适应机制 策略多样化 错误反馈 深度学习

📋 核心要点

  1. 现有大型语言模型在复杂数学推理中表现不佳，尤其是在多步FOL推导任务上准确率低。
  2. 本文提出DREAM，通过自适应机制增强LLMs的推理策略多样性和合理性，解决早期推理错误的问题。
  3. 实验结果表明，DREAM在数学推理任务上性能提升了0.6%至6.4%，并提供了447个定理的数据集用于评估。

📝 摘要（中文）

大型语言模型（LLMs）在一阶逻辑（FOL）推理方面展现出良好的能力，但在涉及多步FOL推导的复杂数学推理中仍然存在不足。尽管LLMs在已有的数学推理基准上表现良好，但在多步FOL任务中却面临挑战，Deepseek-Prover-V2-7B在我们提出的定理证明数据集上的准确率仅为4.2%。为了解决这些问题，本文提出了DREAM，一个自适应解决方案，旨在增强LLMs生成策略的多样性和合理性。DREAM结合了公理驱动的策略多样化机制和子命题错误反馈，帮助LLMs反思和纠正其证明。我们的贡献包括在FOL定理证明中推动LLMs数学推理的前沿，提出了一种新颖的推理阶段解决方案，使性能提升了0.6%至6.4%，并提供了447个数学定理的Lean 4格式数据集以供评估。

🔬 方法详解

问题定义：本文旨在解决大型语言模型在复杂数学推理中，尤其是多步FOL推导任务中的低准确率问题。现有方法在多样化证明策略和早期推理错误的反馈机制上存在不足。

核心思路：DREAM通过引入公理驱动的策略多样化机制和子命题错误反馈，增强LLMs的推理能力，促进多样化的推理结果，并帮助模型反思和纠正错误。

技术框架：DREAM的整体架构包括两个主要模块：策略多样化模块和错误反馈模块。策略多样化模块通过不同的推理策略生成多样的证明路径，而错误反馈模块则对模型的推理过程进行监控和调整。

关键创新：DREAM的核心创新在于其自适应机制，能够根据推理过程中的反馈动态调整生成策略。这一设计与现有方法的静态策略生成形成鲜明对比，显著提升了模型的推理能力。

关键设计：DREAM在参数设置上采用了动态调整机制，损失函数设计上考虑了推理过程中的反馈信息，并在网络结构上引入了多样化策略生成的模块，以支持复杂的推理任务。

📊 实验亮点

实验结果显示，DREAM在数学推理任务中的性能提升显著，准确率提高了0.6%至6.4%。与基线模型Deepseek-Prover-V2-7B相比，DREAM展现出更强的推理能力，尤其是在多步FOL任务上，验证了其有效性。

🎯 应用场景

该研究的潜在应用领域包括数学教育、自动定理证明、智能辅导系统等。通过提升LLMs在复杂数学推理中的表现，DREAM能够为教育和科研提供更强大的工具，推动智能化学习和研究的进步。未来，DREAM的技术框架也可能扩展到其他领域的推理任务中，具有广泛的应用价值。

📄 摘要（原文）

Large language models (LLMs) have shown promising first-order logic (FOL) reasoning capabilities with applications in various areas. However, their effectiveness in complex mathematical reasoning involving multi-step FOL deductions is still under-researched. While LLMs perform competitively on established mathematical reasoning benchmarks, they struggle with multi-step FOL tasks, as demonstrated by Deepseek-Prover-V2-7B's low accuracy (4.2%) on our proposed theorem proving dataset. This issue arises from the limited exploration of diverse proof strategies and the potential for early reasoning mistakes to undermine entire proofs. To address these issues, we propose DREAM, a self-adaptive solution that enhances the Diversity and REAsonability of LLMs' generation strategies. DREAM incorporates an Axiom-Driven Strategy Diversification mechanism to promote varied strategic outcomes and a Sub-Proposition Error Feedback to help LLMs reflect on and correct their proofs. Our contributions include pioneering advancements in LLMs' mathematical reasoning through FOL theorem proving, introducing a novel inference stage solution that improves performance by 0.6% to 6.4%, and providing a curated dataset of 447 mathematical theorems in Lean 4 format for evaluation.