S ym B a: Symbolic Backward Chaining for Structured Natural Language Reasoning (2025)

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.

## introduction large language models (llms) trained with massive amounts of natural language text have shown remarkable reasoning ability in various fields, including logical and arithmetic reasoning @xcite . however, autoregressively generated explanations as in chain-ofthoughts might contain factual and logical errors, which tend to be more covert as llms scale up @xcite . to enhance the accuracy and explainability of natural language reasoning, structured reasoning has been frequently explored as an alternative. in this task, one must provide an explicitly structured explanation, i.e. a proof tree (also known as entailment tree). these structured explanations offer high interpretability by showing how premises connect to intermediate and final conclusions @xcite . among popular approaches for structured reasoning, we focus on backward chaining @xcite . backward chaining reasoners start from the goal and apply rules that decompose the goal into a set of subgoals. it is known to be efficient as it does not require a combinatorial search to generate the next step @xcite . consequently, previous works have proposed llm-based backward chaining systems, which utilize few-shot llms to execute subtasks of the backward chaining process @xcite @xcite . however, we argue that popular llm-based backward chaining systems, namely least-to-most prompting @xcite and lambada @xcite , are incomplete. we compare their implementation to a classic backward chaining algorithm from computational logic-sld resolution @xcite -and provide minimal examples that show their incompleteness in section 3.1. to address this issue, we propose symba (symbolic backward chaining), a method that applies an sld resolution-based symbolic solver directly to natural language reasoning. in symba, the solver controls the proof process, and the llm is only called when the solver requires new information to complete the proof. by this novel solver-llm integration, symba benefits from both the completeness of the sld resolution and the natural language reasoning capability of llms. symba outperforms baselines on answer accuracy, proof accuracy, and efficiency in seven benchmarks from deductive, relational, and arithmetic reasoning. empirical results show that least-tomost prompting suffers from low proof accuracy in complex problems. lambada, on the other hand, cannot handle relational and arithmetic reasoning properly. we claim that these are the direct consequences of their incomplete design. in summary, our contributions are as follows. ## analysis 6.1 solver ablation in previous sections, we show that least-to-most's lack of backtracking reduces proof accuracy, and lambada's lack of binding propagation restricts goal: is danielle niece of harry? gold reasoning path: least-to-most prompting: q. who is danielle's father? a. dale. q. who is the brother of #1? a. unknown. ▷ planning failure q. danielle can be inferred as the niece of harry. a. yes. ▷ shortcut exploitation lambada: danielle is niece of harry. ├ danielle is a daughter of someone. │ └ danielle is the daughter of dale. └ harry is a brother of someone. └ harry is the brother of kenneth. ∴ proved. ▷ invalid bridging entities danielle dale kevin debra harry morgan brian valerie kenneth figure 7: example from clutrr. the proof is correct if it shows a chain of bridging entities, possibly omitting some. least-to-most exploits shortcut, as it mispredicted the reasoning path but answered the final question correctly. lambada cannot resolve the coreference between bridging entities, leading to disconnected proof. in this section, we directly manipulate the solver algorithm, while the llm portion (single-step statement generation) remains as it is. in the -backtrack setting, the symbolic solver will apply only one decomposition and binding even if there are multiple possible ways, as in figure 2(a) . in the -bindingprop setting, the bindings obtained from previous subgoals are not propagated to subsequent ones, as in figure 2(b) . analogous to lambada, -bindingprop cannot answer gsm8k by design, as there is no way to pass the calculated results to the root goal. the -bindingprop outperforming lambada in deductive benchmarks can again be attributed to negation handling. ## conclusion while backward chaining is a promising direction for structured natural language reasoning, current llm-based approaches like least-to-most and lambada are only incomplete reproductions of backward chaining as they leave out backtracking and binding propagation. to this extent, we build symba directly from the sld resolution algorithm. in symba, a symbolic solver controls the proof, while an llm searches and translates relevant natural language statements into symbolic representations. symba outperforms backward chaining baselines in diverse reasoning tasks including deductive, relational, and arithmetic reasoning. not only does it reach the correct answer more frequently, but also demonstrates improved proof accuracy and efficiency than baselines. from both theoretical and empirical perspectives, we believe that symba significantly extends the horizon of llm-based backward chaining.