Computer Science-2021.gz:143437
Computer Science
a8330be474db6d94435f9b31bbc84f7a2b9fb92c
Natural Language Inference using Neural Network and Tableau Method

Natural language inference (NLI) is the task of identifying the inferential relation between a text pair. Neural-based approaches recently achieved high performance on the NLI task, but they cannot explain their reasoning processes. On the other hand, symbolic approaches have an advantage that the reasoning process is understandable to humans. This paper proposes a method to integrate a neural NLI model and a tableau proof system, the latter of which explains the reasoning processes. The standard tableau method consists of decomposing logical formulas by applying inferential rules, and checking whether or not there exists a valuation that satisfies the given constraints. Unlike the standard tableau method, our method adopts not logical formulas but dependency structures as its ingredients and uses a neural NLI model for the latter process. In order to analyze the behavior of a neural NLI model, we conducted an experiment on the neural NLI model alone and the proposed method using the SNLI corpus.


Introduction
Natural language inference (NLI) is the task of identifying the inferential relation between a text pair: premise and hypothesis. If a hypothesis can be inferred from a premise using logical and common sense knowledge, it is judged as entailment; if they are incompatible, it is judged as contradiction; and if neither of them is the case, it is judged as neutral. It is expected to be used in a wide range of fields such as question answering, information retrieval and text summarization.
In recent years, neural-based approaches have achieved high performance on the NLI task. For example, Chen et al. (2017) proposed a model using word embedding and bidirectional LSTM (Hochreiter and Schmidhuber, 1997). Although the model is simple, it achieves a high accuracy in experiments using the SNLI corpus (Bowman et al., 2015). On the other hand, neural-based approaches have a problem that the models cannot explain the reasoning processes that lead to the judgment. The model is a black box, and it is difficult to analyze what kind of inference has been performed. In addition, Gururangan et al. (2018) showed that NLI datasets such as the SNLI corpus and MultiNLI corpus (Williams et al., 2018) have a hidden bias in that inferential relations can be determined only from a hypothesis, and pointed out the risk that neural models are simply identifying inferential relations based on the biases.
On the other hand, symbolic approaches to the NLI task have been proposed. These approaches have the advantage that the reasoning process leading to the result is understandable to humans, unlike the neural model approach. In addition, symbolic manipulations in these approaches are generally founded on a formal logic or linguistic analyses, which allow us to understand the reasoning processes.
In this paper, we propose a method to add to the neural NLI model the ability of the symbolic manipulation approach that makes the reasoning process explicit. Our approach only assumes that an NLI model takes a pair of premise and hypothesis and outputs inferential relation. That is, our ap-proach can be applied to any neural NLI model. Our method combines a neural NLI model and a tableau proof system. The standard tableau method consists of decomposing logical formulas by applying inference rules, and checking whether or not there exists a valuation that satisfies the given constraints. Our method uses a neural NLI model for the latter process. Unlike the standard tableau method, our approach adopts not logical formulas but dependency structures as its ingredients. This characteristic enables us to integrate a neural NLI model into a symbolic proof system.

Tableau Method
In this section, we describe the standard tableau method, which is the basis of our proposed method. The tableau method is a procedure for proving whether or not, given a set of pairs of logical formulas and truth values (called entries in the following), there exists a valuation that assigns a truth value to each logical formula in the set. The relation between NLI and the tableau method can be summarized as follows: • A premise and a hypothesis are in a contradiction relation when the procedure proves that there is no valuation such that both the premise and the hypothesis are true.
• When the procedure proves that there is no valuation where the premise is true and the hypothesis is false, it implies that if the premise is true, then the hypothesis is also true, that is the premise entails the hypothesis.
• If neither can be proved, it means that the neutral relation holds between the premise and the hypothesis.
The tableau method constructs a tree structure, called a tableau, for a given set of entries E. Each node in the tableau is labeled with an entry [X : A]. This entry represents the constraint that the logical formula A must take X as its truth value. The initial tableau consists of nodes labeled with the elements of E. The tableau is derived by repeatedly applying the tableau rules to the nodes. By applying the tableau rules, the constraints expressed by the entries are decomposed into constraints on subformulas. The decomposed constraints are then added to the tableau as new nodes. Branches in tableau mean that there are multiple cases for possible valuation. When nodes on the path from the root to a leaf of a tableau have the labels [T : A] and [F : A] (where T and F denote true and false, respectively), we say that this path is closed. If all the paths in a tableau are closed, we say that the tableau is closed. The fact that the tableau is closed means that there is no valuation that satisfies the constraints represented by E.

