Remarkable progress has been made on automated reasoning with natural text, by using Language Models (LMs) and methods such as Chain-of-Thought 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 the 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. These sub-modules are simply implemented by few-shot prompted LM inference. We show that LAMBADA achieves sizable accuracy boosts over state-of-the-art forward reasoning methods on challenging logical reasoning datasets, particularly when deep and accurate proof chains are required.

翻译：通过使用语言模型（LM）以及思维链与选择-推理等方法，基于自然文本的自动推理已取得显著进展。这些技术从前提出发沿正向推导结论，但会导致搜索空间组合爆炸，从而在需较长推理链的问题中产生高失败率。经典自动推理文献表明，逆向推理（即从待证的结论回溯至支撑前提）在引理寻找方面效率更高。我们将这一洞见引入语言模型场景，开发了名为LAMBADA的逆向链算法，该算法将推理过程分解为四个子模块，并通过少样本提示的LM推理简单实现。实验表明，在挑战性逻辑推理数据集上，尤其是在需要深层精确推理链时，LAMBADA较最先进的正向推理方法实现了显著的准确率提升。