SymBa: Symbolic Backward Chaining for Structured Natural Language Reasoning

TL;DR

SymBa introduces a symbolic backward chaining system that combines a symbolic solver with an LLM to enhance structured reasoning, completeness, and performance in natural language reasoning tasks.

Contribution

It presents a novel backward chaining framework integrating symbolic solving with LLMs, addressing incompleteness in prior LLM-based methods.

Findings

Significant performance improvements on seven reasoning benchmarks.

Enhanced completeness and reliability in structured reasoning.

Effective integration of symbolic solvers with LLMs for reasoning.

Abstract

To improve the performance and explainability of LLM-based natural language reasoning, structured reasoning can be applied to generate explicitly structured proofs. Among different methods for structured reasoning, we specifically focus on backward chaining, where the proof goal is recursively decomposed to subgoals by searching and applying rules. We argue that current LLM-based backward chaining systems (e.g. Least-to-most prompting and LAMBADA) are incomplete, as they omit crucial algorithmic components identified from the classic backward chaining algorithm in computational logic (SLD Resolution). To this end, we propose a novel backward chaining system, SymBa (Symbolic Backward Chaining), which integrates a symbolic solver and an LLM. In SymBa, the solver controls the proof process, and the LLM is only called when the solver requires new information to complete the proof. Empowered by completeness, SymBa achieves a significant improvement in seven deductive, relational, and arithmetic reasoning benchmarks compared to the baselines.