End-to-end Differentiable Proving

By Tim Rocktaschel, Sebastian Riedel. 2017

460 citations recorded by the source corpus.

We introduce neural networks for end-to-end differentiable proving of queries to knowledge bases by operating on dense vector representations of symbols. These neural networks are constructed recursively by taking inspiration from the backward chaining algorithm as used in Prolog. Specifically, we replace symbolic unification with a differentiable computation on vector representations of symbols using a radial basis function kernel, thereby combining symbolic reasoning with learning subsymbolic vector representations. By using gradient descent, the resulting neural network can be trained to infer facts from a given incomplete knowledge base. It learns to (i) place representations of similar symbols in close proximity in a vector space, (ii) make use of such similarities to prove queries, (iii) induce logical rules, and (iv) use provided and induced logical rules for multi-hop reasoning. We demonstrate that this architecture outperforms ComplEx, a state-of-the-art neural link prediction model, on three out of four benchmark knowledge bases while at the same time inducing interpretable function-free first-order logic rules.

Subfields: Artificial Intelligence, Natural Language Processing

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Natural Language Processing

Citations in the corpus

A Survey of Machine Learning for Big Code and Naturalness (2017, background): “One approach, taken by several authors [9, 127, 165, 171], is to relax formal systems into probabilistic.”
FEVER: a Large-scale Dataset for Fact Extraction and VERification (2018, background): “…similar to natural logic inference (Angeli and Manning, 2014) can be applied, where a knowledge base/graph is constructed by reading the textual sources and then a reasoning process over the claim is applied, possibly using recent advances in neural theorem proving (Rockt¨aschel and Riedel, 2017).”
Neural Logic Machines (2019, background): “The key of Rocktäschel & Riedel (2017) and Campero et al. (2018) is to learn subsymbolic embeddings of entities and predicates for efﬁcient KB completion, which differs from our focus.”
Planning chemical syntheses with deep neural networks and symbolic AI (2017, background): “[47] This might be solvable by stronger, but slower reasoning algorithms[41, 48] Another important challenge to be solved is stereochemistry.”
Constructing Datasets for Multi-hop Reading Comprehension Across Documents (2017, background): “Another approach is the Neural Theorem Prover (Rockt¨aschel and Riedel, 2017), which uses dense rule and symbol embeddings to learn a differentiable backward chaining algorithm.”
Integrating Learning and Reasoning with Deep Logic Models (2019, methodology): “A Neural Theorem Prover (NTP) [27, 28] is an end-to-end differentiable prover based on the Prolog’s backward chaining algorithm.”
NLProlog: Reasoning with Weak Unification for Question Answering in Natural Language (2019, methodology): “An area in which neural multi-hop reasoning models have been investigated is Knowledge Base Completion (KBC) (Das et al., 2016; Cohen, 2016; Neelakantan et al., 2015; Rocktäschel and Riedel, 2017; Das et al., 2017; Evans and Grefenstette, 2018).”
Neuro-Symbolic = Neural + Logical + Probabilistic (2019, methodology): “, 2018] X X Propositional logic ∂ILP [Evans and Grefenstette, 2018] Datalog Neural Theorem Prover [Rocktäschel and Riedel, 2017] Clausal logic TensorLog [Cohen et al.”
A Survey on Knowledge Graphs: Representation, Acquisition, and Applications (2020, background): “m induction and axiom injection. The combination of neural and symbolic models has also attracted increasing attention to do rule-based reasoning in an end-to-end manner. Neural Theorem Provers (NTP) [82] learns logical rules for multi-hop reasoning which utilizes radial basis function kernel for di”
Unsupervised Grounding of Plannable First-Order Logic Representation from Images (2019, background): “Neural theorem proving systems (Rocktäschel and Riedel 2017; Sourek et al. 2018; Manhaeve et al. 2018) learn to reason about logical relations.”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, background): “Their performances have been improved by machine learning [30, 3, 12, 21, 33, 24, 15].”
Neurosymbolic AI: the 3rd wave (2020, unknown): “…and d’Avila Garcez 2016) takes another step towards integration by using a differentiable many-valued logic in the loss function of a neural network; (Minervini et al. 2020; Rocktäschel and Riedel 2017) proposes to perform differentiable unification and theorem proving inside the neural network.”
RelNN: A Deep Neural Model for Relational Learning (2017, background): “Examples of these works include path-constrained random walks (e.g., (Lao and Cohen 2010; Lao, Mitchell, and Cohen 2011)), and several hybrid approaches (e.g., (Das et al. 2017; Rockt¨aschel and Riedel 2017; Yang, Yang, and Cohen 2017; Wang, Shi, and Yeung 2017)).”
Neural Guided Constraint Logic Programming for Program Synthesis (2018, unknown): “ilarities with our contribution. For example, [21] uses constraint-based solver to sample terms in order to complete a program sketch, but is not concerned with synthesizing entire programs. Further, [22] implements differentiable logic programming to do fuzzy reasoning and induce soft inference rul”