一句话：提出 MATP 框架，将 LLM 自然语言推理转为 FOL 并用自动定理证明逐步检测逻辑错误。
大语言模型在医疗、法律等高风险场景中的推理常因语言流畅而掩盖细微逻辑错误，现有事实核查、自洽性与规则校验方法难以发现多步推理中的复杂逻辑缺陷。为此，作者提出 MATP——一种基于多步自动定理证明的评估框架：它把自然语言推理步骤翻译为一阶逻辑，再交由自动定理证明器逐步判定其逻辑有效性，并给出细粒度的推理正确性分类。在包含 10 个 LLM 生成的 10,830 条推理实例、覆盖 PrOntoQA-OOD、ProofWriter 与 FOLIO 任务的基准上，MATP 在推理步骤验证上比基于提示的基线高出 42 个百分点以上，还揭示了模型层面的差异：推理模型比通用模型生成更逻辑一致的输出。
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.
@inproceedings{abs-2512-23511,
title = {Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving},
author = {Xinyi Zheng and Ningke Li and Xiaokun Luan and Wang Kailong and Ling Shi and Meng Sun and Haoyu Wang},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3787820}
}