Premise Selection for Theorem Proving by Deep Graph Embedding

Introduction

Automated reasoning over mathematical proofs is a core question of artificial intelligence that dates back to the early days of computer science . It not only constitutes a key aspect of general intelligence, but also underpins a broad set of applications ranging from circuit design to compilers, where it is critical to verify the correctness of a computer system .

A key challenge of theorem proving is premise selection : selecting relevant statements that are useful for proving a given conjecture. Theorem proving is essentially a search problem with the goal of finding a sequence of deductions leading from presumed facts to the given conjecture. The space of this search is combinatorial—with today’s large mathematical knowledge bases , the search can quickly explode beyond the capability of modern automated theorem provers, despite the fact that often only a small fraction of facts in the knowledge base are relevant for proving a given conjecture. Premise selection thus plays a critical role in narrowing down the search space and making it tractable.

Premise selection has been traditionally tackled as hand-designed heuristics based on comparing and analyzing symbols . Recently, machine learning methods have emerged as a promising alternative for premise selection, which can naturally be cast as a classification or ranking problem. Alama et al. trained a kernel-based classifier using essentially bag-of-words features, and demonstrated large improvement over the state of the art system. Alemi et al. were the first to apply deep learning approaches to premise selection and demonstrated competitive results without manual feature engineering. Kaliszyk et al. introduced HolStep, a large dataset of higher-order logic proofs, and provided baselines based on logistic regression and deep networks.

In this paper we propose a new deep learning approach to premise selection. The key idea of our approach is to represent mathematical formulas as graphs and embed them into vector space. This is different from prior work on premise selection that directly applies deep networks to sequences of characters or tokens . Our approach is motivated by the observation that a mathematical formula can be represented as a graph that encodes the syntactic and semantic structure of the formula. For example, the formula $\forall x\exists y(P(x)\wedge Q(x,y))$ can be expressed as the graph shown in Fig. 1, where edges link terms to their constituents and connect quantifiers to their variables.

Our hypothesis is that such graph representations are better than sequential forms because a graph makes explicit key syntactic and semantic structures such as composition, variable binding, and co-reference. Such an explicit representation helps the learning of invariant feature representations. For example, $P(x,T(f(z)+g(z),v))\wedge Q(y)$ and $P(y)\wedge Q(x)$ share the same top level structure $P\wedge Q$, but such similarity would be less apparent and harder to detect from a sequence of tokens because syntactically close terms can be far apart in the sequence.

