Learning as Abduction: Trainable Natural Logic Theorem Prover for Natural Language Inference (2020)

Abstract: Tackling Natural Language Inference with a logic-based method is becoming less and less common. While this might have been counterintuitive several decades ago, nowadays it seems pretty obvious. The main reasons for such a conception are that (a) logic-based methods are usually brittle when it comes to processing wide-coverage texts, and (b) instead of automatically learning from data, they require much of manual effort for development. We make a step towards to overcome such shortcomings by modeling learning from data as abduction: reversing a theorem-proving procedure to abduce semantic relations that serve as the best explanation for the gold label of an inference problem. In other words, instead of proving sentence-level inference relations with the help of lexical relations, the lexical relations are proved taking into account the sentence-level inference relations. We implement the learning method in a tableau theorem prover for natural language and show that it improves the performance of the theorem prover on the SICK dataset by 1.4% while still maintaining high precision (>94%). The obtained results are competitive with the state of the art among logic-based systems.

## introduction natural language inference (nli) is a wellestablished task for measuring intelligent systems' capacity of natural language understanding @xcite . to improve and better evaluate the systems on the nli task, many annotated nli datasets are prepared and used for training and evaluating nlp models. generally speaking, an nli dataset is a set of natural language sentence pairs, called premise-hypothesis pairs, that are annotated by crowd workers with one of three inference labels (entailment, contradiction, and neutral), representing a semantic relation from a premise to a hypothesis. currently, the state-of-the-art systems in nli are exclusively based on deep learning (dl). one of the reasons for this is that dl-based systems can eagerly learn from task-related data and also take an advantage form high-quality pre-trained word embeddings. the training phase helps them to obtain competitive scores on the in-domain test part. on the other hand, logic-based systems are becoming less favored for nli since it is hard to scale them up for reasoning with wide-coverage sentences. despite some rare exceptions @xcite , it is notoriously hard to effectively and efficiently train logic-based systems on nli datasets. although dl-based systems are more robust than logic-based ones, the latter systems offer unique virtues such as a transparent reasoning procedure and reasoning with multiple premises. an opaque decision procedure of dl-based systems makes it difficult to estimate a share of knowledge from what was learned by the systems, because not all what is learned is knowledge. behind high performance of dl-based systems on particular nli datasets, one might miss the systems' inability of generalization @xcite or the exploitation of annotation artefacts @xcite . in this paper, we are not comparing logic-and dl-based approaches with respect to the nli task. rather, we are proposing a learning method which demonstrates how a logic-based nli system can be trained on nli dataset, the aspect in which dl approaches to nli significantly outperform symbolic approaches. the proposed learning algorithm is inspired by abductive reasoning, which is often referred to as inference to the best explanation. following the abduction, the algorithm allows learning those semantic relations over words and short phrases that best explain gold inference labels of nli problems (see figure 1 ). in this way, the current work contributes to automated knowledge acquisition from data, which is considered as a major issue in nli @xcite . the paper makes contributions along two lines: (a) describing how learning as abduction enables a trainable theorem prover for nli, and (b) implementing the algorithm and evaluating its effectiveness. the original aspect of the research is the conceptual simplicity of the learning algorithm. in particular, the standard workflow of the logicbased theorem prover is reversed: instead of proving sentence-level inference relations with the help of lexical relations, the lexical relations are proved taking into account the sentence-level inference relations. throughout the paper we answer the following research questions: q1 what is a computationally feasible learning method that allows training the natural language theorem prover on nli problems? q2 how can learning pseudo-knowledge be avoided? q3 can the learned knowledge replace the lexical knowledge database like wordnet? q4 to what extent the learned knowledge boosts the performance of the prover? the rest of the paper briefly introduces the natural language theorem prover (section 2), describes the new learning algorithm motivated by abduction (section 3), outlines settings of experiments (section 4), reports and analyzes results of the experiments (section 5 and section 6), overviews related work and compares it with the current one (section 7), and finally, concludes the paper by answering the research questions (section 8). ## natural language theorem prover for our experiments, we employ a natural language theorem prover, called langpro (abzianidze, 2017a), which is an implementation of natural tableau-an analytic tableau system for natural logic @xcite ). an inference procedure is more central to natural tableau and its prover than it is usually for other logic-based nli systems @xcite , which first derives meaning representations and then uses a proof engine for inference. the inference in natural tableau not only helps to prove semantic relations but also further expands semantics of logical forms (e.g., shifting from higher to lower-order terms). this makes it difficult to separate inference and semantic representations in natural tableau. its central role of inference makes langpro a suitable candidate for the data-driven learning experiment based on automated theorem proving. the logic behind natural tableau and the prover is a higher-order logic (aka simple type theory) which also acts as a version of natural logic @xcite . the λ-terms, given below with their corresponding sentences, represent logical forms of the natural logic. a hedgehog is cradled by a boy (1) a hedgehog be (λx. a boy (λy. by y cradle x)) (1a) a person holds an animal (2) a person (λx. an animal (λy. hold y x)) (2a) most dogs which jumped also barked loud (3) most (which jump dog) also (loud bark) in addition to the lexical terms, the terms employ only variables and constants. therefore, common logical connectives (e.g., ∧, ¬) and quantifiers (e.g., ∃, ∀) are not part of the formal language. the terms are built using the λ abstraction and function application. 1 the role of variables and λ is to access and fill certain argument positions and control scope. variables and λ are mainly used for terms with arity two or more, like cradle and hold. @xcite showed that the terms can be automatically obtained from the derivations of combinatory cat- the tableau starts with (1a) being true and (2a) false, expressed by the entries 1 and 2 . but what are the meanings of 1 and 2 ? to flesh out their meanings, inference rules are applied to the entries. in particular, 1 produces 3 and 4 with the help of the rule (∃ t ), which says: if an a does b is true, then there is some entity, let's name it n, which is a and does b. 2 further applying (∃ t ) to 4 introduces 5 and 6 . 7 is obtained from 6 with the help of (pss), which paraphrases passive constructions with any truth sign (x) as active constructions. so far, the prover managed to fold out semantics of 1 : there are b and h who are a boy 5 and a hedgehog 2 obtaining 4 from 1 additionally requires application of (λ<) and the rule for auxiliaries that will treat be as an identity function and discard it. in principle, it is also necessary to verify the nli problem for contradiction. in that case, the tableau proof starts with 1 and 2 being true. if neither entailment nor contradiction is proved, the problem is classified as neutral. ## experiments we design experiments to evaluate learning as abduction for nli. first, we implement the abductive learning for langpro @xcite . the implementation takes advantage of prolog's virtue of satisfying goals in the forward and backward fashion and uses it to apply closure rules in backwards during the search for b-sets. this leaves the inventory of tableau rules intact. 7 the workflow of the abductive learning is depicted in figure 4 . searching for the best t-set is an np-hard problem. 8 to make the implementation efficient (q1), we significantly reduce a space of t-sets by considering only those t-sets that coincide with b-sets. in other words, we require existence of the shared b-sets across all open branches. the example in figure 3 to test the learning algorithm, we use the sick dataset @xcite for three reasons. first, compositional lexical knowledge involved in the dataset is suitable for the abductive learning. second, it is large enough (up to 10k problems) to support learning from a training part and eval- unsolved problems all problems abductive inference with all filters langpro sentence consistent shape of terms comparable terms kb consistent information amount impact on accuracy learned relations incorporate learned relations and restart the learning phase if new relations were learned calculate impact based on relevant problems 3 -1 2 2 7 langpro reverse proving 4 number of terms uation on an unseen part. third, sick has been used for evaluating logic-based nli systems, including langpro, and this allows comparison to the existing results. our data partition follows the semeval-14 task-1 (marelli et al., 2014a): sick-train&trial (4500 + 500 problems) is a training data and sick-test (4927 problems) a hidden test data. the error analysis is conducted only on the training data. to choose optimal learning parameters (see subsection 3.3) and measure impact of the filters and knowledge resources, we run the learning algorithm with stratified three-fold cross-validation (cv) on the training data. the stratified version is due to a skewed distribution of gold labels in sick. we opt for three-fold cv as it better reflects 1:1 ratio between sick-train&trial and -test sizes. logic-based nli systems using logical forms from syntactic trees often employ output of several parsers to increase the quality of logical forms @xcite @xcite . in our cv experiments, we use the re-banked c&c ccg parser @xcite . the ensemble of parsers, used for evaluation on sick-test, additionally includes easy-ccg @xcite and depccg @xcite with standard models. ## results initially we run langpro with wordnet @xcite relations and all filters enabled (see subsection 3.3). the results in we conduct ablation experiments to verify the contributions of the filters. we also tested whether the learned relations can compensate for the wordnet relations (q3). the results show that wordnet relations still contribute to high accuracy as their exclusion drops accuracy by 2.44%. abzianidze (2015) uses hand-crafted kb of ∼30 lexical relations collected from sick-train&trial. when this kb is add, only six more problems on average (0.36%) is classified correctly. to answer (q4), we compare langpro with and without abduction on unseen sick-test. the results in ## error analysis in total 312 relations were learned with abduction from sick-train&trial based on a single parser. despite having a sequence of filters, substantial pseudo-knowledge (29%) still leaked during the learning. one of the main reasons for this is a strong learning bias towards minimal explanations which often leads to ignoring context. this way, from sk-9624 . . . is looking toward the stars. . . entailing . . . is looking toward the sky. . . , star sky relation was wrongly learned. additionally, learning in the dark at night is preferred to currently learned in at. this is a common drawback of pure logic-based approaches which is induced by a general principle, called a rule of replacement, which licenses replacement of equivalent terms. a number of incorrect learned relations are conditioned by noisy gold labels of sick @xcite . dog bull dog was learned due to sk-2608, a monkey is brushing the dog contradicting the monkey is not brushing a bull dog; person man is due to sk-4680, someone is drilling a hole in a strip of wood with a power drill entailing a man is correct (26.6%) wrong (28.8%) add x to y | remove x from y the blonde girl | a little girl a x lie down | a x run around aim a gun draw a gun perform acrobatics perform a trick ride in x | get out of x reversed (28.9%) contextual (15.7%) have lunch eat hang on a cord hang on a rope look at x stare at x man in a cap man in a hat prepare some food prepare a meal in the dark at night ## related work & comparison the closest work to ours, to the best of our knowledge, represents @xcite . @xcite , and verbocean (vo, @xcite . to hit the high score on sick, they combine multiple components including distributional semantics, a set of hand-crafted rules, resolution-based on-fly generation of inference rules, and an svm classifier as the final predictor. @xcite use a lightweight system, called monalog, based on monotonicity reasoning. it is further combined with bert @xcite to reclassify problems that were predicted by monalog as neutral. abductive reasoning was already employed by @xcite at the first recognizing textual entailment challenge @xcite . they used resolution method and a learned cost model to select the cheapest set of assumptions supporting the entailment. @xcite uses weighted abduction to model text interpretation as the minimal explanation of why text would be true. the title of the current paper is inspired by this work. ## conclusion for future work it is interesting to explore the ways that consider larger explanation space and are not strictly preferring short phrases to longer ones. the latter will allow relations with more context.