Traditional automated theorem provers have relied on manually tuned heuristics to guide how they perform proof search. Recently, however, there has been a surge of interest in the design of learning mechanisms that can be integrated into theorem provers to improve their performance automatically. In this work, we describe TRAIL (Trial Reasoner for AI that Learns), a deep learning-based approach to theorem proving that characterizes core elements of saturation-based theorem proving within a neural framework. TRAIL leverages (a) an effective graph neural network for representing logical formulas, (b) a novel neural representation of the state of a saturation-based theorem prover in terms of processed clauses and available actions, and (c) a novel representation of the inference selection process as an attention-based action policy. We show through a systematic analysis that these components allow TRAIL to significantly outperform previous reinforcement learning-based theorem provers on two standard benchmark datasets (up to 36% more theorems proved). In addition, to the best of our knowledge, TRAIL is the first reinforcement learning-based approach to exceed the performance of a state-of-the-art traditional theorem prover on a standard theorem proving benchmark (solving up to 17% more theorems).

Automated theorem provers have traditionally relied on manually tuned heuristics to guide how they perform proof search. Deep reinforcement learning has been proposed as a way to obviate the need for such heuristics, however, its deployment in automated theorem proving remains a challenge. In this paper we introduce TRAIL, a system that applies deep reinforcement learning to saturation-based theorem proving. TRAIL leverages (a) a novel neural representation of the state of a theorem prover and (b) a novel characterization of the inference selection process in terms of an attention-based action policy. We show through systematic analysis that these mechanisms allow TRAIL to significantly outperform previous reinforcement-learning-based theorem provers on two benchmark datasets for first-order logic automated theorem proving (proving around 15% more theorems).

Textual entailment is a fundamental task in natural language processing. Most approaches for solving this problem use only the textual content present in training data. A few approaches have shown that information from external knowledge sources like knowledge graphs (KGs) can add value, in addition to the textual content, by providing background knowledge that may be critical for a task. However, the proposed models do not fully exploit the information in the usually large and noisy KGs, and it is not clear how it can be effectively encoded to be useful for entailment. We present an approach that complements text-based entailment models with information from KGs by (1) using Personalized PageRank to generate contextual subgraphs with reduced noise and (2) encoding these subgraphs using graph convolutional networks to capture the structural and semantic information in KGs. We evaluate our approach on multiple textual entailment datasets and show that the use of external knowledge helps the model to be robust and improves prediction accuracy. This is particularly evident in the challenging BreakingNLI dataset, where we see an absolute improvement of 5-20% over multiple text-based entailment models.

Natural Language Inference (NLI) is fundamental to many Natural Language Processing (NLP) applications including semantic search and question answering. The NLI problem has gained significant attention due to the release of large scale, challenging datasets. Present approaches to the problem largely focus on learning-based methods that use only textual information in order to classify whether a given premise entails, contradicts, or is neutral with respect to a given hypothesis. Surprisingly, the use of methods based on structured knowledge – a central topic in artificial intelligence – has not received much attention vis-a-vis the NLI problem. While there are many open knowledge bases that contain various types of reasoning information, their use for NLI has not been well explored. To address this, we present a combination of techniques that harness external knowledge to improve performance on the NLI problem in the science questions domain. We present the results of applying our techniques on text, graph, and text-and-graph based models; and discuss the implications of using external knowledge to solve the NLI problem. Our model achieves close to state-of-the-art performance for NLI on the SciTail science questions dataset.

Virtual worlds present a natural test bed to observe and study the social behaviors of people at a large scale. Analyzing the rich “big data” generated by the activities of players in a virtual world enables us to better understand the online society, to validate and propose sociological theories, and to provide insights of how people behave in the real world. However, how to better store and analyze such complex big data has always been an issue that prevents in-depth analyses. In this paper, we first review the research on trust in virtual worlds and Semantic Web as applied in social network analysis. Then, we present how we employed Semantic Web technologies to address this issue, and how we explored certain social concepts expressed within a massively multiplayer online game-Ever Quest I I. Specifically, the relations between mentors and mentees in the game are studied. We use the housing network to measure the trust between mentors and mentees and adopt the logistic regression model to identify the predictors of building trust between them. Our research sheds light on how to analyze largescale data within a virtual world by exploring the flow of trust in different layers of social networks with the help of Semantic Web technologies.

Analyzing “what topics” a user discusses with others is important in social network analysis. Since social relationships can be represented as multiobject relationships (e.g., those composed of a user, another user, and the topic of communication), they can be naturally represented as a tensor. By factorizing the tensor, we can perform communication prediction that predicts links among users and the topics discussed among them. The prediction accuracy, however, is often inadequate for applications because: 1) users usually discuss a variety of topics, and thus the prediction results tend to be biased toward popular domains and 2) topics that are rarely discussed among users trigger the sparsity problem in tensor factorization. Our solution, cross-domain tensor factorization (CrTF), first determines the topic domain by analyzing communication logs among users using the DBpedia knowledge base and creates a tensor composed of users, other users, and the topics of communication for each domain; it avoids strong bias toward particular domains. It then simultaneously factorizes tensors across domains while integrating semantics from DBpedia into factorizations; this solves the sparsity problem. Experiments using Twitter data sets show that CrTF achieves higher accuracy than the state-ofthe-art tensor-based methods and extracts key topics and social influencers for each domain.