Automated Theorem Provers Help Improve Large Language Model Reasoning

TL;DR

This work tackles the problem of unreliable reasoning in Large Language Models (LLMs) by coupling them with external Automated Reasoning (AR) tools in a loosely coupled, neuro-symbolic framework. Problems are translated by the LLM into logic programs, which are then solved by an AR engine (Fusemate) while a Semantic Error Detection and Correction (SEDAC) framework assesses and automatically corrects both syntactic and semantic translation errors using a First-Order Logic representation. SEDAC leverages a ground-truth DCG-based NL-to-FOL translator and a formal LP-to-FOL translation, delivering corrective guidance through rewrite and derivation rules; semantic corrections, in particular, are enabled via integration with first-order ATPs, yielding substantial reductions in semantic errors and notable accuracy gains. The results on PRONTOQA steamroller problems show that integrating AR tooling can boost LLM reasoning accuracy to levels comparable to or surpassing Chain-of-Thought methods, while also providing trustworthy explanations; this approach offers a practical path toward more reliable, verifiable AI reasoning in logic-intensive tasks.

Abstract

In this paper we demonstrate how logic programming systems and Automated first-order logic Theorem Provers (ATPs) can improve the accuracy of Large Language Models (LLMs) for logical reasoning tasks where the baseline performance is given by direct LLM solutions. We first evaluate LLM reasoning on steamroller problems using the PRONTOQA benchmark. We show how accuracy can be improved with a neuro-symbolic architecture where the LLM acts solely as a front-end for translating a given problem into a formal logic language and an automated reasoning engine is called for solving it. However, this approach critically hinges on the correctness of the LLM translation. To assess this translation correctness, we secondly define a framework of syntactic and semantic error categories. We implemented the framework and used it to identify errors that LLMs make in the benchmark domain. Based on these findings, we thirdly extended our method with capabilities for automatically correcting syntactic and semantic errors. For semantic error correction we integrate first-order logic ATPs, which is our main and novel contribution. We demonstrate that this approach reduces semantic errors significantly and further increases the accurracy of LLM logical reasoning.

Figures (6)

• Figure 1: A diagram of the general structure of Large Language Model tool use. In order to successfully use a tool an LLM must successfully generate instructions for that tool that are free of both syntax errors and semantic errors. Our contributions to improving this process including auto-correcting and error type classification are shown blue.
• Figure 2: The SEDAC algorithm in pseudocode.
• Figure 3: The rule system of propose for fixing shallow semantic errors (above the double lines) and deep semantic errors (below the double lines).
• Figure 4: A graph of the percentage of error cases that contained each error type for each model. Note that this is an indication of the relative frequency of each error type for a given model and experimental condition. Error bars show the minimum and maximum values across the three trials.
• Figure 5: Re-running divergent problems after syntax only, Partial-SEDAC and Full-SEDAC corrections wrt. open-world (classical first-order logic) and closed-world (LP) semantics.