Exposing LLM-Generated Logical Flaws in Reasoning via Automated Theorem Proving (arxiv.org)

Researchers have unveiled a new evaluation framework called MATP, designed to uncover logical flaws in the reasoning of Large Language Models (LLMs) using Multi-step Automated Theorem Proving. While LLMs have made significant strides in reasoning tasks, they frequently produce nuanced logical errors that traditional methods, such as fact-checking and self-consistency evaluations, fail to identify. MATP addresses this gap by converting natural language reasoning into First-Order Logic (FOL) and employing automated theorem provers to rigorously assess logical validity across reasoning steps. The significance of MATP for the AI/ML community lies in its ability to enhance the reliability of LLM-generated reasoning, particularly in high-stakes areas like healthcare and law. In tests involving over 10,830 reasoning instances generated by 10 different LLMs, MATP demonstrated a remarkable improvement, outperforming prompting-based baselines by over 42 percentage points in reasoning step verification. This research highlights the importance of developing more sophisticated tools for evaluating AI reasoning, revealing substantial variations in performance based on the models used and suggesting that specialized reasoning models tend to generate more logically consistent outputs than their general counterparts.