Logic- LM : Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning (2023)

Abstract: Large Language Models (LLMs) have shown human-like reasoning abilities but still struggle with complex logical problems. This paper introduces a novel framework, Logic-LM, which integrates LLMs with symbolic solvers to improve logical problem-solving. Our method first utilizes LLMs to translate a natural language problem into a symbolic formulation. Afterward, a deterministic symbolic solver performs inference on the formulated problem. We also introduce a self-refinement module, which utilizes the symbolic solver’s error messages to revise symbolic formalizations. We demonstrate Logic-LM’s effectiveness on five logical reasoning datasets: ProofWriter, PrOntoQA, FOLIO, LogicalDeduction, and AR-LSAT. On average, Logic-LM achieves a significant performance boost of 39.2% over using LLM alone with standard prompting and 18.4% over LLM with chain-of-thought prompting. Our findings suggest that Logic-LM, by combining LLMs with symbolic logic, offers a promising avenue for faithful logical reasoning.

## introduction logical reasoning is a cognitive process that involves using evidence, arguments, and logic to arrive at conclusions or make judgments @xcite . it plays a central role in intelligent systems for problem-solving, decision-making, and critical thinking. recently, large language models (llms) @xcite @xcite have exhibited emergent ability to "reason" like human @xcite . when prompted with step-wise explanations of reasoning ("chain of thoughts"), or a simple prompt "let's think step by step.", these models are able to answer questions with explicit reasoning steps @xcite . despite the advances of llms, they still struggle with complex logical reasoning problems @xcite . recent studies @xcite @xcite found that llms occasionally make unfaithful reasoning, i.e., the derived conclusion does not follow the previously generated reasoning chain. while chain-of-thought may imitate human reasoning processes, the fundamental nature of llms remains that of black-box probabilistic models, lacking a mechanism to guarantee the faithfulness of reasoning @xcite . in contrast, symbolic inference engines, such as expert systems @xcite , are faithful and transparent because the reasoning is based on symbolic-represented knowledge and follows well-defined inference rules that adhere to logical principles. the main obstacle is how to accurately translate a problem into symbolic representations, considering the inherent ambiguity and flexibility of natural language. this is precisely where llms excel, making llms a promising complement to symbolic solvers. this drives our exploration of neuro-symbolic methods that integrate llms with symbolic reasoning. as illustrated in figure 1 , we present logic-lm, a novel framework that decomposes a logical reasoning problem into three stages: problem formulation, symbolic reasoning, and result interpretation. during problem formulation, an llm converts the natural language description of the problem into an appropriate symbolic formulation, identifying key entities, facts, and rules present in the problem statement. subsequently, at the symbolic reasoning stage, a deterministic symbolic solver performs inference on the symbolic formulation. lastly, a result interpreter explains the output and maps it to the correct answer. by incorporating llms with symbolic solvers, we can exploit the robust natural language understanding capabilities of llms to precisely represent the problem using symbolic representations, while also taking advantage of the logical faithfulness and transparency offered by symbolic solvers. to improve the accuracy of the symbolic parsing, we also incorporate the idea of self-refinement to iteratively revise the generated logical form using the error messages from the symbolic solver as feedback. we showcase the adaptability and effectiveness of logic-lm on five logical reasoning datasets: proofwriter @xcite , pron-toqa @xcite , folio @xcite , ar-lsat @xcite , and the log-icaldeduction dataset from bigbench @xcite . these datasets cover a wide range of logical reasoning problems, including: our evaluations show that the strategy of integrating llms with symbolic solvers performs significantly better than purely relying on llms for logical reasoning, with an average improvement of 39.2% over the standard prompting and 18.4% over the chain-of-thought prompting ( § 4.1). we also find that logic-lm becomes increasingly effective as the required reasoning depth increases ( § 4.3). finally, by analyzing the impact of selfrefinement, we highlight the effectiveness of incrementally revising symbolic formalizations when interacting with the symbolic solver ( § 4.4). ## related work language models for logical reasoning. recent works in adapting llms for logical reasoning tasks can be broadly categorized into two groups: 1) fine-tuning approaches that optimize llms' reasoning ability through fine-tuning or training specialized modules @xcite @xcite , and 2) in-context learning approaches that design special prompts to elicit llms' step-by-step reasoning capabilities. typical methods include chain-of-thought prompting @xcite that generates explanations before the final answer and the least-tomost prompting @xcite that breaks the problem down into simpler components that can be solved individually. both the above approaches perform reasoning directly over natural language (nl), providing greater flexibility than symbolicbased reasoning. however, the intrinsic complexity and ambiguity of nl also bring undesired issues such as unfaithful reasoning and hallucinations. different from prior works, we use symbolic language as the basic unit of reasoning. this effectively transfers the burden of executing complex, precise reasoning from llms to more reliable, interpretable external symbolic solvers. simultaneously, we leverage the strong in-context learning ability of llms to formulate the nl-based problem into suitable symbolic representations, thus maintaining the benefit of flexibility. although prior works @xcite @xcite @xcite also propose neuro-symbolic methods to combine neural networks with symbolic reasoning, these methods suffer from limitations such as hand-crafted or specialized module designs that are not easily generalizable, or brittleness due to the difficulty of optimization. in contrast, we propose a more generalizable framework that integrates modern llms with symbolic logic without the need for training or designing complex problem-specific modules. tool-augmented language models. language models have inherent limitations such as the inability to access up-to-date information, take actions, or perform precise mathematical reasoning. to no giant language model could have bad performance. if a language model has good performance, it is used by some researchers. a work used by some researchers should be popular. if bert is a giant language model, then the same for gpt3. bert is a giant language model. is the following statement true, false, or unknown? gpt3 is popular. is the following statement true, false, or unknown? nails cannot conduct electricity. ## experiments datasets. we evaluate logic-lm on five common logical reasoning datasets, as follows. prontoqa @xcite is a recent synthetic dataset created to analyze the capacity of llms for deductive reasoning. we use the hardest fictional characters version of the dataset, based on the results in @xcite . each version is divided into different subsets depending on the number of reasoning hops required. we use the hardest 5-hop subset for evaluation. each question in prontoqa aims to validate a new fact's veracity, such as "true or false: alex is not shy.". proofwriter @xcite is another commonly used dataset for deductive logical reasoning. compared with prontoqa, the problems are expressed in a more naturalistic language form. we use the open-world assumption (owa) subset in which each example is a (problem, goal) pair and the label is one of {proved, disproved, unknown}. the dataset is divided into five parts, each part requiring 0, ≤ 1, ≤ 2, ≤ 3, @xmath0, respectively. we evaluate the hardest depth-5 subset. to reduce overall experimentation costs, we randomly sample 600 examples in the test set and ensure a balanced label distribution. folio @xcite is a challenging expert-written dataset for logical reasoning. the problems are mostly aligned with real-world knowledge and use highly natural wordings, and the questions require complex first-order logic reasoning to solve. we use the entire folio test set for evaluation, consisting of 204 examples. logicaldeduction is a challenging logical reasoning task from the bigbench @xcite collaborative benchmark. the problems are mostly about deducing the order of a sequence of objects from a minimal set of conditions. we use the full test set consisting of 300 examples. ar-lsat @xcite is a dataset that collects all analytical logic reasoning questions from the law school admission test from 1991 to 2016. we use the test set which has 231 multiplechoice questions. ar-lsat is particularly challenging, with state-of-the-art models only achieving performance slightly better than random guessing @xcite . we convert all examples into a standard multiplechoice format, comprising a problem statement, a question, and potential answers, as shown in figure 2. we also select 1-5 examples from the training set of each dataset as in-context examples. detailed data statistics are in appendix b. baselines. we compare our model against two baselines that depend solely on llms for logical reasoning: 1) standard llms, which leverage incontext learning to directly answer the question; and 2) chain-of-thought (cot) @xcite , which adopts a step-by-step problem-solving approach, generating explanations before providing the final answer. we separately evaluate the settings that chatgpt (gpt-3.5-turbo), gpt-3.5 (text-davinci-003) @xcite and gpt-4 (gpt-4) (openai, 2023) serve as the underlying llms for all models. to ensure fair comparisons, we use the same in-context examples for all models. for reproducible results, we set the temperature to 0 and select the response with the highest probability from llms. since all examples are formed as multiple-choice questions, we evaluate model performance based on the accuracy of selecting the correct answer. ## conclusion and future work in this work, we propose a novel approach to address logical reasoning problems by combining large language models with symbolic solvers. we introduce logic-lm, one instantiation of such a framework, and demonstrate how it significantly improves performance over pure llms and chainof-thought prompting techniques. while logic-lm has proven to be a capable system, it can be further improved with extension to more flexible and powerful logic systems. for example, statistical relational learning (srl) systems such as markov logic networks @xcite and probabilistic soft logic @xcite have demonstrated great promise in reasoning under uncertainty and integration with our framework would enable even more adaptive problem-solving capabilities. additionally, our method can be extended to reasoning problems requiring commonsense, which remains a significant challenge as they often require reasoning over complex and ambiguous rules.