LAMBADA: Backward Chaining for Automated Reasoning in Natural Language

TL;DR

LAMBADA introduces a backward chaining approach for natural language reasoning, significantly improving proof-finding efficiency and accuracy over forward methods by decomposing reasoning into sub-modules guided by language models.

Contribution

The paper presents LAMBADA, a novel backward chaining algorithm that enhances automated reasoning in natural language by decomposing proofs into sub-modules using language models.

Findings

LAMBADA outperforms forward reasoning methods on logical reasoning datasets.

Backward chaining reduces search space and improves proof accuracy.

LAMBADA is effective for deep, complex reasoning chains.

Abstract

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.