LAMBADA : Backward Chaining for Automated Reasoning in Natural Language (2023)

Abstract: Remarkable progress has been made on automated reasoning with natural text, by using Large Language Models (LLMs) and methods such as Chain-of-Thought prompting and Selection-Inference. These techniques search for proofs in the forward direction from axioms to the conclusion, which suffers from a combinatorial explosion of the search space, and thus high failure rates for problems requiring longer chains of reasoning. The classical automated reasoning literature has shown that reasoning in the backward direction (i.e. from intended conclusion to supporting axioms) is significantly more efficient at proof-finding. Importing this intuition into the LM setting, we develop a Backward Chaining algorithm, called LAMBADA, that decomposes reasoning into four sub-modules, that are simply implemented by few-shot prompted LLM inference. We show that LAMBADA achieves sizable accuracy boosts over state-of-the-art forward reasoning methods on two challenging logical reasoning datasets, particularly when deep and accurate proof chains are required.

## introduction automated reasoning, the ability to draw valid conclusions from explicitly provided knowledge, has been a fundamental goal for ai since its early days @xcite . furthermore, logical reasoning, especially reasoning with unstructured, natural text is an important building block for automated knowledge discovery and holds the key for future advances across various scientific domains. while in recent years tremendous progress has been made towards natural language understanding thanks to pretrained language models (lms) @xcite , the performance of these models for logical reasoning still lags behind @xcite @xcite compared to the advancements in other areas such as reading comprehension and question-answering. ## related work the deep learning based models that have been developed to solve text-based (logical) reasoning tasks can be categorized as follows (see @xcite chang 2022 for a recent survey of the literature). pretraining on relevant tasks: pretraining an lm on corpora relevant to the target reasoning task can lead to improvements @xcite . pretraining is, however, costly especially for larger lms. implicit reasoning: these approaches finetune lms to produce the label directly given the input @xcite @xcite ; reasoning is expected to happen implicitly in the parameters of the lm. it has been shown that finetuning lms on logical reasoning tasks makes them learn spurious correlations @xcite , and is not robust to multi-hop reasoning @xcite . besides, finetuning large lms is costly especially when the dataset is large, and may introduce distributional shocks to the model @xcite . in this paper, we focus on models that only take in-context examples as supervision. explicit reasoning: generating the intermediate reasoning steps such as the chain of reasoning @xcite @xcite @xcite has shown substantial improvement for many reasoning tasks @xcite . such chains have been explored both in the forward and the backward directions, e.g., using multiple constrained lms for logical reasoning @xcite . @xcite investigated how transformer models perform when trained to perform forward or backward chaining, and drew conclusions about their internal reasoning strategies. we compare against a popular recent prompting strategy, namely chain-of-thought (cot) @xcite , from this category. verifiers: to improve cot, some works train a verifier using chain-level labels. the verifier takes a reasoning chain produced by the model as input and judges the quality of the chain @xcite @xcite . using this verifier, one can then generate multiple reasoning chains (e.g., by running the algorithm multiple times with different decoding temperatures) and use the best chain according to the verifier. since lambada also generates proofs, verifiers are also applicable to our algorithm. in this paper, we assume not having access to chain-level labels, and leave experiments with verifiers as future work. ## lambada: language model augmented backward chaining we focus on performing automated reasoning over facts, i.e., natural language assertions such as "nice people are red", that are coherent but not necessarily grounded in reality. a rule is a natural language statement that is either of the form, or can be rewritten in the form, "if p then q"; e.g., "rough, cold people are blue" can be rewritten as "if a person is rough and cold, then they are blue". p is called the antecedent and q is called the consequent of the rule. a theory c consists of facts @xmath0, f 2 , . . . , f n } and rules @xmath1, r 2 , . . . , r m }. we let g represent a goal that we would like to prove or disprove based on the theory. an example theory with fictional characters and rules is demonstrated in figure 1 . based on the theory, one should prove or disprove the goal "eric is nice". ## experimental setup we describe our baselines and datasets here, and provide further implementation details in appendix d. unless stated otherwise, all experiments are based on the palm 540b model @xcite . ## results we now describe the results and compare lam-bada and the baselines in detail. ## conclusion and future directions we developed lambada, an algorithm for deductive logical reasoning with natural language that combines the capacity of lms to handle naturalistic text input with the backward chaining algorithm for robust symbolic reasoning. we showed that lambada achieves significant improvements over competitive approaches on challenging benchmarks, both in terms of label accuracy (predicting if a statement can be proved or disproved based on a theory) and proof accuracy. importantly, this improvement was also observed in a dataset that expresses the theory in more naturalistic expressions, clearly illustrating the benefit of combining an lm with reasoning modules. we also demonstrated the query efficiency and lexical robustness of lam-bada. although in this paper we only experiment with formal reasoning problems and datasets, we believe our key insight on the efficacy of backward, goal-directed reasoning with lms has broader implications and can be adapted to other nlp tasks where multi-step inference is required.