超越正确性：用多步自动定理证明揭示大语言模型推理中的逻辑缺陷
Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving
AI 导读
研究者提出 MATP 框架，用多步自动定理证明揭示大语言模型推理中隐藏的逻辑缺陷。该框架将自然语言推理翻译为一阶逻辑，再用自动定理证明器逐步验证逻辑有效性。在 10 个大语言模型生成的 10,830 条推理实例（任务来自 PrOntoQA-OOD、ProofWriter、FOLIO）上，MATP 的推理步骤验证比提示词基线高出逾 42 个百分点，且推理模型的输出比通用模型更具逻辑连贯性。