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.

通过引入符号性的自上而下求解器，与大型语言模型的集成，SymBa 在多步推理基准测试中（ProofWriter，Birds-Electricity，GSM8k，CLUTRR-TF，ECtHR Article 6）相对于基线算法实现了性能、证明准确性和效率的显著提升。