Talking with the Theorem Prover to Interactively Solve Natural Language Inference

Talking with the Theorem Prover to Interactively Solve Natural Language Inference 1Atsushi Sumita University of Tokyo 2Koji Mineshima Keio University 1atsushisumita0421@gmail.com 2minesima@abelard.flet.keio.ac.jp 3yusuke@is.s.u-tokyo.ac.jp 3Yusuke Miyao University of Tokyo Abstract Solving natural language inference (NLI) with formal semantics and automated theorem proving has the merit of high precision and interpretability. However, they suffer from non-logical inference such as lexical infer- ence. To overcome this weakness, we propose a human-in-the-loop mechanism in which the user provides non-logical knowledge to the theorem prover. We focus on the subgoal of a proof. A subgoal is a proposition that remains unproved by the theorem prover. Although the subgoal conveys what knowledge should be supplemented to the proof, it is a logical for- mula inscrutable to normal users. To make the subgoal understandable to the user, we pro- pose a method to translate the subgoal into a natural language text. The resulting sentence is called a readable subgoal. The reaction to the readable subgoal is communicated to the theorem prover in the form of temporary ax- iom, a logical formula that conveys the con- tent of the reaction. We experimented with our method by adding an interactive component to an existing NLI system, ccg2lambda. The annotators recruited by Amazon Mechanical Turk used the proposed system to solve SICK, a data set for NLI. Experiments show the inter- action improved the recall rate of ccg2lambda from 32.1% to 44.1%, and the accuracy from 70.4% to 75.1%. 1 Introduction Natural Language Inference (NLI) is a task to judge whether a text fragment entails another text frag- ment (Levy et al., 2013). The former fragment is Figure 1: The user enters the premise and the hypothesis, which the semantic parser converts to semantic represen- tations. This is passed to the automated theorem prover, which attempts to prove the hypothesis from the premise. If the proof does not succeed, it outputs the subgoal, which is the input to our proposed method. Our method converts the subgoal into readable subgoal, so the user can understand the content of the subgoal. The reaction of the user is fed back to the theorem prover as tempo- rary axioms, so the proof can continue. called the premise, and the latter fragment is called the hypothesis. NLI has many potential applica- tions such as question answering, summarization, machine translation, and so on (Dagan et al., 2010; White et al., 2017; Bora-Kathariya and Haribhakta, 2018; Demszky et al., 2018; Poliak et al., 2018; Thorne and Vlachos, 2018). Moreover, NLI itself has been considered as an important task to measure progress in natural language understanding (Wang et al., 2018; Wang et al., 2020). We hypothesize that interaction between the ma- chine and the human is useful for NLI. Generally speaking, humans are better at recog- nizing non-logical inference such as lexical infer- ence or common sense reasoning, while machines are better at comprehensive search and verification over logical relationships. To evaluate this hypoth- esis, we propose an NLI system based on formal semantics and theorem prover, which …

Content truncated to 500 words