Premise Selection for Theorem Proving by Deep Graph Embedding

By Mingzhe Wang, Yihe Tang, Jian Wang, Jia Deng. 2017

151 citations recorded by the source corpus.

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

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition, Information Retrieval & Search

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Vision and Pattern Recognition

In Information Retrieval & Search

Citations in the corpus

oLMpics-On What Language Model Pre-training Captures (2019, background): “Prior work explored retrieving the correct quantifier for a statement (Herbelot and Vecchi, 2015; Wang et al., 2017).”
Generative Language Modeling for Automated Theorem Proving (2020, methodology): “DeepMath [26] explored the use of CNNs and RNNs to predict whether a premise is useful to demonstrate a given conjecture, their results were later improved with FormulaNet [27] by the use of graph neural networks, reminiscent of NeuroSAT [28].”
Learning to Represent Programs with Graphs (2017, background): “Somewhat related to source code is the work of Wang et al. (2017) who learn graph-based representations of mathematical formulas for premise selection in theorem proving.”
Image Generation from Scene Graphs (2018, methodology): “GNNs and related models have been applied to molecular property prediction [7], program verification [29], modeling human motion [19], and premise selection for theorem proving [54].”
LambdaNet: Probabilistic Type Inference using Graph Neural Networks (2020, methodology): “Wang et al. (2017) use GNNs to encode mathematical formulas for premise selection in automated theorem proving.”
Formal Mathematics Statement Curriculum Learning (2022, background): “…in mathlib (which typically includes generic theorems and lem-mas but very few exercises), we hypothesized that if the difﬁculty of this set of statements was made varied enough, expert iteration could potentially leverage it to effectively shift our models’ distribution closer to miniF2F ’s, and…”
GamePad: A Learning Environment for Theorem Proving (2018, methodology): “[23] extend the HolStep work to show the advantage of using a DeBruijn representation of proof terms as opposed to string-level encodings for premise selection.”
Learning to Reason in Large Theories without Imitation (2019, background): “More recent works include Alama et al. [2014], Blanchette et al. [2016], Kaliszyk and Urban [2015] and Wang et al. [2017].”
Embedding Logical Queries on Knowledge Graphs (2018, result): “Lastly, our work builds closely upon recent advancements in neural theorem proving [34, 43], which have demonstrated how neural networks can prove first-order logic statements in toy knowledge bases [36].”
A Semantic Loss Function for Deep Learning with Symbolic Knowledge (2017, background): “, 2016), neural theorem proving, and learning with constraints (Hu et al., 2016; Stewart & Ermon, 2017; Minervini et al., 2017; Wang et al., 2017).”
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling (2019, methodology): “For the proof step classiﬁcation task on Holstep, we compare against 4 systems implemented in two prior works: 1) DeepWalk and FormulaNet, both of which were applied to Holstep in [18].”
Learning to Prove Theorems via Interacting with Proof Assistants (2019, methodology): “The proof search has been signiﬁcantly improved by machine learning (Irving et al., 2016; Wang et al., 2017; Urban et al., 2011; Bridge et al., 2014; Loos et al., 2017; Kaliszyk et al., 2018; Rockt ¨ aschel & Riedel, 2017).”
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning (2021, background): “Graph neural networks are shown to provide a much stronger performance than tree models in premise selection (Wang et al., 2017) and theorem proving (Paliwal et al.”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, background): “A few approaches [Irving et al., 2016, Wang et al., 2017, Kaliszyk et al., 2017] use deep learning in the premise selection task.”
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, methodology): “[45] proposed a premise selection method utilizing deep graphs embeddings.”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, methodology): “Their performances have been improved by machine learning [30, 3, 12, 21, 33, 24, 15].”