@inproceedings{cao-etal-2025-towards,
    title = "Towards Advanced Mathematical Reasoning for {LLM}s via First-Order Logic Theorem Proving",
    author = "Cao, Chuxue  and
      Li, Mengze  and
      Dai, Juntao  and
      Yang, Jinluan  and
      Zhao, Zijian  and
      Zhang, Shengyu  and
      Shi, Weijie  and
      Liu, Chengzhong  and
      Han, Sirui  and
      Guo, Yike",
    editor = "Christodoulopoulos, Christos  and
      Chakraborty, Tanmoy  and
      Rose, Carolyn  and
      Peng, Violet",
    booktitle = "Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing",
    month = nov,
    year = "2025",
    address = "Suzhou, China",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-emnlp/2025.emnlp-main.628/",
    pages = "12440--12460",
    ISBN = "979-8-89176-332-6",
    abstract = "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."
}