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

arXiv: https://arxiv.org/abs/2506.17104 · HTML: https://mlsanity.com/paper/2506.17104/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 23 of its 50 references that are in the map.
- First posted on arXiv 20 Jun 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 23 of 23)

- [Large Language Monkeys: Scaling Inference Compute with Repeated Sampling](https://mlsanity.com/paper/2407.21787/) (2024)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search](https://mlsanity.com/paper/2410.15700/) (2024)
- [Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation](https://mlsanity.com/paper/2502.06563/) (2025)
- [RuleArena: A Benchmark for Rule-Guided Reasoning with LLMs in Real-World Scenarios](https://mlsanity.com/paper/2412.08972/) (2024)
- [Mix Data or Merge Models? Balancing the Helpfulness, Honesty, and Harmlessness of Large Language Model via Model Merging](https://mlsanity.com/paper/2502.06876/) (2025)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection](https://mlsanity.com/paper/2405.02318/) (2024)
- [ThinkPatterns-21k: A Systematic Study on the Impact of Thinking Patterns in LLMs](https://mlsanity.com/paper/2503.12918/) (2025)
- [REFACTOR: Learning to Extract Theorems from Proofs](https://mlsanity.com/paper/2402.17032/) (2024)
- [SafeLawBench: Towards Safe Alignment of Large Language Models](https://mlsanity.com/paper/2506.06636/) (2025)
- [Assessing the Sensitivity and Alignment of FOL Closeness Metrics](https://mlsanity.com/paper/2501.08613/) (2025)
- [On the logical skills of large language models: evaluations using arbitrarily complex first-order logic problems](https://mlsanity.com/paper/2502.14180/) (2025)

## Built on by (most cited first, 8 of 8)

- [LRAS: Advanced Legal Reasoning with Agentic Search](https://mlsanity.com/paper/2601.07296/) (2026)
- [What, Whether and How? Unveiling Process Reward Models for Thinking with Images Reasoning](https://mlsanity.com/paper/2602.08346/) (2026)
- [Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification](https://mlsanity.com/paper/2601.22642/) (2026)
- [Reasoning Fails Where Step Flow Breaks](https://mlsanity.com/paper/2604.06695/) (2026)
- [Shaping Schema via Language Representation as the Next Frontier for LLM Intelligence Expanding](https://mlsanity.com/paper/2605.09271/) (2026)
- [Forty Shades of Blue: Quality-Diversity Alignment via Mode-Conditioned Reinforcement Learning](https://mlsanity.com/paper/2609.14896/) (2026)
- [Zero-Effort Image-to-Music Generation: An Interpretable RAG-based VLM Approach](https://mlsanity.com/paper/2509.22378/) (2025)
- [Causal Reasoning Favors Encoders: On The Limits of Decoder-Only Models](https://mlsanity.com/paper/2512.10561/) (2025)

## Abstract (arXiv)

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.