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{\"{a}}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.

Introduction: Recent advancements in deep learning intensified the long-standing interests in integrating symbolic reasoning with connectionist models BIBREF1 , BIBREF2 , BIBREF3 , BIBREF4 . The attraction of said integration stems from the complementing properties of these systems. Symbolic reasoning models offer interpretability, efficient generalisation from a small number of examples, and the ability to leverage knowledge provided by an expert. However, these systems are unable to handle ambiguous and noisy high-dimensional data such as sensory inputs BIBREF5 . On the other hand, representation learning models exhibit robustness to noise and ambiguity, can learn task-specific representations, and achieve state-of-the-art results on a wide variety of tasks BIBREF6 . However, being universal function approximators, these models require vast amounts of training data and are treated as non-interpretable black boxes. One way of integrating the symbolic and sub-symbolic models is by continuously relaxing discrete operations and implementing them in a connectionist framework. Recent approaches in this direction focused on learning algorithmic behaviour without the explicit symbolic representations of a program BIBREF7 , BIBREF8 , BIBREF9 , BIBREF10 , BIBREF11 , and consequently with it BIBREF12 , BIBREF13 , BIBREF14 , BIBREF15 . In the inductive logic programming setting, two new models, NTP BIBREF0 and Differentiable Inductive Logic Programming ( $\partial $ ILP) BIBREF16 successfully combined the interpretability and data efficiency of a logic programming system with the expressiveness and robustness of neural networks. In this paper, we focus on the NTP model proposed by BIBREF0 . Akin to recent neural-symbolic models, NTP rely on a continuous relaxation of a discrete algorithm, operating over the sub-symbolic representations. In this case, the algorithm is an analogue to Prolog's backward chaining with a relaxed unification operator. The backward chaining algorithm constructs neural networks, which model continuously relaxed proof paths using sub-symbolic representations. These representations are learned end-to-end by maximising the proof scores of facts in the KB, while minimising the score of facts not in the KB, in a link prediction setting BIBREF17 . However, while the symbolic unification checks whether two terms can represent the same structure, the relaxed unification measures the similarity between their sub-symbolic representations. This continuous relaxation is at the crux of NTP' inability to scale to large datasets. During both training and inference, NTP need to compute all possible proof trees needed for proving a query, relying on the continuous unification of the query with all the rules and facts in the KB. This procedure quickly becomes infeasible for large datasets, as the number of nodes of the resulting computation graph grows exponentially. Our insight is that we can radically reduce the computational complexity of inference and learning by generating only the most promising proof paths. In particular, we show that the problem of finding the facts in the KB that best explain a query can be reduced to a $k$ -nearest neighbour problem, for which efficient exact and approximate solutions exist BIBREF18 . This enables us to apply NTP to previously unreachable real-world datasets, such as WordNet.

Question: What are proof paths?
Answer: A sequence of logical statements represented in a computational graph