# Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation

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

## Key facts

- Cited by 28 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 11 of its 42 references that are in the map.
- First posted on arXiv 10 Feb 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

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

- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Mistral 7B](https://mlsanity.com/paper/2310.06825/) (2023)
- [Mixtral of Experts](https://mlsanity.com/paper/2401.04088/) (2024)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [AR-LSAT: Investigating Analytical Reasoning of Text](https://mlsanity.com/paper/2104.06598/) (2021)
- [Won't Get Fooled Again: Answering Questions with False Premises](https://mlsanity.com/paper/2307.02394/) (2023)
- [LAB: Large-Scale Alignment for ChatBots](https://mlsanity.com/paper/2403.01081/) (2024)
- [ConditionalQA: A Complex Reading Comprehension Dataset with Conditional Answers](https://mlsanity.com/paper/2110.06884/) (2021)
- [ORAN-Bench-13K: An Open Source Benchmark for Assessing LLMs in Open Radio Access Networks](https://mlsanity.com/paper/2407.06245/) (2024)
- [DiLA: Enhancing LLM Tool Learning with Differential Logic Layer](https://mlsanity.com/paper/2402.11903/) (2024)

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

- [Semantic-Aware Logical Reasoning via a Semiotic Framework](https://mlsanity.com/paper/2509.24765/) (2025)
- [Logical Phase Transitions: Understanding Collapse in LLM Logical Reasoning](https://mlsanity.com/paper/2601.02902/) (2026)
- [Learning to Reason via Mixture-of-Thought for Logical Reasoning](https://mlsanity.com/paper/2505.15817/) (2025)
- [What Has Been Lost with Synthetic Evaluation?](https://mlsanity.com/paper/2505.22830/) (2025)
- [Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations](https://mlsanity.com/paper/2505.24264/) (2025)
- [Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving](https://mlsanity.com/paper/2506.17104/) (2025)
- [RuleReasoner: Reinforced Rule-based Reasoning via Domain-aware Dynamic Sampling](https://mlsanity.com/paper/2506.08672/) (2025)
- [LogicReward: Incentivizing LLM Reasoning via Step-Wise Logical Supervision](https://mlsanity.com/paper/2512.18196/) (2025)
- [Are LLMs Stable Formal Logic Translators in Logical Reasoning Across Linguistically Diversified Texts?](https://mlsanity.com/paper/2506.04575/) (2025)
- [Non-Interactive Symbolic-Aided Chain-of-Thought for Logical Reasoning](https://mlsanity.com/paper/2508.12425/) (2025)
- [Logical Reasoning with Outcome Reward Models for Test-Time Scaling](https://mlsanity.com/paper/2508.19903/) (2025)
- [SciEvalKit: An Open-source Evaluation Toolkit for Scientific General Intelligence](https://mlsanity.com/paper/2512.22334/) (2025)
- [Improving Symbolic Translation of Language Models for Logical Reasoning](https://mlsanity.com/paper/2601.09446/) (2026)
- [LOGICPO: Efficient Translation of NL-based Logical Problems to FOL using LLMs and Preference Optimization](https://mlsanity.com/paper/2506.18383/) (2025)
- [LogicGraph : Benchmarking Multi-Path Logical Reasoning via Neuro-Symbolic Generation and Verification](https://mlsanity.com/paper/2602.21044/) (2026)
- [Hierarchical Alignment: Enforcing Hierarchical Instruction-Following in LLMs through Logical Consistency](https://mlsanity.com/paper/2604.09075/) (2026)
- [Semiotic logical hexagon theory for LLM logical reasoning](https://mlsanity.com/paper/2607.21933/) (2026)
- [Symbolic Neural Generation with Applications to Lead Discovery in Drug Design](https://mlsanity.com/paper/2510.23379/) (2025)
- [Stemming Hallucination in Language Models Using a Licensing Oracle](https://mlsanity.com/paper/2511.06073/) (2025)
- [Cognitive Inception: Agentic Reasoning against Visual Deceptions by Injecting Skepticism](https://mlsanity.com/paper/2511.17672/) (2025)
- [Provable Long-Range Benefits of Next-Token Prediction](https://mlsanity.com/paper/2512.07818/) (2025)
- [From Natural Language to Executable Narsese: A Neuro-Symbolic Benchmark and Pipeline for Reasoning with NARS](https://mlsanity.com/paper/2604.18873/) (2026)
- [When Correct Demonstrations Hurt: Rethinking the Role of Exemplars in In-Context Learning](https://mlsanity.com/paper/2605.26350/) (2026)
- [RuleWeaver: Benchmarking Rule-Centered Scenario Reasoning for Large Language Models](https://mlsanity.com/paper/2608.26832/) (2026)
- [Instruct, Not Answer: Using Instruction Privileges in On-Policy Context Distillation](https://mlsanity.com/paper/2609.32201/) (2026)
- [Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning](https://mlsanity.com/paper/2609.37203/) (2026)
- [ArgGYM: A Procedural, Engine-Verified Benchmark for Structured Defeasible Reasoning](https://mlsanity.com/paper/2609.38409/) (2026)
- [SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers](https://mlsanity.com/paper/2610.14402/) (2026)

## Abstract (arXiv)

First-order logic (FOL) reasoning, which involves sequential deduction, is pivotal for intelligent systems and serves as a valuable task for evaluating reasoning capabilities, particularly in chain-of-thought (CoT) contexts. Existing benchmarks often rely on extensive human annotation or handcrafted templates, making it difficult to achieve the necessary complexity, scalability, and diversity for robust evaluation. To address these limitations, we propose a novel framework called ProverGen that synergizes the generative strengths of Large Language Models (LLMs) with the rigor and precision of symbolic provers, enabling the creation of a scalable, diverse, and high-quality FOL reasoning dataset, ProverQA. ProverQA is also distinguished by its inclusion of accessible and logically coherent intermediate reasoning steps for each problem. Our evaluation shows that state-of-the-art LLMs struggle to solve ProverQA problems, even with CoT prompting, highlighting the dataset's challenging nature. We also finetune Llama3.1-8B-Instruct on a separate training set generated by our framework. The finetuned model demonstrates consistent improvements on both in-distribution and out-of-distribution test sets, suggesting the value of our proposed data generation framework. Code available at: https://github.com/opendatalab/ProverGen