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）相对于基线算法实现了性能、证明准确性和效率的显著提升。

SymBa：用于多步自然语言推理的符号式向后推理

SymBa: Symbolic Backward Chaining for Multi-step Natural Language  Reasoning

Automated Theorem Proving (ATP) deals with the development of computer
programs being able to show that some conjectures (queries) are a logical
consequence of a set of axioms (facts and rules). There exists several
successful ATPs where conjectures and axioms are formally provided (e.g.
formalised as First Order Logic formulas). Recent approaches, such as (Clark et
al., 2020), have proposed transformer-based architectures for deriving
conjectures given axioms expressed in natural language (English). The
conjecture is verified through a binary text classifier, where the transformers
model is trained to predict the truth value of a conjecture given the axioms.
The RuleTaker approach of (Clark et al., 2020) achieves appealing results both
in terms of accuracy and in the ability to generalize, showing that when the
model is trained with deep enough queries (at least 3 inference steps), the
transformers are able to correctly answer the majority of queries (97.6%) that
require up to 5 inference steps. In this work we propose a new architecture,
namely the Neural Unifier, and a relative training procedure, which achieves
state-of-the-art results in term of generalisation, showing that mimicking a
well-known inference procedure, the backward chaining, it is possible to answer
deep queries even when the model is trained only on shallow ones. The approach
is demonstrated in experiments using a diverse set of benchmark data.

本文提出了一种新的架构 —— 神经单元器，并提出了相应的训练过程，实现了最先进的推理结果，通过模拟一种众所周知的推理过程 —— 向后链接，即使模型只在浅层次的数据上进行训练，也能回答深度问题，并通过使用各种基准数据集进行实验。

基于神经网络的自然语言逻辑推理统一化

Neural Unification for Logic Reasoning over Natural Language

With the growth of the Semantic Web in size and importance, more and more
knowledge is stored in machine-readable formats such as the Web Ontology
Language OWL. This paper outlines common approaches for efficient reasoning on
large-scale data consisting of billions ($10^9$) of triples. Therefore, OWL and
its sublanguages, as well as forward and backward chaining techniques are
presented. The WebPIE reasoner is discussed in detail as an example for forward
chaining using MapReduce for materialisation. Moreover, the QueryPIE reasoner
is presented as a backward chaining/hybrid approach which uses query rewriting.
Furthermore, an overview on other reasoners is given such as OWLIM and TrOWL.

本文介绍了在 Semantic Web 环境下，如何有效地处理数十亿组三元组数据的一些方法，包括利用 OWL 和其子语言，以及前向和后向链接技术。还详细讨论了 WebPIE reasoner，QueryPIE reasoner，OWLIM 和 TrOWL 等其他推理器。