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

• URL: http://arxiv.org/abs/2506.17104v1
• Date: Fri, 20 Jun 2025 16:09:56 GMT
• Title: Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving
• Authors: Chuxue Cao, Mengze Li, Juntao Dai, Jinluan Yang, Zijian Zhao, Shengyu Zhang, Weijie Shi, Chengzhong Liu, Sirui Han, Yike Guo,
• Abstract summary: Large language models (LLMs) have shown promising first-order logic (FOL) reasoning capabilities.<n>However, their effectiveness in complex mathematical reasoning involving multi-step FOL deductions is still under-researched.<n>We propose DREAM, a self-adaptive solution that enhances the Diversity and REAsonability of LLMs' generation strategies.
• Score: 14.569345246475509
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• The Promise and Limits of LLMs in Constructing Proofs and Hints for Logic Problems in Intelligent Tutoring Systems [4.146233417549798]
  Large language models (LLMs) offer promising capabilities for dynamic feedback generation.<n>LLMs risk producing hallucinations or pedagogically unsound explanations.<n>DeepSeek-V3 achieved superior performance with 84.4% accuracy on stepwise proof construction.
  arXiv  Detail & Related papers  (2025-05-07T18:48:23Z)
• Guiding Reasoning in Small Language Models with LLM Assistance [23.3038074903744]
  Small Language Models cast doubt suitability for tasks demanding deep, multi-step logical deduction.<n>This paper introduces a framework called Small Reasons, Large Hints, which selectively augments SLM reasoning with targeted guidance from large language models.<n>Our experiments on mathematical reasoning datasets demonstrate that targeted external scaffolding significantly improves performance.
  arXiv  Detail & Related papers  (2025-04-14T06:32:45Z)
• Weaker LLMs' Opinions Also Matter: Mixture of Opinions Enhances LLM's Mathematical Reasoning [3.0449420665138485]
  Large Language Models (LLMs) have raised interest in their formal reasoning capabilities, particularly in mathematics.<n>We propose a post-training approach leveraging a mixture of opinions (MoO) from weaker ancillary LLMs to enhance a (relatively) stronger LLM's reasoning.<n>Our results show that incorporating weaker LLMs' opinions improves mathematical reasoning by an average of 5%, highlighting the value of diverse perspectives in reasoning tasks.
  arXiv  Detail & Related papers  (2025-02-26T23:22:02Z)
• Teaching LLMs According to Their Aptitude: Adaptive Reasoning for Mathematical Problem Solving [55.895917967408586]
  Existing approaches to mathematical reasoning with large language models rely on Chain-of-Thought (CoT) for generalizability or Tool-Integrated Reasoning (TIR) for precise computation.<n>We propose TATA (Teaching LLMs According to Their Aptitude), an adaptive framework that enables LLMs to personalize their reasoning strategy spontaneously.
  arXiv  Detail & Related papers  (2025-02-17T16:56:23Z)
• Satori: Reinforcement Learning with Chain-of-Action-Thought Enhances LLM Reasoning via Autoregressive Search [57.28671084993782]
  Large language models (LLMs) have demonstrated remarkable reasoning capabilities across diverse domains.<n>Recent studies have shown that increasing test-time computation enhances LLMs' reasoning capabilities.<n>We propose a two-stage training paradigm: 1) a small-scale format tuning stage to internalize the COAT reasoning format and 2) a large-scale self-improvement stage leveraging reinforcement learning.
  arXiv  Detail & Related papers  (2025-02-04T17:26:58Z)
• LLM2: Let Large Language Models Harness System 2 Reasoning [65.89293674479907]
  Large language models (LLMs) have exhibited impressive capabilities across a myriad of tasks, yet they occasionally yield undesirable outputs.<n>We introduce LLM2, a novel framework that combines an LLM with a process-based verifier.<n>LLMs2 is responsible for generating plausible candidates, while the verifier provides timely process-based feedback to distinguish desirable and undesirable outputs.
  arXiv  Detail & Related papers  (2024-12-29T06:32:36Z)
• What Makes In-context Learning Effective for Mathematical Reasoning: A Theoretical Analysis [81.15503859645149]
  In this paper, we aim to theoretically analyze the impact of in-context demonstrations on large language models' reasoning performance.<n>We propose a straightforward, generalizable, and low-complexity demonstration selection method named LMS3.
  arXiv  Detail & Related papers  (2024-12-11T11:38:11Z)
• GIVE: Structured Reasoning of Large Language Models with Knowledge Graph Inspired Veracity Extrapolation [108.2008975785364]
  Graph Inspired Veracity Extrapolation (GIVE) is a novel reasoning method that merges parametric and non-parametric memories to improve accurate reasoning with minimal external input.<n>GIVE guides the LLM agent to select the most pertinent expert data (observe), engage in query-specific divergent thinking (reflect), and then synthesize this information to produce the final output (speak)
  arXiv  Detail & Related papers  (2024-10-11T03:05:06Z)
• Large Language Models Struggle with Unreasonability in Math Problems [41.970853209666224]
  Large Language Models (LLMs) have shown remarkable success on a wide range of math and reasoning benchmarks.<n>We observe that they often struggle when faced with unreasonable math problems.<n>We propose the textbfUnreasonable Math Problems (UMP) benchmark, designed to evaluate LLMs' ability to detect and respond to unreasonable math problem statements.
  arXiv  Detail & Related papers  (2024-03-28T12:04:28Z)
• Identifying Factual Inconsistencies in Summaries: Grounding LLM Inference via Task Taxonomy [48.29181662640212]
  Factual inconsistencies pose a significant hurdle for the faithful summarization by generative models. We consolidate key error types of inconsistent facts in summaries, and incorporate them to facilitate both the zero-shot and supervised paradigms of LLMs.
  arXiv  Detail & Related papers  (2024-02-20T08:41:23Z)
• Fill in the Blank: Exploring and Enhancing LLM Capabilities for Backward Reasoning in Math Word Problems [17.80128896525717]
  backward reasoning is relatively unexplored. backward reasoning can be seen as the ''inverse'' of forward reasoning. We propose variations of three different forward reasoning strategies to improve performance.
  arXiv  Detail & Related papers  (2023-10-03T12:03:06Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.