A Model-Theoretic Formalization of Natural Language Inference Using Neural Network and Tableau Method

28793

Authors

nan

Abstract

Saji et al. (2021) integrated a neural-based NLI model and a symbolic one into a framework to get the best of both worlds. This framework is based on a tableau method, which is a proof system for formal logic; however, it has a re- maining issue that its theoretical limitations have not been clarified. To solve this issue, this paper formalizes the framework model- theoretically. On the basis of the formalization, we demonstrate that a certain kind of sound- ness holds for this framework, while the com- pleteness does not. 1

Keywords

nan

Full Content

A Model-Theoretic Formalization of Natural Language Inference Using Neural Network and Tableau Method Ayahito Saji1, Yoshihide Kato2, Shigeki Matsubara1,2 1Graduate School of Informatics, Nagoya University 2Information and Communications, Nagoya University Furo-cho, Chikusa-ku, Nagoya, 464-8601, Japan saji.ayahito.y7@s.mail.nagoya-u.ac.jp Abstract Saji et al. (2021) integrated a neural-based NLI model and a symbolic one into a framework to get the best of both worlds. This framework is based on a tableau method, which is a proof system for formal logic; however, it has a re- maining issue that its theoretical limitations have not been clarified. To solve this issue, this paper formalizes the framework model- theoretically. On the basis of the formalization, we demonstrate that a certain kind of sound- ness holds for this framework, while the com- pleteness does not. 1 Introduction The natural language inference (NLI) (Dagan et al., 2013) is the task of identifying the inferential re- lation between a text pair: a premise and hypothe- sis. If a hypothesis can be inferred from a premise using logical and commonsense knowledge, it is judged as entailment. If a premise and hypothe- sis are incompatible, it is judged as contradiction, and if neither of these cases hold, it is judged as neutral. NLI systems are expected to be applied to a wide range of fields, e.g., question answering, information retrieval, and text summarization. In recent years, neural-based approaches (Parikh et al., 2016; Chen et al., 2017; Devlin et al., 2019; Lan et al., 2019; Tai et al., 2020; Wang et al., 2021) have achieved high accuracy in experiments with many NLI datasets, e.g., the SNLI corpus (Bowman et al., 2015), MultiNLI (MNLI) corpus (Williams et al., 2018), Adversarial NLI (ANLI) dataset (Nie et al., 2020), and QNLI dataset (Wang et al., 2018). However, neural-based models have the limitation that they cannot explain the reasoning processes by which inferential relations are derived. Such models represented a black box, and it is difficult to analyze what kind of inference was performed.1 Yanaka et al. (2020) proposed a method to evaluate 1One of the exceptions is the NLI system, which gener- ates explanations by Kumar and Talukdar (2020); however, whether neural models learn the systematicity of monotonicity inference in natural language, and they demonstrated that the generalization ability of current neural models is limited. Gururangan et al. (2018) and Tsuchiya (2018) showed that NLI datasets such as the SNLI corpus and MNLI corpus have a hidden bias in that only a hypothesis is suf- ficient to determine inferential relations, and there is a risk that neural models are simply identifying inferential relations based on such biases. From a different perspective, symbolic ap- proaches to the NLI task have been proposed (Bar- Haim et al., 2007; MacCartney and Manning, 2007, 2008, 2009; Mineshima et al., 2015; Abzianidze, 2015, 2017; Hu et al., 2020). These approaches have the advantage that the reasoning process de- riving the relation is understandable to humans, unlike neural-based approaches. In addition, sym- bolic approaches are generally founded on formal logic or linguistic …

Content truncated to 500 words

Labeled Text

Saji et al. (2021) integrated a neural-based NLI model and a symbolic one into a framework to get the best of both worlds. This framework is based on a tableau method, which is a proof system for formal logic; however, it has a remaining issue that its theoretical limitations have not been clarified. To solve this issue, this paper formalizes the framework modeltheoretically. On the basis of the formalization, we demonstrate that a certain kind of soundness holds for this framework, while the completeness does not. 1

Publication Details

Paper ID:
28793
Year:
2022
Publication:
TIPSTER
Publication Type:
conf
DOI:
nan