# Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 21 of its 61 references that are in the map.
- First posted on arXiv 29 Dec 2025.

## Placed in

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

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [GPT-4o System Card](https://mlsanity.com/paper/2410.21276/) (2024)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Logic-RL: Unleashing LLM Reasoning with Rule-Based Reinforcement Learning](https://mlsanity.com/paper/2502.14768/) (2025)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [ROSCOE: A Suite of Metrics for Scoring Step-by-Step Reasoning](https://mlsanity.com/paper/2212.07919/) (2022)
- [Foundation Models for Decision Making: Problems, Methods, and Opportunities](https://mlsanity.com/paper/2303.04129/) (2023)
- [Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples](https://mlsanity.com/paper/2305.15269/) (2023)
- [Evaluating Step-by-step Reasoning Traces: A Survey](https://mlsanity.com/paper/2502.12289/) (2025)
- [Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation](https://mlsanity.com/paper/2305.15541/) (2023)
- [MR-GSM8K: A Meta-Reasoning Benchmark for Large Language Model Evaluation](https://mlsanity.com/paper/2312.17080/) (2023)
- [Determinants of LLM-assisted Decision-Making](https://mlsanity.com/paper/2402.17385/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Logic-of-Thought: Injecting Logic into Contexts for Full Reasoning in Large Language Models](https://mlsanity.com/paper/2409.17539/) (2024)
- [Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection](https://mlsanity.com/paper/2405.02318/) (2024)
- [Practical Reasoning Interruption Attacks on Reasoning Large Language Models](https://mlsanity.com/paper/2505.06643/) (2025)
- [Assessing the Sensitivity and Alignment of FOL Closeness Metrics](https://mlsanity.com/paper/2501.08613/) (2025)

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

- [AgentArk: Distilling Multi-Agent Intelligence into a Single LLM Agent](https://mlsanity.com/paper/2602.03955/) (2026)
- [Position: Logical Soundness is not a Reliable Criterion for Neurosymbolic Fact-Checking with LLMs](https://mlsanity.com/paper/2604.04177/) (2026)
- [R2IF: Aligning Reasoning with Decisions via Composite Rewards for Interpretable LLM Function Calling](https://mlsanity.com/paper/2604.20316/) (2026)
- [Constraint-Guided Enterprise Data Mapping with Large Language Models](https://mlsanity.com/paper/2608.24218/) (2026)
- [Lost in Perception: Isolating Perceptual and Reasoning Failures in Multimodal Physics and Geometry Reasoning](https://mlsanity.com/paper/2609.18991/) (2026)
- [SoK: Formal Methods for Fact-Checking and Information Integrity](https://mlsanity.com/paper/2609.23239/) (2026)

## Abstract (arXiv)

Large Language Models (LLMs) have demonstrated impressive reasoning capabilities, leading to their adoption in high-stakes domains such as healthcare, law, and scientific research. However, their reasoning often contains subtle logical errors masked by fluent language, posing significant risks for critical applications. While existing approaches like fact-checking, self-consistency methods, and rule-based validation provide partial solutions, they fail to detect complex logical flaws in multi-step reasoning. To overcome these challenges, we present MATP, an evaluation framework for systematically verifying LLM reasoning via Multi-step Automatic Theorem Proving. MATP translates natural language reasoning into First-Order Logic (FOL) and applies automated theorem provers to assess step-by-step logical validity. This approach identifies hidden logical errors and provides fine-grained classifications of reasoning correctness. Evaluations on a benchmark comprising 10,830 reasoning instances generated by 10 LLMs across tasks from PrOntoQA-OOD, ProofWriter, and FOLIO show that MATP surpasses prompting-based baselines by over 42 percentage points in reasoning step verification. It further reveals model-level disparities, with reasoning models generating more logically coherent outputs than general models. These results demonstrate MATP's potential to enhance the trustworthiness of LLM-generated reasoning.