Premise Selection for Theorem Proving by Deep Graph Embedding

2017/09/28 by Mingzhe Wang, Yihe Tang, Wang, Mingzhe +5 · 28 citations
Computer Science · Mathematics · #Advanced Graph Neural Networks #Artificial Intelligence (cs.AI) #Artificial intelligence #Computer science #Discrete mathematics #Embedding #Epistemology #FOS: Computer and information sciences #Graph #Graph Theory and Algorithms #Logic in Computer Science (cs.LO) #Machine Learning (cs.LG) #Mathematical economics #Mathematics #Philosophy #Premise #Selection (genetic algorithm) #Theoretical computer science #Topic Modeling #cs.AI #cs.LG #cs.LO

paper · pdf · doi:10.48550/arxiv.1709.09994

published in arXiv (Cornell University) (Cornell University) · Mingzhe Wang and Yihe Tang contributed equally

arxiv created 2017/09/28 · openalex publication_date 2017/09/28 · arxiv updated 2017/10/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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%.

Citations

• Deep Convolutional Networks on Graph-Structured Data
• Gated Graph Sequence Neural Networks
• Learning Convolutional Neural Networks for Graphs
• Holophrasm: a neural Automated Theorem Prover for higher-order logic
• Semi-Supervised Classification with Graph Convolutional Networks
• HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
• Internal Guidance for Satallax
• node2vec

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)
• MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
• Hierarchical Attention Generates Better Proofs
• AI for Mathematics: Progress, Challenges, and Prospects
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification

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