通过一阶逻辑定理证明提升 LLM 的高级数学推理能力
人工智能
2025-06-23 v1 计算与语言
计算机科学中的逻辑
摘要
大语言模型（LLMs）在各类领域展现出有前景的一阶逻辑（FOL）推理能力。然而，其在涉及多步骤 FOL 推理的复杂数学推理方面的效果仍受到 insufficient 研究。虽然 LLMs 在 established 数学推理基准上表现竖井，但在多步骤 FOL 任务上仍表现不佳，例如 Deepseek-Prover-V2-7B 在我们提出的定理证明数据集上仅达 4.2% 的准确率。这一问题源于对多样化证明策略的探索不足，以及早期推理错误可能削弱整个证明的潜在因素。为此，我们提出了 DREAM—a 一个自适应解决方案，通过增强 LLMs 生成策略的多样性（Diversity）和可行性（REAsonability）来提高性能。DREAM 包含 Axiom-Driven Strategy Diversification 机制以促进多样化的战略结果，并引入 Sub-Proposition Error Feedback 以帮助 LLMs 对其证明进行反思并进行纠正。我们的贡献包括：通过 FOL 定理证明推动 LLMs 数学推理的开创性进展、引入一种新型推理阶段解决方案使性能提升 0.6%至 6.4%，并提供一个包含 447 个数学定理的精选数据集（采用 Lean 4 格式）用于评估。
引用
@article{arxiv.2506.17104,
title = {Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving},
author = {Chuxue Cao and Mengze Li and Juntao Dai and Jinluan Yang and Zijian Zhao and Shengyu Zhang and Weijie Shi and Chengzhong Liu and Sirui Han and Yike Guo},
journal= {arXiv preprint arXiv:2506.17104},
year = {2025}
}