Beyond correctness: using multi-step automated theorem proving to reveal logical flaws in large language model reasoning

Researchers propose the MATP framework, which uses multi-step automated theorem proving to reveal hidden logical flaws in large language model reasoning. The framework translates natural language reasoning into first-order logic, then uses an automated theorem prover to verify logical validity step by step. On 10,830 reasoning instances generated by 10 large language models (tasks from PrOntoQA-OOD, ProofWriter, FOLIO), MATP's reasoning-step verification exceeded the prompting baseline by more than 42 percentage points, and reasoning models' outputs were more logically coherent than those of general-purpose models.