Another benefit of a graph representation is that we can make it invariant to variable renaming while preserving the semantics. For example, the graph for $\forall x\exists y(P(x)\wedge Q(x,y)$ (Fig. 1) is the same regardless of how the variables are named in the formula, but the semantics of quantifiers and co-reference is completely preserved—the quantifier $\forall$ binds a variable that is the first argument of both $P$ and $Q$, and the quantifier $\exists$ binds a variable that is the second argument of $Q$.

It is worth noting that although a sequential form encodes the same information, and a neural network may well be able to learn to convert a sequence of tokens into a graph, such a neural conversion is unnecessary—unlike parsing natural language sentences, constructing a graph out of a formula is straightforward and unambiguous. Thus there is no obvious benefit to be gained through an end-to-end approach that starts from the textual representation of formulas.

To perform premise selection, we convert a formula into a graph, embed the graph into a vector, and then classify the relevance of the formula. To embed a graph into a vector, we assign an initial embedding vector for each node of the graph, and then iteratively update the embedding of each node using the embeddings of its neighbors. We then pool the embeddings of all nodes to form the embedding of the entire graph. The parameters of each update are learned end to end through backpropagation. In other words, we learn a deep network that embeds a graph into a vector; the topology of the unrolled network is determined by the input graph.

We perform experiments using the HolStep dataset , which consists of over two million conjecture-statement pairs that can be used to evaluate premise selection. The results show that our graph-embedding approach achieves large improvement over sequence-based models. In particular, our approach improves the state-of-the-art accuracy on HolStep by 7.3%.

Our main contributions of this work are twofold. First, we propose a novel approach to premise selection that represents formulas as graphs and embeds them into vectors. To the best our knowledge, this is the first time premise selection is approached using deep graph embedding. Second, we improve the state-of-the-art classification accuracy on the HolStep dataset from 83% to 90.3%.

Related Work

Research on automated theorem proving has a long history . Decades of research has resulted in a variety of well-developed automated theorem provers such as Coq , Isabelle , and E . However, no existing automated provers can scale to large mathematical libraries due to combinatorial explosion of the search space. This limitation gave rise to the development of interactive theorem proving , which combines humans and machines in theorem proving and has led to impressive achievements such as the proof of the Kepler conjecture and the formal proof of the Feit-Thompson problem .

Premise selection as a machine learning problem was introduced by Alama et al. , who constructed a corpus of proofs to train a kernelized classifier using bag-of-word features that represent the occurrences of terms in a vocabulary. Deep learning techniques were first applied to premise selection in the DeepMath work by Alemi et al. , who applied recurrent networks and convolutional to formulas represented as textual sequences, and showed that deep learning approaches can achieve competitive results against baselines using hand-engineered features. Serving the needs for large datasets for training deep models, Kaliszyk et al. introduced the HolStep dataset that consists of 2M statements and 10K conjectures, an order of magnitude larger than the DeepMath dataset .

A related task to premise selection is proof guidance , the selection of the next clause to process inside an automated theorem prover. Proof guidance differs from premise selection in that proof guidance depends on the logical representation, inference algorithm, and current state inside a theorem prover, whereas premise selection is only about picking relevant statements as the initial input to a theorem prover that is treated as a black box. Because proof guidance is tightly integrated with proof search and is invoked repeatedly, efficiency is as important as accuracy, whereas for premise selection efficiency is not as critical.

Loos et al. were the first to apply deep networks to proof guidance. They experimented with both sequential representations and tree representations (recursive neural networks ). Note that their tree representations are simply the parse trees, which, unlike our graphs, are not invariant to variable renaming and do not capture how quantifiers bind variables. Whalen et al. used GRU networks to guide the exploration of partial proof trees, with formulas represented as sequences of tokens.

In addition to premise selection and proof guidance, other aspects of theorem proving have also benefited from machine learning. For example, Kühlwein et al. applied kernel methods to strategy finding, the problem of searching for good parameter configurations for an automated prover. Similarly, Bridge et al. applied SVM and Gaussian Processes to select good heuristics, which are collections of standard settings for parameters and other decisions.

Our graph embedding method is related to a large body of prior work on embeddings and graphs. Deepwalk , LINE and Node2Vec focus on learning node embeddings. Similar to Word2Vec , they optimize the embedding of a node to predict nodes in a neighborhood. Recursive neural networks and Tree LSTMs consider embeddings of trees, a special type of graphs. Neural networks on general graphs were first introduced by Gori et al and Scarselli et al . Many follow-up works proposed specific architectures to handle graph-based input by extending recurrent neural network to graph data or making use of graph convolutions based on spectral graph theories . Our approach is most similar to the work of , where they encode molecular fragments as neural fingerprints with graph-based convolutions for chemical applications. But to the best of our knowledge, no previous deep learning approaches on general graphs preserve the order of edges. In contrast, we propose a novel way of graph embedding that can preserve the information of edge ordering, and demonstrate its effectiveness for premise selection.

FormulaNet: Formulas to Graphs to Embeddings

We consider formulas in higher-order logic . A higher-order formula can be defined recursively based on a vocabulary of constants, variables, and quantifiers. A variable or a constant can act as a value or a function. For example, $\forall f\exists x(f(x,c)\wedge P(f))$ is a higher-order formula where $\forall$ and $\exists$ are quantifiers, $c$ is a constant value, $P,\wedge$ are constant functions, $x$ is a variable value, and $f$ is both a variable function and a variable value.

To construct a graph from a formula, we first parse the formula into a tree, where each internal node represents a constant function, a variable function, or a quantifier, and each leaf node represents a variable value or a constant value. We then add edges that connect a quantifier node to all instances of its quantified variables, after which we merge (leaf) nodes that represent the same constant or variable. Finally, for each occurrence of a variable, we replace its original name with $\mathtt{VAR}$, or $\mathtt{VARFUNC}$ if it acts as a function. Fig. 2 illustrates these steps.

Formally, let $\mathcal{S}$ be the set of all formulas, $\mathcal{C}_{v}$ be the set of constant values, $\mathcal{C}_{f}$ the set of constant functions, $\mathcal{V}_{v}$ the set of variable values, $\mathcal{V}_{f}$ the set of variable functions, and $\mathcal{Q}$ the set of quantifiers. Let $s$ be a higher-order logic formula with no free variables—any free variables can be bounded by adding quantifiers $\forall$ to the front of the formula. The graph $G_{s}=(V_{s},E_{s})$ of formula $s$ can be recursively constructed as follows:

if $s=\alpha$, where $\alpha\in\mathcal{C}_{v}\cup\mathcal{V}_{v}$, then $G_{s}\leftarrow(\{\alpha\},\emptyset)$, i.e. the graph contains a single node $\alpha$.

if $s=f(s_{1},s_{2},\dots,s_{n})$, where $f\in\mathcal{C}_{f}\cup\mathcal{V}_{f}$ and $s_{1},\dots,s_{n}\in\mathcal{S}$, then we perform $G_{s}^{\prime}\leftarrow\left(\bigcup_{i}^{n}V_{s_{i}}\cup\{f\},\bigcup_{i}^{n}E_{s_{i}}\cup\{(f,\nu(s_{i}))\}_{i}\right)$ followed by $G_{s}\leftarrow\mathtt{MERGE\_C}(G_{s}^{\prime})$, where $\nu(s_{i})$ is the “head node” of $s_{i}$ and $\mathtt{MERGE\_C}$ is an operation that merges the same constant (leaf) nodes in the graph.

if $s=\phi_{x}t$, where $\phi\in\mathcal{Q}$, $t\in\mathcal{S}$, $x\in\mathcal{V}_{v}\cup\mathcal{V}_{f}$, then we perform $G_{s}^{\prime\prime}\leftarrow\left(V_{t}\cup\{f\},E_{t}\cup\{(\phi,\nu(t))\bigcup_{v\in V_{t}[x]}\{(\phi,v)\}\right)$, followed by $G_{s}^{\prime}\leftarrow\mathtt{MERGE}_{x}(G_{s}^{\prime\prime})$ if $x\in\mathcal{V}_{v}\cup\mathcal{V}_{f}$ and $G_{s}\leftarrow\mathtt{RENAME}_{x}(G_{s}^{\prime})$, where $V_{t}[x]$ is the nodes that represent the variable $x$ in the graph of $t$, $\mathtt{MERGE_{x}}$ is an operation that merges all nodes representing the variable $x$ into a single node, and $\mathtt{RENAME}_{x}$ is an operation that renames $x$ to $\mathtt{VAR}$ (or $\mathtt{VARFUNC}$ if $x$ acts as a function).

By construction, our graph is invariant to variable renaming, yet no syntactic or semantic information is lost. This is because for a variable node (either as a function or value), its original name in the formula is irrelevant in the graph—the graph structure already encodes where it is syntactically and which quantifier binds it.

2 Graphs to Embeddings

To embed a graph to a vector, we take an approach similar to performing convolution or message passing on graphs . The overall idea is to associate each node with an initial embedding and iteratively update them. As shown in Fig. 3, suppose $v$ and each node around $v$ has an initial embedding. We update the embedding of $v$ by the node embeddings in its neighborhood. After multi-step updates, the embedding of $v$ will contain information from its local strcuture. Then we max-pool the node embeddings across all of nodes in the graph to form an embedding for the graph.

To initialize the embedding for each node, we use the one-hot vector that represents the name of the node. Note that in our graph all variables have the same name $\mathtt{VAR}$ (or $\mathtt{VARFUNC}$ if the variable acts as a function), so their initial embeddings are the same. All other nodes (constants and quantifiers) each have their names and thus their own one-hot vectors.

We then repeatedly update the embedding of each node using the embeddings of its neighbors. Given a graph $G=(V,E)$, at step $t+1$ we update the embedding $x_{v}^{t+1}$ of node $v$ as follows:

where $d_{v}$ is the degree of node $v$, $F_{I}^{t}$ and $F_{O}^{t}$ are update functions using incoming edges and outgoing edges, and $F_{P}^{t}$ is an update function to conbine the old embeddings with the new update from neighbor nodes. We parametrize these update functions as neural networks; the detailed configurations will be given in Sec. 4.2.

It is worth noting that all node embeddings are updated in parallel using the same update functions, but the update functions can be different across steps to allow more flexibility. Repeated updates allow each embedding to incorporate information from a bigger neighborhood and thus capture more global structures. Interestingly, with zero updates, our model reduces to a bag-of-words representation, that is, a max pooling of individual node embeddings.

To predict the usefulness of a statement for a conjecture, we send the concatenation of their embeddings to a classifier. The classification can also be done in the unconditional setting where only the statement is given; in this case we directly send the embedding of the statement to a classifier. The parameters of the update functions and the classifiers are learned end to end through backpropagation.

3 Order-Preserving Embeddings

For functions in a formula, the order of its arguments matters. That is, $f(x,y)$ cannot generally be presumed to mean the same as $f(y,x)$. But our current embedding update as defined in Eqn. 1 is invariant to the ordering of arguments. Given that it is possible that the ordering of arguments can be a useful feature for premise selection, we now consider a variant of our basic approach to make our graph embeddings sensitive to the ordering of arguments. In this variant, we update each node considering the ordering of its incoming edges and outgoing edges.

Before we define our new update equation, we need to introduce the notion of a treelet. Given a node $v$ in graph $G=(V,E)$, let $(v,w)\in E$ be an outgoing edge of $v$, and let $r_{v}(w)\in\{1,2,\ldots\}$ be the rank of edge $(v,w)$ among all outgoing edges of $v$. We define a treelet of graph $G=(V,E)$ as a tuple of nodes $(u,v,w)\in V\times V\times V$ such that (1) both $(v,u)$ and $(v,w)$ are edges in the graph and (2) $(v,u)$ is ranked before $(v,w)$ among all outgoing edges of $v$. In other words, a treelet is a subgraph that consists of a head node $v$, a left child $u$ and a right child $w$. We use $\mathcal{T}_{G}$ to denote all treelets of graph $G$, that is, $\mathcal{T}_{G}=\{(u,v,w):(v,u)\in E,(v,w)\in E,r_{v}(u)<r_{v}(w)\}$.

Now, when we update a node embedding, we consider not only its direct neighbors, but also its roles in all the treelets it belongs to:

where $e_{v}=|\{(u,v,w):(u,v,w)\in\mathcal{T}_{G}\vee(v,u,w)\in\mathcal{T}_{G}\vee(u,w,v)\in\mathcal{T}_{G}\}|$ is the number of total treelets containing $v$. In this new update equation, $F_{L}$ is an update function that considers a treelet where node $v$ is the left child. Similarly, $F_{H}$ considers a treelet where node $v$ is the head and $F_{R}$ considers a treelet where node $v$ is the right child. As in Sec. 3.2, the same update functions are applied to all nodes at each step, but across steps the update functions can be different. Fig. 3 shows the update equation of a concrete example.

Our design of Eqn. 2 now allows a node to be embedded differently dependent on the ordering of its own arguments and dependent on which argument slot it takes in a parent function. For example, the function node $f$ can now be embedded differently for $f(a,b)$ and $f(b,a)$ because of the output of $F_{H}$ can be different. As another example, in the formula $g(f(a),f(a))$, there are two function nodes with the same name $f$, same parent $g$, and same child $a$, but they can be embedded differently because only $F_{L}$ will be applied to the $f$ as the first argument of $g$ and only $F_{R}$ will be applied to the $f$ as the second argument of $g$.

To distinguish the two variants of our approach, we call the method with the treelet update terms FormulaNet, as opposed to the basic FormulaNet-basic without considering edge ordering.

Experiments

We evaluate our approach on the HolStep dataset , a recently introduced benchmark for evaluating machine learning approaches for theorem proving. It was constructed from the proof trace files of the HOL Light theorem prover on its multivariate analysis library and the formal proof of the Kepler conjecture. The dataset contains 11,410 conjectures, including 9,999 in the training set and 1,411 in the test set. Each conjecture is associated with a set of statements, each with a ground truth label on whether the statement is useful for proving the conjecture. There are 2,209,076 conjecture-statement pairs in total. We hold out 700 conjectures from the training set as the validation set to tune hyperparameters and perform ablation analysis.

Following the evaluation setup proposed in , we treat premise selection as a binary classification task and evaluate classification accuracy. Also following , we evaluate two settings, the conditional setting where both the conjecture and the statement are given, and the unconditional setting where the conjecture is ignored. In HolStep, each conjecture is associated with an equal number of positive statements and negative statements, so the accuracy of random prediction is $50\%$.

2 Network Configurations

The initial one-hot vector for each node has 1909 dimensions, representing 1909 unique tokens. These 1909 tokens include 1906 unique constants from the training set and three special tokens, "VAR", "VARFUNC", and "UNKNOWN" (representing all novel tokens during testing).

The update functions in Eqn. 1 and Eqn. 2 are parametrized as neural networks. Fig. 4 (a), (b) shows their configurations. All update functions are configured the same: concatenation of inputs followed by two fully connected layers with ReLUs, Batch Normalizations .

The classifier for the conditional setting takes in the embeddings from the conjecture and the statement. Its configuration is shown in Fig. 4 (c). The classifier for the unconditional setting uses only the embedding of the statement; its configuration is shown in Fig. 4 (d).

3 Model Training

We train our networks using RMSProp with 0.001 learning rate and $1\times 10^{-4}$ weight decay. We lower the learning rate by 3X after each epoch. We train all models for five epochs and all networks converge after about three or four epochs.

It is worth noting that there are two levels of batching in our approach: intra-graph batching and inter-graph batching. Intra-graph batching arises from the fact that to embed a graph, each update function ($F_{P},F_{I},F_{O},F_{L},F_{H},F_{R}$ in Eqn. 2) is applied to all nodes in parallel. This is the same as training each update function as a standalone network with a batch of input examples. Thus batch normalization can be applied to the inputs of each update function within a single graph.

Furthermore, this batch normalization within a graph can be run in the training mode even when we are only performing inference to embed a graph, because there are multiple input examples to each update function within a graph. Another level of batching is the regular batching of multiple graphs in training, as is necessary for training the classifier. As usual, batch normalization across graphs is done in the evaluation mode in test time.

We also apply intermediate supervision after each step of embedding update using a separate classifier. For training, our loss function is the sum of cross-entropy losses for each step. We use the prediction from the last step as our final predictions.

4 Main Results

Table 1 compares the accuracy of our approach versus the best existing results . Our approach improves the best existing result by a large margin from $83\%$ to $90.3\%$ in the conditional setting and from $83\%$ to $90.0\%$ in the unconditional setting. We also see that FormulaNet gives a $1\%$ improvement over the FormulaNet-basic, validating our hypothesis that the order of function arguments provides useful cues.

Consistent with prior work , conditional and unconditional selection have similar performances. This is likely due to the data distribution in HolStep. In the training set, only 0.8% of the statements appear in both a positive statement-conjecture pair and a negative statement-conjecture pair, and the upper performance bound of unconditional selection is 97%. In addition, HolStep contains 9,999 unique conjectures but 1,304,888 unique statements for training, so it is likely easier for the network to learn useful patterns from statements than from conjectures.

We also apply Deepwalk , an unsupervised approach for generating node embeddings that is purely based on graph topology without considering the token associated with each node. For each formula graph, we max-pool its node embeddings and train a classifier. The accuracy is 61.8% (conditional) and 61.7% (unconditional). This result suggests that for embedding formulas it is important to use token information and end-to-end supervision.

5 Ablation Experiments

Invariance to Variable Renaming One motivation for our graph representation is that the meaning of formulas should be invariant to the renaming of variable values and variable functions. To achieve such invariance, we perform two main transformations of a parse tree to generate a graph: (1) we convert the tree to a graph by linking quantifiers and variables, and (2) we discard the variable names.

We now study the effect of these steps on the premise selection task. We compare FormulaNet-basic with the following three variants whose only difference is the format of the input graph:

Tree-old-names: Use the parse tree as the graph and keep all original names for the nodes. An example is the tree in Fig. 2 (b).

Tree-renamed: Use the parse tree as the graph but rename all variable values to $\mathtt{VAR}$ and variable functions to $\mathtt{VARFUNC}$.

Graph-old-names: Use the same graph as FormulaNet-basic but keep all original names for the nodes, thus making the graph embedding dependent on the original variable names. An example is the graph in Fig. 2 (c).

We train these variants on the same training set as FormulaNet-basic. To compare with FormulaNet-basic, we evaluate them on the same held-out validation set. In addition, we generate a new validation set (Renamed Validation) by randomly permutating the variable names in the formulas—the textual representation is different but the semantics remains the same. We also compare all models on this renamed validation set to evaluate their robustness to variable renaming.

Table 2 reports the results. If we use a tree with the original names, there is a slight drop when evaluate on the original validation set, but there is a very large drop when evaluated on the renamed validation set. This shows that there are features exploitable in the original variable names and the model is exploiting it, but the model is essentially overfitting to the bias in the original names and cannot generalize to renamed formulas. The same applies to the model trained on graphs with the original names, whose performance also drops drastically on renamed formulas.

It is also interesting to note that the model trained on renamed trees performs poorly, although it is invariant to variable renaming. This shows that the syntactic and semantic information encoded in the graph on variables—particularly their quantifiers and coreferences—is important.

Number of Update Steps An important hyperparameter of our approach is the number of steps to update the embeddings. Zero steps can only embed a bag of unstructured tokens, while more steps can embed information from larger graph structures. Table 3 compares the accuracy of models with different numbers of update steps. Perhaps surprisingly, models with zero steps can already achieve an accuracy of $81.5\%$, showing that much of the performance comes from just the names of constant functions and values. More steps lead to notable increases of accuracy, showing that the structures in the graph are important. There is a diminishing return after 3 steps, but this can be reasonably expected because a radius of 3 in a graph is a fairly sizable neighborhood and can encompass reasonably complex expressions—a node can influence its grand-grandchildren and grand-grandparents. In addition, it would naturally be more difficult to learn generalizable features from long-range patterns because they are more varied and each of them occurs much less frequently.

6 Visualization of Embeddings

To qualitatively examine the learned embeddings, we find out a set of nodes with similar embeddings and visualize their local structures in Fig. 5. In each row, we use a node as the query and find the nearest neighbors across all nodes from different graphs. We can see that the nearest neighbors have similar structures in terms of topology and naming. This demonstrates that our graph embeddings can capture syntactic and semantic structures of a formula.

Conclusion

In this work, we have proposed a deep learning-based approach to premise selection. We represent a higher-order logic formula as a graph that is invariant to variable renaming but fully preserves syntactic and semantic information. We then embed the graph into a continuous vector through a novel embedding method that preserves the information of edge ordering. Our approach has achieved state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%.

This work is partially supported by the National Science Foundation under Grant No. 1633157.

References