Neural Unification for Logic Reasoning over Natural Language (2021)

Abstract: 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., 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. 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 and the source code is released to the research community for reproducibility.

## introduction 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) @xcite . this problem has wide applications in many domains, including problem solving @xcite and question answering @xcite @xcite , and is being actively studied, an extensive reference can be found in @xcite and @xcite . recent approaches, such as ruletaker @xcite , uses transformers @xcite as automated theorem prover over queries, facts and rules expressed in natural language (english). the theorem proving problem is translated into a binary text classification problem, where the transformers model is trained to predict the truth value (true/false) of a textual query q given an input knowledge base κ consisting of textual facts and rules. this class of atp is especially interesting since it does not require the explicit translation of axioms and conjecture to formal logical (e.g first order logic) or probabilistic rules, making it possible to reason on knowledge expressed verbatim. furthermore, these models do not specify an explicit reasoning procedure, but learn to implicitly demonstrate a query from example instances during the learning phase. figure 1 shows an example of an instance of the logic reasoning problem in natural language illustrated in @xcite . the results reported in @xcite demonstrated that state-of-the-art pretrained language models, such as roberta @xcite or bert @xcite , can be fine-tuned with labeled data to achieve 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. this interesting result holds not only for training and test data in the same domain, but also for zero-shot testing on texts in other domains. in this paper we propose an architecture that is able to answer deep queries (having large inference depths) even when it is trained only with shallow queries at depth 1 or 2. our main assumption is that by inducing a neural network to mimic some elements of an explicit general reasoning procedure, e.g. the backward chaining, we can increase the ability of the model to generalize. in particular we focus on mimicking the iterative process in which, at each step, a query is simplified by unifying it with an existing rule to create a new but simpler query for further checking @xcite . in a unification step, when the query matches with the consequent (then clause) of a rule, the antecedent (if clause) of the rule is combined with that query via symbolic substitution to create a new query. for example, for the query "bob is green" shown in figure 1 , the following steps lead to the answer (proof): as we can see in the given example, the query "bob is green" is simplified iteratively with the help of the unification steps and is transformed into a factual query "bob is rough", which is then checked by the fact-checking step via a simple look-up in the knowledge base. these sequences of inference steps are the basis of the famous backward chaining inference in formal logic @xcite illustrated in figure 1 . the main building blocks of such inference methods are the unification and the fact checking algorithms. while backward chaining inference with formal representation can be formulated as a tree search problem @xcite , emulating these algorithms for textual input data using neural networks is still an open research problem, mainly due to the ambiguity in mapping entities and relations expressed in natural language to corresponding mentioning entities and relations in freetext knowledge bases. in the following sections we describe the neural unifier architecture, that mimics the unification and the fact checking algorithms, in order to improve generalisation on answering deep queries. we test our approaches with publicly available datasets where the neural unifier is trained with depth-1 or depth-2 queries, and demonstrate that it can answer queries at higher depths with high accuracy (up to five inference steps). in particular, the proposed approach achieved state-of-the-art results in these benchmark datasets and outperformed the state-ofthe-art algorithms with a significant margin. ## preliminaries and problem definition this section provides a formal problem definition and introduces the main intuition of the approach used for mimicking the backward chaining. the backward chaining algorithm, described extensively in @xcite , is one of the most used algorithms for reasoning with inference rules: it is based on a depth-first strategy to explore the search space, and it generates a proof including a sequence of unification and fact checking operations. an example of execution of this algorithm is shown in figure 1 . let q denote a the query (conjecture) and κ be the knowledge base that consists of a set of rules r and a set of facts f ; in this work we consider all q, r, and f expressed in natural language, where queries, facts and rules can be very simple lexicalizations of logical formulas (e.g, figure 1 ); or they can be paraphrased in a more creative way. experiments with both simple lexicalizations and paraphrases are reported in section 4.3 and section 4.5 respectively. let q n denote as depth-n query that requires at least n inference steps in order to provide an answer. for example, query 1 in figure 1 is a depth-1 query because it requires a unification with r 2 , plus a fact checking step (shown as the success path in figure 1 ). the fact checking function denoted as f can now be formalised as the operation that takes as input a depth-0 query q 0 and returns true if the corresponding fact is present in the given κ, and false otherwise: the unification operation denoted as u can be formalised as the operation that takes as input a query q n and the set of facts and rules κ and provides as output a simpler query q n-1 at depth-(n-1): u(q n , κ) = q n-1 while the application of k unification steps consecutively is denoted as u k (q n , κ) = q n-k , and for the special case where @xmath0: let now assume the existence of a perfect unification operator denoted as u * , that is when it explores the search tree defined by backward chaining, always chooses the branch corresponding to the optimal path (where an optimal path for a query q n is a series of unification operations leading to a query q 0 with the same truth value of q n in n steps). considering a relaxed version of the problem where the queries do not require closed or open word assumption to prove, the truth value of a query q n can therefore be found with n unification steps plus a fact checking operation: f (u n * (q n , κ), κ). with a symbolic representation, the unification and the fact checking operations can be done via explicit mathematical transformations. however, when the input is represented in natural language without an explicit structure, it requires machines to learn these tasks by examples under the presence of language ambiguity. in this work, we propose a neural network architecture called neural unifier (nu) aiming at learning to approximate the function f (u n * (q n , κ), κ) with input expressed in natural language. details about our approach are discussed in the next section. ## training procedure with a slight abuse of notation, in order to simplify the discussion, when we use q to denote the query, we also refer it as a notation of the embedding vector of the query, because a textual query in a neural network is represented as an embedding vector. the main idea behind the approach presented is an architecture composed of two units trained in two separate phases: while the first phase of training is rather intuitive, the second phase teaches the unification unit, starting from a query q n , to transform it into a vector embedding q 0 such that the neural fact checking unit can predict the correct truth value for the query q n . since the fu unit is pretrained to perform fact-checking tasks, the uu unit is forced to produce a query q 0 from a complex query q n so that the answer given by the fu unit is correct, hence figure 2 : a neural unification network consists of a pretrained fact-checking unit and a unification unit. the fact-checking unit is a model trained to check whether an embedding vector of depth-0 query q 0 is true/false given a knowledge base embedding vector c. the unification unit takes an embedding vector q n of a depth-n query and an embedding vector c of the knowledge base as an input. it transforms the input vector q n , thanks to the multi-attention layers, to predict an embedding vector q 0 such that the pretrained fact look-up unit can make a correct prediction of the query's label. ## experiments and results this section discusses experimental settings and results. ## related work while our work is, to the best of our knowledge, the first proposed architecture that emulates backward chaining inference over rule sets and facts expressed in natural language, there are several methods which explore this research area. @xcite introduce the use of transformers to reason over explicitly stated rule sets expressed in natural language; their approach show that transformers are able to solve the problem with high accuracy when the neural network is trained with sufficiently deep reasoning paths, without imposing any structure on the neural reasoning. our main contribution with respect to @xcite consists in emulating, through a neural network, a general reasoning mechanism inspired by the backward chaining algorithm used in formal logic programming. also, our method demonstrate better accuracy for high depth queries, even when trained only with shallow queries. @xcite and @xcite modify the @xcite approach in order to generate proof together with the predicted truth value, these methods however require the explicit knowledge of the proof during the training phase. furthermore, our work is substantially different from the methods that focus on an initial translation of knowledge expressed in textual form to a formal specification, with the aim of applying classic reasoning algorithms, such as the architecture proposed in @xcite for translating text into first order logic formulas. our work is also different from @xcite : the authors present a neural network suitable for reasoning over relationships between two entities of a knowledge base, focusing specifically on predicting additional true facts using only vector representations of existing entities in the knowledge base. other approaches have combined neural and symbolic reasoning methods. one notable example is the neural theorem proving (ntp) presented in @xcite . the authors propose an end-to-end differentiable prover, operating on symbolic representations, for automated completion of a knowledge base: they recursively construct neural networks to prove queries on the knowledge base by following prolog's backward chaining algorithm. additionally, they introduce a differentiable unification operation between vector representations of symbols. @xcite describes an ntp capable of jointly reasoning over kbs and natural language corpora. although the method is versatile, explicit mapping to entities in the kb is required. other relevant methods implement forms of neural reasoning starting from a formal knowledge base, including @xcite , @xcite , and @xcite , or starting from an ontology (which usually define not just the predicates, but also rules) @xcite . conversely, we focus on using transformers both as a fact look-up model (over a knowledge base expressed in natural language), and as a unification unit for transforming queries, which may require many steps of inference, into factual queries that can be answered with the fact look-up model. some early work on simulating the first-order algorithm of unification using neural networks is presented in @xcite . the author shows how error-correction learning algorithm can be used for the purposes of unification. however, this work considers a version of the problem where the knowledge is represented using a formal first order logic language, and uses an explicit mapping of each symbol of the language into a input vector. similarly to our work, @xcite approach the problem of reasoning over natural language emulating unification. they present a model combining neural networks with logic programming for solving multi-hop reasoning tasks over natural language. in the proposed approach the authors extend a prolog prover to use a similarity function over pretrained sentence encoders. a substantial difference with respect to our work is that @xcite approach requires the transformation of natural language text into triples (by using co-occurrences of named entities), and then embedding representations of the symbols in a triple using an encoder. in this paper, we take inspiration from the method presented in @xcite , a recurrent cell that simulates a reasoning step, although the architecture is specially designed for performing visual reasoning given a textual query. our goal is quite different from answering complex multi-hop questions using a corpus of documents as a virtual knowledge base as proposed in the recent work by @xcite , which requires selecting spans from paragraphs of texts. our work can be described as the formalization of a model and a training process that leads the neural network emulate a backward chaining inference process for answering deep queries. ## conclusion and future work in this paper we have shown (in a limited, but not trivial setting) that machines can be trained to perform deep reasoning over language, even if trained only on shallow reasoning. the presented approach performs inference without the need for a translation phase from natural language to a formal specifi-cation, and it obtains high accuracy on the datasets considered. furthermore, with a particular learning architecture that brings learning closer to a deductive argument form, help improving the ability to generalize to deep queries. although this work is a step in the direction of combining the ability of neural networks to emulate reasoning on nonformal data with the explanatory power of a formal demonstration procedure, further work is needed to fill the gaps. in an ideal situation, a machine should perform n inference steps (with explicit reference to the parts of the text concerned) to answer a query with depth n. moreover, the reasoning procedure should be able to reason on any possible textual expression of rules or facts, excluding ambiguous and irrelevant information. with further advances, we may potentially be able to: