Premise Selection for Theorem Proving by Deep Graph Embedding

2017/09/28 by Wang, Mingzhe, Tang, Yihe, Wang, Jian +1 · 4 citations
#Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Machine Learning (cs.LG)

paper · doi:10.48550/arxiv.1709.09994

Abstract

We propose a deep learning-based approach to the problem of premise selection: selecting mathematical statements relevant for proving a given conjecture. We represent a higher-order logic formula as a graph that is invariant to variable renaming but still fully preserves syntactic and semantic information. We then embed the graph into a vector via a novel embedding method that preserves the information of edge ordering. Our approach achieves state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%.

Cited by

• Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective
• Solving Formal Math Problems by Decomposition and Iterative Reflection
• Partial Label Learning for Automated Theorem Proving
• When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)

Related

• DeepMath - Deep Sequence Models for Premise Selection
• Combining Textual and Structural Information for Premise Selection in Lean
• Premise selection with neural networks and distributed representation of features
• Embedding Symbolic Knowledge into Deep Networks
• Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling