Verifiable, Debuggable, and Repairable Commonsense Logical Reasoning via LLM -based Theory Resolution (2024)

Abstract: Recent advances in Large Language Models (LLM) have led to substantial interest in their application to commonsense reasoning tasks. Despite their potential, LLMs are susceptible to reasoning errors and hallucinations that may be harmful in use cases where accurate reasoning is critical. This challenge underscores the need for verifiable, debuggable, and repairable LLM reasoning. Recent works have made progress toward verifiable reasoning with LLMs by using them as either (i) a reasoner over an axiomatic knowledge base, or (ii) a semantic parser for use in existing logical inference systems. However, both settings are unable to extract commonsense axioms from the LLM that are not already formalized in the knowledge base, and also lack a reliable method to repair missed commonsense inferences. In this work, we present LLM-TRes, a logical reasoning framework based on the notion of “theory resolution” that allows for seamless integration of the commonsense knowledge from LLMs with a verifiable logical reasoning framework that mitigates hallucinations and facilitates debugging of the reasoning procedure as well as repair. We crucially prove that repaired axioms are theoretically guaranteed to be given precedence over flawed ones in our theory resolution inference process. We conclude by evaluating on three diverse language-based reasoning tasks—preference reasoning, deductive reasoning, and causal commonsense reasoning—and demonstrate the superior performance of LLM-TRes vs. state-of-the-art LLM-based reasoning methods in terms of both accuracy and reasoning correctness.

## introduction the rise of large language models (llms) has marked a pivotal moment in the real-world deployment of ai, particularly due to the exceptional ability of llms to handle complex reasoning tasks @xcite . research has shown that llms have acquired significant commonsense knowledge @xcite , which is crucial for engaging with real-world users in tasks such as question answering @xcite and recommendation @xcite . unfortunately, llms are prone to a variety of reasoning errors; for example, they commonly incorporate superficially plausible but factually incorrect information into their reasoning in a phenomenon known as hallucination @xcite @xcite . furthermore, since the underlying reasoning process of the llm is latent and hence largely opaque, validating reasoning soundness and identifying errors remains an open research problem. such issues present a significant challenge to the reliability of using llms as reasoning systems, which impedes their practical utility @xcite . in light of these obstacles, recent research has proposed methodologies for extracting verifiable reasoning from llms by leveraging formal reasoning procedures. such works fall under two main categories: (i) using the llm as a reasoner across an axiomatic knowledge base, while organizing the reasoning process into simpler subgoals to facilitate soundness of the overall reasoning @xcite . (ii) leveraging the llm as a semantic parser that translates natural language statements into logical axioms, followed by the use of an off-the-shelf theorem prover to perform logical reasoning @xcite . while these seminal works have made progress towards verifiable llm reasoning, their application in real-world tasks requiring commonsense reasoning is limited since they all suffer from the inability to extract verifiable commonsense axioms from the llm that are not already formalized in the provided knowledge base axioms. hence, these existing methodologies critically lack the ability to leverage the llm as a verifiable commonsense recipe 2: "cajun catfish stew" " " " " " " recipe 2: "cajun catfish stew" " " " " " " recipe 1: "garlic shrimp" recipe 1 is the more probable recipe before repair. after repair, recipe 2 is now the more probable recipe. i'd like a seafood recipe with a kick to it. ## repairability of erroneous resolution since llm-tres provides access to atomic inference steps in the resolution process, it facilitates verifiability and debuggability. although the entailment probabilities assigned by the llms may be erroneous, the exact resolution step at which the failure occurs is discernible. furthermore, it can be easily corrected by introducing a rectifying rule into the knowledge base. an example of such a case is presented in figure 1 . the llm's mistake in assigning a low entailment score for "catfish" to entail "seafood" leads to incorrect reasoning. however, introducing the correct axiom ∀y"catfish"(y) =⇒ "seafood"(y) to the kb repairs this mistake. the following proposition formalizes this property and is proven in appendix a. proposition 1. consider proof p ϕ c using axiom ϕ that derives clause c. for any incorrect llm reasoning axiom ϕ, a repair axiom ϕ ′ can be inserted such that p ϕ ′ c will be produced before p ϕ c . ## experiments we evaluate llm-tres on three different tasks involving commonsense reasoning on natural language data: preference reasoning, deductive reasoning, and causal commonsense reasoning. we release our implementation and data foot_1 . ## conclusion we presented llm-tres, a novel framework for formal reasoning with llms based on theory resolution that allowed us to integrate llms into resolution logical reasoning seamlessly. by providing access to every atomic reasoning step, llm-tres enabled verifiability and debuggability of the process. it also offered a reliable repairing mechanism for correcting flaws in the llm reasoning by asserting the particular missed axiom which was theoretically guaranteed to override the mistakenly low-probability resolution step. the promising performance of llm-tres on preference reasoning, deductive reasoning, and causal commonsense reasoning tasks demonstrates its efficacy in providing accurate answers and correct proofs. these capabilities make llm-tres a robust foundation for counteracting hallucination and pave the way for more trustworthy deployment of llm-based commonsense reasoners in applications where correctness, verifiability, and repairability are paramount.