We present an approach for systematic reasoning that produces human
interpretable proof trees grounded in a factbase. Our solution evokes classic
Prolog-based inference engines, where we replace handcrafted rules through a
combination of neural language modeling, guided generation, and semiparametric
dense retrieval. This novel reasoning engine, NELLIE, dynamically instantiates
interpretable inference rules that capture and score entailment
(de)compositions over natural language statements. NELLIE shows competitive
performance on scientific QA datasets requiring structured explanations over
multiple facts while fully grounding justification proofs in verified
knowledge.

提出一种系统性推理方法，它可以生成基于事实库的人类可解释证明树。新方法使用神经语言建模、引导生成和半参数密集检索来替换手工制定的规则，从而动态实例化可解释推理规则，并在多个事实上得分。经验证的知识证明完全落实在科学 QA 数据集上。

神经符号专家系统中可解释推理规则的动态生成

Dynamic Generation of Interpretable Inference Rules in a Neuro-Symbolic Expert System

In this work we propose a multi-valued extension of logic programs under the
stable models semantics where each true atom in a model is associated with a
set of justifications, in a similar spirit than a set of proof trees. The main
contribution of this paper is that we capture justifications into an algebra of
truth values with three internal operations: an addition '+' representing
alternative justifications for a formula, a commutative product '*'
representing joint interaction of causes and a non-commutative product '.'
acting as a concatenation or proof constructor. Using this multi-valued
semantics, we obtain a one-to-one correspondence between the syntactic proof
tree of a standard (non-causal) logic program and the interpretation of each
true atom in a model. Furthermore, thanks to this algebraic characterization we
can detect semantic properties like redundancy and relevance of the obtained
justifications. We also identify a lattice-based characterization of this
algebra, defining a direct consequences operator, proving its continuity and
that its least fix point can be computed after a finite number of iterations.
Finally, we define the concept of causal stable model by introducing an
analogous transformation to Gelfond and Lifschitz's program reduct.

本文提出了一种多值扩展的逻辑程序，基于可靠模型语义，其中模型中的每个真实原子都与一组证明关联，在一个证明树的集合中类似，我们将证明捕捉到一个真值的代数中，该代数具有三个内部操作：加号表示公式的替代证明，可交换乘积表示导致的联合交互以及非交换积表示证明构造器。使用这种多值语义，我们得到了标准（非因果）逻辑程序的语法证明树与模型中每个真实原子的解释之间的一一对应关系，并且由于这种代数特征，我们可以检测到获得的证明的冗余性和相关性。我们还确定了此代数的基于格的特征，定义了直接后果算子，证明了其连续性，并证明其最小修复点可以在有限次迭代后计算。最后，我们通过引入类似于 Gelfond 和 Lifschitz 的程序削减的变换来定义因果稳定模型的概念。