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

TL;DR

This paper introduces MATP, a framework that translates LLM reasoning into First-Order Logic and uses automated theorem proving to detect subtle logical errors in multi-step reasoning, improving trustworthiness.

Contribution

The paper presents MATP, a novel evaluation method that systematically verifies LLM reasoning correctness through formal logic translation and automated theorem proving, surpassing existing baselines.

Findings

MATP outperforms prompting-based baselines by over 42 percentage points in reasoning verification.

Model-specific analysis shows reasoning models produce more logically coherent outputs.

MATP effectively identifies hidden logical errors in LLM-generated reasoning.

Abstract

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.