Proposed Method
In this section, we propose an NLI system that combines a tableau method based on dependency structures and a neural model-based judgment of closed tableaux. Our system performs the following steps: Dependency parsing Convert the premise and hypothesis texts into dependency structures D P and D H , respectively.
Inference based on the tableau method For the dependency structures D P and D H , our system constructs two tableaux. The one proves entailment relation (a tableau derived from [T : D P ], [F : D H ]) and the other proves contradiction relation (a tableau derived from [T : D P ], [T : D H ]). In the following, we refer to these tableaux as entailment tableau and contradiction tableau, respectively.
Checking closed tableau Determine whether or not the entailment and contradiction tableaux are closed using a neural NLI model.

Dependency parsing
Our proposed method uses a neural NLI model to determine the closed tableau, and the model takes natural language sentences as input. To make this possible, we use not logical formulas but dependency structure as an entry in the tableau. In this step, the premise and hypothesis sentences are converted into dependency structures. We adopt Universal Dependencies (UD) (McDonald et al., 2013) as the dependency formalism. Any UD-based dependency parser is available for this step. Figure 1 shows an example of dependency structure.
Either Smith or Anderson signed the contract root nsubj cc:preconj conj cc obj det Figure 1: The Dependency structure of "Either Smith or Anderson signed the contract."

Inference based on the tableau method
In this section, we explain the tableau method based on the dependency structure.

