Large Language Models (LLMs) have recently demonstrated remarkable reasoning ability as in Chain-of-thought prompting, but faithful multi-step reasoning remains a challenge. We specifically focus on backward chaining, where the query is recursively decomposed using logical rules until proven. To address the limitations of current backward chaining implementations, we propose SymBa (Symbolic Backward Chaining). In SymBa, the symbolic top-down solver controls the entire proof process and the LLM is called to generate a single reasoning step only when the solver encounters a dead end. By this novel solver-LLM integration, while being able to produce an interpretable, structured proof, SymBa achieves significant improvement in performance, proof faithfulness, and efficiency in diverse multi-step reasoning benchmarks (ProofWriter, Birds-Electricity, GSM8k, CLUTRR-TF, ECtHR Article 6) compared to backward chaining baselines.

翻译：大语言模型（LLMs）近期在思维链提示中展现出显著的推理能力，但可信的多步推理仍是一大挑战。我们聚焦于反向链方法，该方法通过逻辑规则递归分解查询直至证明成立。为解决现有反向链实现的局限性，我们提出SymBa（符号反向链）。在SymBa中，符号化的自顶向下求解器控制整个证明过程，而LLM仅在求解器遇到死胡同时被调用来生成单步推理。通过这种新颖的求解器-LLM集成方式，SymBa既能生成可解释的结构化证明，又在多样化的多步推理基准测试（ProofWriter、Birds-Electricity、GSM8k、CLUTRR-TF、ECtHR第6条）中实现了相较于反向链基线方法在性能、证明可信度及效率方面的显著提升。