Towards Neural Theorem Proving at Scale

Abstract

Neural models combining representation learning and reasoning in an end-to-end trainable manner are receiving increasing interest. However, their use is severely limited by their computational complexity, which renders them unusable on real world datasets. We focus on the Neural Theorem Prover (NTP) model proposed by Rockt{ä}schel and Riedel (2017), a continuous relaxation of the Prolog backward chaining algorithm where unification between terms is replaced by the similarity between their embedding representations. For answering a given query, this model needs to consider all possible proof paths, and then aggregate results - this quickly becomes infeasible even for small Knowledge Bases (KBs). We observe that we can accurately approximate the inference process in this model by considering only proof paths associated with the highest proof scores. This enables inference and learning on previously impracticable KBs.

arXiv commentFederated Artificial Intelligence Meeting (FAIM) Workshop on Neural Abstract Machines & Program Induction v2

References in corpus (4)

• Deep Learning: A Critical Appraisal
• End-to-End Differentiable Proving
• TerpreT: A Probabilistic Programming Language for Program Induction
• Approximate Nearest Neighbor Search on High Dimensional Data --- Experiments, Analyses, and Improvement (v1.0)

Cited by in corpus (8)

• Beyond Graph Neural Networks with Lifted Relational Neural Networks
• Learn to Explain Efficiently via Neural Logic Inductive Learning
• Neural Theorem Provers Do Not Learn Rules Without Exploration
• From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
• IterefinE: Iterative KG Refinement Embeddings using Symbolic Knowledge
• Program synthesis performance constrained by non-linear spatial relations in Synthetic Visual Reasoning Test
• Semantic Reasoning with Differentiable Graph Transformations
• RuDaS: Synthetic Datasets for Rule Learning and Evaluation Tools