Tableau rules
Each tableau is derived by applying tableau rules as in the standard method. All tableau rules in the proposed method are in the following form: where P, C 1,1 , . . . , C 1,n 1 , . . . , C m,1 , . . . , C m,nm are pairs of truth values and dependency structure patterns. The dependency structure patterns contain variables, and each variable is bound to a matched dependency structure or a matched dependency structure sequence. Examples of tableau rules are shown in Figure 2. If P matches a node N on a path of the tableau, the procedure adds new m branches ⟨σ(C 1,1 ) . . . σ(C 1,n 1 )⟩, . . ., ⟨σ(C m,1 ) . . . σ(C m,nm )⟩ as children of the leaves of the path. Here, σ is the function that substitutes the variables with the bounded elements.
The tableau rules decompose the constraints expressed by the source node. For example, applying the rule on the left of Figure 2 to the node with the label [T: Either Smith or Anderson signed the contract.] will add two nodes to the end of the path (the tableau leaf). The added nodes are labeled with [T: Smith signed the contract.] and [T: Anderson singed the contract.]. The constraints expressed by the two newly added nodes are equivalent to the constraints of the original nodes. For nodes to which the tableau rule has been applied, there is no need to apply a new operation, because the constraint is already expressed by the node from which it was derived. Therefore, it is not necessary to handle the original node anymore. Our proposed method sets a flag for each node to distinguish whether the tableau rule is applied or not. The flagged node is not used for any further operations (application of the rule  Figure 3 shows the entailment tableau for the premise "Either Smith or Anderson signed the contract." and the hypothesis "If Smith didn't sign the contract, Anderson made an agreement.".

Judgment of closed tableau
In standard tableau methods, a closed path is defined by the existence of entries on the path that differ only in their truth values. In addition, our proposed method introduces another type of definition of a closed path, which is based on a neural NLI model. An NLI model takes a premise P and a hypothesis H as input and returns one of the following classes: entailment, neutral, or contradiction. In the following, we write Rel M (P, H) for the class determined by the model M. When two nodes are labeled with [X 1 : D 1 ] and [X 2 : D 2 ], the following two situations are those in which it is not possible to assign a truth value.
Here, sen(D) is the sentence corresponding to the dependency structure D. In the proposed method, we define a path to be closed when there are two nodes on the path that satisfy either of the two conditions. For example, the tableau in Figure 3 has a path ( 1 2 3 4 5 6 ) that contains 6 [T: Smith It's because 5 and 6 are same dependency structure.
In determining the closed tableau, only those nodes that have not been given the flag described in the previous section need to be considered.

Experiment
In order to analyze the behavior of a neural NLI model from the viewpoint of making the reasoning process explicit, we conducted an experiment. 1

Dataset
We used the SNLI corpus (Bowman et al., 2015) as the dataset. We used the standard data split, that is, 549,367 samples for training data, 9842 for development data, and 9824 for test data. 2

Dependency parsing
We used Udify (Kondratyuk and Straka, 2019) which is a multilingual dependency parser using BERT (Devlin et al., 2019). It outputs the UD-based dependency structures.

Neural NLI model
We used ESIM (Chen et al., 2017) which is based on LSTM. 3 The parameters of ESIM was estimated using the training and development data.

Tableau rules
We have created 32 tableau rules that correspond to the rules of the standard tableau method for propositional logic. The rules can be classified into four categories: conjunction, disjunction, negation, and conditional. The rules for conjunction and disjunction can handle not only the coordinated structures of sentences but also the ones for core arguments (subject, object, etc.) of UD. The tableau rules are shown in Appendix A.

Evaluation
The distributions of the derived tableau sizes (defined as number of entries) are shown in Figure 4 and 5. Our tableau system could decompose the sentences for 660 of 9824 test samples.
We used the standard metrics for performance evaluation. One notable point is that, when both the entailment contradiction tableau were closed, they were classified as errors. The F 1 value is the harmonic mean of the recall and precision defined below:  Here, TP A is the number of samples which the correct answer and prediction are class A, True A is the number of samples which the correct answer are class A, and Positive A is the number of samples which the prediction are class A. Table 1 and 2 show the accuracy, recall, precision, and F 1 value for each class for the 660 samples where some tableau rule was applied. The micro accuracy of the proposed method was 68.64%, the percentage classified as an error class was 6.97%, and the micro accuracy of the neural NLI model was 86.82%.
The proposed method has a tendency to erroneously predict contradiction relation in comparison with the method using only neural models. In the next section, we analyze the reason for this.

Error analysis
To investigate why the proposed method failed to identify the inferential relations, we checked the tableaux constructed for such samples. In the fol-  lowing, we will use the following actual samples: Premise: Four people and a baby are crossing the street at a crosswalk.
Hypothesis: People and a baby crossing the street.

Relation: Entailment
The contradiction tableau for this sample is shown in Figure 6. Because the correct label of this sample is entailment, the tableau should not be closed. However, the tableau is closed due to the fact that Rel ESIM (sen( 3 ), sen( 6 )) = contradiction.
As pointed out in (Bowman et al., 2015), there is a certain indeterminacy in the inferential relation between sen( 3 ) and sen( 6 ). The inferential relation may depend on whether the entities which the noun phrases refer to are identical or not. The inferential relation between sen( 3 ) and sen( 6 ) is "contradiction" if "Four people" and "A baby" refer to the same entity, but "neutral" if they do not refer to the same entity. In the 38 samples where the contradiction tableau should not be closed in the development dataset, the contradiction tableaux of 21 samples were incorrectly closed by the same reason. The point to be noted here is that we were able to capture this fact using the tableaux constructed by our method.

Related Work
Our proposed method adopts an approach inspired by Natural Logic (Lakoff, 1970) that performs inferences based on syntactic structures. This section gives an overview of previous Natural Logic-based methods and compares them with ours.
Natural Logic-based systems can be classified into the following two types: • Transition-based method

• Proof-based method
In the transition-based approach, a premise is converted into a hypothesis using some operations. Bar-Haim et al. (2007) proposed entailment-preserving rules that transform dependency structures. Mac-Cartney and Manning (2008) proposed a system called NatLog which is based on an extended version of monotonicity calculus (MacCartney and Manning, 2009). These methods are similar to ours in terms of directly handling natural language sentences. However, it is unclear how to integrate neural NLI models into them. Furthermore, transitionbased methods cannot handle multi-premise problems, unlike ours.
Abzianidze (2017) proposed a tableau proof system called LangPro. Hu et al. (2020) developed a proof system called MonaLog, which is based on monotonicity reasoning. These systems use semantic representations similar but not identical to natural language sentences. That is, it is impossible to integrate a neural NLI model with their proof system, unlike ours.

Conclusion
In this paper, we proposed an NLI system using the tableau method and a neural model. In this reported experiment, we trained the neural model using the premises and hypotheses of the dataset as they were. On the other hand, as another type of training, we will explore how to use decomposed premises and hypotheses according to the proposed tableau method as training examples. In addition we will enrich the tableau rules and support multiple languages in future research.   Figure 7 shows all rules that we created. Here, V is a variable matching any dependency structure whose head word is a verb, C i is a variable matching any dependency structure, and, X is a dependency relation in {nsubj, csubj, obj, iobj, ccomp, xcomp}.