LINC : A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers (2023)

Abstract: Logical reasoning, i.e., deductively inferring the truth value of a conclusion from a set of premises, is an important task for artificial intelligence with wide potential impacts on science, mathematics, and society. While many prompting-based strategies have been proposed to enable Large Language Models (LLMs) to do such reasoning more effectively, they still appear unsatisfactory, often failing in subtle and unpredictable ways. In this work, we investigate the validity of instead reformulating such tasks as modular neurosymbolic programming, which we call LINC: Logical Inference via Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser, translating premises and conclusions from natural language to expressions in first-order logic. These expressions are then offloaded to an external theorem prover, which symbolically performs deductive inference. Leveraging this approach, we observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate. On ProofWriter, augmenting the comparatively small open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5 and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%, respectively. When used with GPT-4, LINC scores 26% higher than CoT on ProofWriter while performing comparatively on FOLIO. Further analysis reveals that although both methods on average succeed roughly equally often on this dataset, they exhibit distinct and complementary failure modes. We thus provide promising evidence for how logical reasoning over natural language can be tackled through jointly leveraging LLMs alongside symbolic provers. All corresponding code is publicly available.

## introduction widespread adoption of large language models (llms) such as gpt-3 @xcite , @xcite , and palm @xcite have led to a series of remarkable successes in tasks ranging from text summarization to program synthesis. some of these successes have encouraged the hypothesis that such models are able to flexibly and systematically reason @xcite , especially when using prompting strategies that explicitly encourage verbalizing intermediate reasoning steps before generating the final answer @xcite @xcite . however, this reasoning ability appears to be unreliable for tasks that require reasoning out of domain @xcite , understanding negation @xcite , and following long reasoning chains @xcite . furthermore, while the standard approach of "scaling up" seems to improve performance across some reasoning domains, other domains, e.g., reasoning involving use of modus tollens, show no such improvements @xcite . these findings suggest that such models may be relying on approximate heuristics based on surface-level statistical patterns in reasoning tasks, rather than consistent, generalizable representations and strategies @xcite . at the same time, the ability to accurately and soundly perform logical reasoning is important for ai and nlp due to its impact on downstream tasks. for example: retrieval-augmented chatbots may become more truthful if it can be verified that their answers logically follow from the retrieved facts; data-driven models capable of logical reasoning may speed up progress across mathematics and the sciences through automated theorem proving and knowledge discovery; and ai tutoring systems which ensure internal logical consistency might make for better educational platforms, teaching students to think more clearly and rigorously. the question of how to enable state-of-the-art llms to become more reliable logical reasoners is thus one of great importance, with far-reaching implications. in this work, we analyze linc: logical inference via neurosymbolic computation (fig. 1 ). in linc, logical reasoning is tackled through a modular, two-step neurosymbolic process. first, the language model converts the natural language premises and desired conclusion into first-order logic (fol) expressions @xcite . second, a symbolic fol theorem prover algorithmically determines the truth value of the conclusion given the formalized premises. in practice, we also incorporate a third majority voting step, which is shown to improve performance. linc is a natural extension of recent work augmenting lanugage models with symbolic tools such as calculators or interpreters @xcite . linc has a key advantage: the language model itself no longer needs to perform any deductive reasoning, which is offloaded to the theorem prover. however, there are also clear drawbacks: the formalization from natural language to first-order logic must perfectly capture all relevant information contained in the premises, and any loss of information in the formalization procedure may lead the solver astray, leading to an incorrect conclusion. as it is not clear whether the task of formalization is more or less difficult than that of end-to-end natural language reasoning, our core interest in this work is to compare and contrast our neurosymbolic approach to existing reasoning strategies like chain-of-thought. our contributions are thus three-fold: overall, we present strong evidence for the potential of future neurosymbolic logical reasoning systems based on integrating language models and theorem provers. ## linc: logical inference via neurosymbolic computation our neurosymbolic approach to end-to-end logical reasoning consists of two stages. in the first stage, the llm acts as a semantic parser, translating nl statements into fol expressions in our supported logic language. in the second stage, these expressions are parsed from the text generated by the llm and then get passed to an automated theorem prover; we use prover9, a high-performance prover widely used in the logic community @xcite . the external solver then executes a symbolic deduction algorithm, which either returns a value from the set {true, false, uncertain} or raises an exception due to improper fol syntax (e.g., if the model fails to balance parantheses in the formulae). at its core, the strength of this approach lies in the reformulation of the problem space. end-toend nl-based reasoning allows for operation over a highly flexible expression space, but leaves the llm with the difficult task of performing explicit deductive inference over expressions in this space. using linc, we instead trade off the flexible expression space of nl for syntactically strict logic formulas, allowing us to leverage symbolic algorithms with provable guarantees that the deductive chains will be correct with respect to the semantics of the intermediate representation. making effective use of this reformulation thus requires the logic expressions generated by the llm to be 1) syntactically valid, such that they are accepted by the prover, and 2) semantically valid, such that their evaluation results in the correct conclusion. in our experiments, we mitigate these risks by using a kway majority voting procedure, which is discussed further in sec. 3. the significance of this problem space reformulation can-beyond the numerical increases in performance observed across our experimentsperhaps best be seen through an in-depth comparison of how linc and traditional end-to-end llm reasoning approaches such as chain-of-thought (cot) fail. to foreshadow our latter analysis, we find that compared to cot, linc has worse recall but better precision on true/false predictions. we discuss this further in sec. 5 and highlight that this suggests that linc, as well as neurosymbolic computation more generally, has the potential to reduce llm overconfidence and hallucination. ## experiments in this section, we present our experimental setup, the models we use, and the three baselines to which we compare linc. ## results & discussion our main results are shown in figure 3 . each bar represents either linc or one of the three baselines, while each group of bars indicates the language model used (in {starcoder+, gpt-3.5, gpt-4}). we note first that in the folio domain (figure 3a ), starcoder+-the smallest model we experiment with-benefits the most from linc, achieving a mean accuracy that is 14.2 points higher than the closest controlled baseline (56.0% vs. 41.8% with cot). we find that scratchpad, where the intermediate logical formulae are still generated but the call to the symbolic solver is ablated and replaced by the model's own prediction, does not appear to benefit performance; for starcoder+, neither scratchpad nor the naïve baseline perform better than simply deterministically predicting the most common label ("uncertain"). for gpt-3.5, the trend is similar, although the gap between linc and the closest baseline shrinks (62.6% vs. 54.9% in light of the high accuracies obtained with linc on proofwriter, we offer two plausible reasons why linc is particularly favorable on this dataset. firstly, proofwriter is-unlike foliocompletely synthetically generated, with relatively short sentences, perhaps lending itself particularly well to being formalized in fol. however, it is noteworthy that the scratchpad mode does not seem to improve performance over the naïve baseline, indicating that even if the nl-to-fol task were particularly easy in this domain, this is not something that the model is itself capable of leveraging to improve its predictions. the second reason might be that the baseline strategies struggle in this out-of-distribution setting, in which the model must generalize to a larger set of premises (with potentially longer deductive chains) than those found in the prompt. this distribution shift makes it harder for the model to ignore irrelevant premises in the question and carry out all deductive chains correctly. meanwhile, with linc, the symbolic solver robustly handles irrelevant premises and long deductive chains, since the llm only needs to translate each sentence into fol. to test this last explanation further, we plot each model's performance across proofwriter as a func-tion of the necessary proof depth in figure 4 . we note first that starcoder+'s performance remains flat and close to chance with all three baseline methods (figure 4a ). meanwhile, with linc the performance remains far above chance, although it drops somewhat as necessary proof depth increases; this performance drop suggests that starcoder+ struggles somewhat with the nl-to-fol translation task as the problem at hand gets larger. for gpt-3.5, all baselines perform above chance at proof depth 0 (i.e., where the conclusion can immediately be reached from the premises), but then quickly drop back down (figure 4b ). while chain-of-thought prompting allows the model to complete some depth-1 tasks, even this strategy then performs equivalently to chance (within 1 standard deviation) for higher depths. when augmented with linc, however, gpt-3.5 is able to achieve near-perfect performance across all proof depths, providing evidence for the scalability of this approach to longer deductive chains. finally, for gpt-4 we observe much stronger performance from the baselines; in particular, cot performs above chance for all proof depths, and all baselines perform well for shallow proofs (figure 4c ). however, even with gpt-4 the performance drops as the necessary proof depth increases with every configuration except for linc, which performs near or at ceiling through the maximum proof depth available in the dataset. ## error analysis having established that linc can improve performance in many settings, we now move on to our final research question: how do the failure modes of linc compare to those of in-context reasoning ## conclusion in this work, we present linc: logical inference via neurosymbolic computation, a neurosymbolic approach for scalable logical reasoning with large language models. our experiments show that linc leads to significant performance gains in nearly every setting we consider, and that it supports generalization to settings where the model has to reason about a much larger set of premises than it is shown in the in-context learning examples. furthermore, carrying out a quantitative and qualitative analysis of the mistakes made by linc, we find evidence that it may complement purely in-context reasoning strategies such as chain-of-thought prompting, since they differ greatly in the types and frequencies of mistakes made. this work thus supports the efficacy of neurosymbolic approaches to natural language reasoning, setting the stage for continued advances in combining large language models and symbolic reasoning engines; we discuss several promising future directions in appendix a.