The Role of Entropy
in Guiding a Connection Prover

Learning based ATP systems have for a long time explored suitable characterizations of mathematical objects, leading to solutions that process text directly (e.g. [2, 29, 4]) and solutions that rely on manually engineered features (e.g. [26, 18]). Graph neural networks (GNN) [37] provide an alternative to both approaches: the graph representation allows for retaining the syntactic structure of mathematical objects, while also allowing for end-to-end (i.e., involving no manually designed features) training. However, improving over learning based on manual feature extraction has proven to be challenging with GNNs, especially in real time, as noted in several works (e.g. [9, 11]). Usually it required high level of technical engineering. The GNN presented in [32] was designed to preserve many useful invariance properties of logical formulae and has demonstrated impressive improvement in guiding the leanCoP connection calculus compared with gradient boosted trees. We refer to this system as graphCoP.

leanCoP [34] is a compact theorem prover for first-order logic, implementing connection tableau search. The proof search starts with a start clause as a goal and proceeds by building a connection tableau by applying extension steps and reduction steps. leanCoP uses iterative deepening to ensure completeness.

A series of learning systems guiding the leanCoP connection calculus have been developed recently. Of these, we highlight three that use roughly the same reinforcement learning setup: rlCoP [25], plCoP [51] and graphCoP [32]. These systems search for proofs using Monte Carlo Tree Search [7] and they train the value (the proof state quality) and the policy (the inference quality in a proof state) functions similarly to systems like AlphaZero [40, 3]. rlCoP and plCoP use manually developed features [26] and gradient boosted trees (XGBoost [8]) for learning while graphCoP employs a GNN for end-to-end feature extraction and learning. This graph neural network was designed for processing mathematical formulae and has several useful invariance properties: the graph structure is invariant under renaming of symbols, negation and reordering of clauses and literals. In this paper, we incorporate the GNN of [32] into plCoP.

The plCoP system extends leanCoP with paramodulation steps that can handle equality predicates more efficiently. Let $t|_{p}$ denote the subterm of $t$ at position $p$ and $t[u]_{p}$ denote the term obtained after replacing in $t$ at position $p$ by term $u$. Given a goal $G$ and an input clause ¹¹1Assuming Disjunctive Normal Form. $\{X\neq Y,B\}$, such that, for some position $p$ there is a substitution $\sigma$ such that $G|_{p}\sigma=X\sigma$, the paramodulation step changes $G$ to $\{G[Y]_{p}\sigma,B\sigma\}$. Rewriting is allowed in both directions, i.e., the roles of $X$ and $Y$ can be switched.

Reinforcement learning (RL) [43] aims to find the optimal behaviour in an environment defined as a Markov Decision Process (MDP). An $\mbox{MDP}(\mathcal{S},\mathcal{A},\mathcal{R},\mathcal{P},\gamma)$ describes a dynamic process and consists of the following components: $\mathcal{S}$ is the set of possible states, $\mathcal{A}$ is the set of possible actions, $\mathcal{R}:(\mathcal{S}\times\mathcal{A})\rightarrow\mathbb{R}$ is a reward function, $\mathcal{P}:(\mathcal{S}\times\mathcal{A})\rightarrow\mathcal{S}$ is the state transition function and $\gamma$ is the discount factor. We assume that an agent interacts with this MDP, generating sequences of $(s_{t},a_{t},r_{t})$ state-action-reward tuples, called trajectories. The agent is equipped with a policy function $\pi:\mathcal{S}\rightarrow\mathcal{A}$ which determines which action it selects in a particular state. The policy is often stochastic, i.e., it defines a probability distribution over inferences that are possible in a given state. The aim of the agent is to maximize its total accumulated reward $\sum_{t\geq 0}\gamma^{t}r_{t}$. Several components, such as the reward and transition functions, can be stochastic, in which case the aim of the agent it to find the policy $\pi^{*}$ that maximizes its cumulative expected reward, where future rewards are discounted with the $\gamma$ discount factor:

MCTS is a simple RL algorithm, which builds a search tree whose nodes are states and where edges represent actions. The aim of the search algorithm is to find trajectories (branches in the search tree) that yield high accumulated rewards. The search starts from a single root node, and new nodes are added iteratively. In each node $i$, we maintain the number of visits $n_{i}$, the total reward $r_{i}$, and the prior probability (estimated typically by a trained predictor) $p_{i}$ of all its possible successors (in our case produced by the possible inferences). Each iteration, also called playout, involves the addition of a new leaf node.

The policy $\pi$ used for selecting the actions of the playout is based on the standard UCT [27] (Upper Confidence Trees) formula (1): in each state we select the action with the maximal UCT value in the successor state. Once a new leaf state is created, we observe its reward and update its ancestors: visit counts are increased by 1 and rewards are increased by the reward of the leaf.

The plCoP, rlCoP and graphCoP systems use the MaLARea/DAgger [45, 36] meta-learning algorithm to learn the policy and value functions. They interleave ATP runs based on the current policy and value (data collection phase) with a training phase, in which these functions are updated to fit the collected data. Such iterative interleaving of proving and learning has been used successfully in ATP systems such as MaLARea [45] and ENIGMA [20].

During the proof search we build a Monte Carlo tree for each training problem. Its nodes are the proof states (partial tableaux), and the edges represent inferences. Note that the Monte Carlo tree is thus different from the tableau trees. A branch of this Monte Carlo tree leading to a node with a closed tableau is a valid proof. Initially, the three leanCoP-based systems use somewhat different heuristic value and policy functions, later to be replaced with the learned guidance. To enforce deeper exploration, we perform a bigstep after a fixed number of playouts: the starting node of exploration is moved one level down towards the child with the highest value (called the bigstep node). Later MCTS steps thus only extend the subtree under the bigstep node. This in practice means no backtracking of the bigsteps, which in turn involves giving up completeness.

When training the policy, directly maximizing the expected utility on the action sequences observed by an RL agent (i.e., the training examples) can lead to instability. The policy can get stuck in local minima and become overconfident, preventing it from exploring the search space sufficiently when necessary to make good decisions. This has motivated using stochastic policies and several regularization (i.e., encouraging generality) techniques that ensure that all actions have a chance of being selected. Another motivation for properly regularized stochastic policy learning comes from experiments on humans and animals, suggesting that biological agents do not deterministically select the action with the greatest expected utility [47]: instead they randomly select actions with probability proportional to the expected utility, called probability matching. Consequently, action sequences that generate similar rewards tend to be similarly probable, i.e., we avoid making strong commitments whenever it is possible. Maximum Entropy Reinforcement Learning (MaxEnt RL), achieves probability matching by adding an entropy term to the loss founction when the policy is trained:

Shannon’s entropy measures the uniformity of a single distribution. However, when contrasting different policies, we will need a measure to compare different distributions. For this, one of the most widely used options is the Kullback-Leibler (KL) divergence, also called relative entropy, which is a measure of how one probability distribution differs from a given reference distribution. For a discrete target distribution $Q$ and a reference distribution $P$, the KL divergence is defined as:

$KL(P\lVert Q)=1.48$ and $KL(Q\lVert P)=0.58$. When the summed terms are weighted according to $P$ in $KL(P\lVert Q)$, the first two terms get large weight, while only the first term gets large weight in $KL(Q\lVert P)$. When both KL divergences are small, it is a good indicator of similarity of the two distributions.

The MCTS implemented via the UCT formula has a built-in mechanism for balancing the exploitation of proof states that already have high rewards and the exploration of inferences whose effect is not yet known. This balancing serves to mitigate errors in the proof state value estimates. However, we need to do another balancing within exploration, between the different under-explored inference branches. This is estimated by the $\pi^{M}$ policy predictor as the prior probabilities of the possible inferences. Hence, besides the ordering of the inferences that are possible from a given state, their exact prior probabilities are important as they determine how the exploration budget is split between them. This observation directs our attention to the entropy (uncertainty) of $\pi^{M}$ and its relation to the theorem proving performance.

We argue that finding the right level of (un)certainty is particularly important for theorem proving. The goal of learning is to acquire inductive biases that allow the system to perform well on novel problems.²²2In this sense, theorem proving can be considered as a meta learning task. In many situations, however, it is not realistic to extract enough knowledge from the training data that justifies a high level of confidence. Sometimes, there is just not enough analogy between a new problem and the training problems, and we would like our guidance to be more conservative so that we can explore all directions equally. This makes a strong case for using MaxEnt RL, which gives tools for shaping the entropy (uncertainty) profile of our learned $\pi^{M}$ policy predictor.

In this work, we empirically demonstrate the importance of including the “right amount” of entropy when training the policy that guides the theorem prover. To the best of our knowledge, this is the first time that the effect of entropy regularization for MCTS in general and for theorem proving in particular is examined.

Using standard entropy for comparing probability vectors of different length would, however, be misleading. The same entropy value can mean very different uncertainty if the length of the vector changes. For example, consider the vectors

Their entropy is roughly the same (1.1), despite the fact that the first is nearly uniform and the second centers around its first value. To make the uncertainty of these two vectors comparable, we introduce normalized entropy:

Here, $\log(n)$ is the entropy of the uniform distribution when the length is $n$, hence it is the upper bound of $H[p]$. Consequently, $H^{*}[p]\in[0,1]$. Furthermore, it is dimensionless, i.e., it does not depend on the base of the logarithm. The difference between the two distributions in the example above is better captured by their normalized entropy, which is 1 and 0.48.

An alternative mechanism for injecting entropy into the policy is through the softmax temperature parameter $T$. Our policy predictors (both XGBoost and GNN) output an unconstrained logit vector $l$, which is normalized to a probability vector $p$ using the softmax function:

Increasing the temperature flattens the probability curve, approaching the uniform distribution in the limit. On the other hand, if the temperature gets close to $0$, then most of the probability mass concentrates on the most likely action.

While both higher temperature and entropy regularization increase the ultimate entropy of the policy, they work differently. The temperature acts globally and uniformly, flattening all inference probabilities estimated by the trained policy predictor. Entropy regularization, on the other hand, is part of the training process and it allows the neural network to learn distinguishing between situations with low and high uncertainty. In obvious situations, entropy regularization does not prevent the neural network from acquiring great certainty, while it will drive the network to more uniform predictions when there is no strong evidence against that in the training data. Hence, we expect entropy regularization to be more targeted and powerful than the temperature optimization. This is empirically demonstrated in Section 5.

The proof state in the leanCoP setting is roughly described by the partial tableau and by the set of input clauses corresponding to the initial axioms and conjecture. Each time we choose an extension step, we map the state into a hypergraph, as described in [32]. In more detail, we use the current goal (single literal), the active path leading to the current goal (set of literals), the set of all open goals (set of literals), and the input clauses in the hypergraph construction. The GNN processes the hypergraph and outputs a value prediction for the proof state in the range $[0,1]$. It also outputs a probability distribution over all the literals of the axiom clauses that can be used for extension steps, i.e., that can be unified with the negation of the current goal literal.

The above method is used already in graphCoP, but the hypergraph construction algorithm used by graphCoP was designed to guide only the extension steps. Hence it expects the set of all clauses together with the information that identifies literals within the clauses that unify with the negation of the current goal. We adapt this to paramodulation by temporarily creating a clause for each valid paramodulation step that “simulates” the latter as an extension step. Suppose that the current goal is $G$ and there is an input clause $\{X\neq Y,B\}$, such that, for some position $p$ there is a substitution $\sigma$ such that $G|_{p}\sigma=X\sigma$. There is a valid paramodulation step that replaces $G$ with $\{G[Y]_{p}\sigma,B\sigma\}$. We simulate this step as an extension by adding clause $\{\lnot G\sigma,G[Y]_{p}\sigma,B\sigma\}$ to the input clauses, when constructing the graph.

As in plCoP, the value and policy estimates are stored in the MCTS nodes and are used for guiding proof search. The training data for learning policy (inference probabilities) and value (state quality) are also handled as in plCoP. They are extracted from the tableau states of the bigstep nodes. For each bigstep state, the value target is 1³³3A discount factor of 0.99 is applied to positive rewards to favor shorter proofs. if it leads to a proof and 0 otherwise. The policy targets at a particular proof state are the relative frequencies of the possible inferences, i.e., the children in the search tree.

For graphCoP, a single GNN was jointly trained to predict both the value and the policy [32]. However, we observed that training separate predictors yields a small improvement, hence we conduct our experiments in this setup. Consider a tableau state $s$ for which we want to learn its target value $v$ and target policy $p_{1},\dots,p_{n}$. Suppose that the partially trained value predictor outputs $v^{\prime}$ and the policy predictor outputs $p^{\prime}_{1},\dots,p^{\prime}_{n}$, then the objectives that we minimize are:

• •

  value objective: $(v-v^{\prime})^{2}$

• •

  policy objective: $-\sum_{i=1}^{n}p_{i}\cdot\log(p^{\prime}_{i})-\alpha H[p^{\prime}]$

For more details of the graph construction and neural training we refer to [32]. In summary, we use the same setting as there, except for (i) extending guidance to paramodulation steps, (ii) training separate policy and value GNNs, (iii) increasing the number of neural layers in the GNN from 5 to 10,⁴⁴4This is motivated by the experiments with the ENIGMA-GNN system [18], where 8-10 layers produce better results than 5 layers. and (iv) changing the policy training to encourage policies with higher entropy.

We evaluate our system⁵⁵5The new extensions described here and the experimental configuration files are publicly available at plCoP’s repository: https://github.com/zsoltzombori/plcop. using the same datasets as those in [25]. The Mizar40 dataset [22] consists of 32524 problems from the Mizar Mathematical Library that have been proven by several state-of-the-art ATPs used with many strategies and high time limits in the experiments described in [24]. Based on the proofs, the axioms were ATP-minimized, i.e., only those axioms were kept that were needed in any of the ATP proofs found. The smaller M2k dataset [21] consists of 2003 Mizar40 problems that come from related Mizar articles. Finally, we use the bushy (small) problems from the MPTP2078 benchmark [1], which contains just an article-based selection of Mizar problems, regardless of their solvability by a particular ATP system.

Unless otherwise specified, we use the same hyperparameters as described in [51], with the following important exceptions. To allow for faster experiments and put more emphasis on guidance instead of search, we reduce the per problem inference limit from 200000 to 20000 and the bigstep frequency from 2000 to 200. Hence the overall search budget is reduced by a factor of 10. We use a very large CPU time limit (300 sec) intended to ensure that proof search terminates after exhausting the inference limit.

In this experiment, we examine the effect of regularizing the entropy of our policy predictor. We produce several variants of the GNN policy predictor which differ in the entropy coefficient $\alpha$ used in its training. Table 1 summarizes our results. We find that the entropy coefficient has a big impact on performance. By the 10th iteration, the best GNN predictor with $\alpha=0.7$ is $17\%$ better than the unregularized GNN and $5\%$ better than XGBoost. Table 1 also shows the average entropy of the policies generated by the predictor during the proof search. Note that the average entropy of the best predictor in most iterations is reasonably close (often the closest) to the entropy of the XGBoost predictor. This suggests that one key strength of the XGBoost predictor is that it hits the “right” amount of entropy. Matching this entropy in the GNN with adequate regularization allows for matching and even surpassing XGBoost in performance.

Table 1 reveals that there is a reasonable match in average entropy between XGBoost policies and our best GNN policies. Note, however, that this is in general measured on different proof states as the policies themselves determine what proof states the prover explores. To gain a deeper understanding, we create a separate dataset of proof states and compare the different GNNs from Experiment 1 with XGBoost on these proof states using the following four metrics: 1) fraction of proof states where the two predictors have the same most probable inference (Best), 2) fraction of proof states where the two predictors yield the same inference ordering (Order), and the average KL divergence (relative entropy) between the predictors in both directions: 3) $KL(X\lVert G)$ and 4) $KL(G\lVert X)$.⁶⁶6$X$ and $G$ stand for the probability distributions predicted by XGBoost and GNN, respectively. We contrast these metrics with the number of problems solved (Succ) by the corresponding entropy regularized GNN.

We perform this comparison using two datasets. These are the set of states visited by an unguided prover on the 1) M2k dataset and the 2) MPTP2078 bushy benchmark. The first set is part of the training corpus, while the second was never seen by the predictors before. The results can be seen in Table 2.

Changing the entropy coefficient mostly does not change the order of actions, as expected. For the two datasets, the GNN and the XGBoost predictors select the same best inference in around $80\%$ and $58\%$ of the states and yield exactly the same inference ordering in around $40\%$ and $22\%$ of the states. This reveals a significant diversity among the two predictor families, suggesting potential in combining them. We leave this direction for future work.

We find that the same level of entropy regularization ($\alpha=0.7$) is the best when running both on the familiar (M2k) and the previously unseen (MPTP2078) dataset. This is where the two directional KL divergences (relative entropies) roughly coincide and their sum is roughly minimal. These results make a stronger case for the hypothesis from Experiment 1, that the best GNN performance is obtained when the policy distributions are statistically close to those of the XGBoost predictor.

Tables 1 and 2 demonstrate the importance of the entropy of the inference policy in ATP performance. To make this even more apparent, we design an experiment in which we remove a large part of the information contained in the inference policy, only preserving the inference ordering and the normalized entropy. The top two lines of Table 3 show the normalized entropy across iterations of the XGBoost and GNN predictors. Note that it is very stable. We select a target normalized entropy $H^{*}$ and for each length $l$ we generate a fixed random discrete probability $p_{l}$ of length $l$ whose normalized entropy is $H^{*}$. Finally, we run an MCTS evaluation in which each time our policy predictor emits a probability vector of length $l$, we replace it with $p_{l}$, permuted so that the ordering remains the same as in the original policy. Table 3 shows the ATP performance for the differently normalized entropy targets.

We find that the performance of this predictor is surprisingly good: its performance (1154) is only $1\%$ worse than XGBoost (1171), $10\%$ better than unregularized GNN (1050) and $6\%$ worse than the best GNN (1228). This suggests that the right inference ordering plus the right amount of entropy capture most of the benefits of the learned inference guidance.

As noted in Section 3, tuning the softmax temperature is an alternative to entropy regularization. For XGBoost, the temperature was previously optimized to be $T=2$ and all reported experiments use this number. For the GNN predictors, we used the default $T=1$. In Table 4, we show how the ATP performance of the GNN changes after it has been trained for 10 iterations on the M2k dataset (without entropy regularization). Increasing the temperature brings some improvement, however, this is much smaller than the benefit of entropy regularization. This is true even if we take the best temperature ($T=4$) and perform a full 10 iteration training with this temperature, as shown in Table 5. We obtain $3\%$ improvement via the temperature optimization, compared with $17\%$ improvement via the entropy regularization. We conclude that the effect of entropy regularization is much more refined and powerful than just flattening the probability curve.

Finally, we perform a large evaluation of plCoP using XGBoost and GNN on the full Mizar40 dataset, and we compare its performance with rlCoP and graphCoP. This evaluation, including the training of the GNNs on the growing sets of proofs generated from the successive proving/learning iterations, takes over 10 days on a large multicore server, and the number of training policy/value examples extracted from the MCTS proof searches goes over 5M in the last iteration.

The 32524 problems are randomly split using a 9:1 ratio into 29272 training problems and 3252 evaluation problems. For consistency, we employ the same split that was used in [25]. Successive predictors are only trained on data extracted from the training problems, but we always evaluate the predictors on both the training and evaluation sets and report the number of proofs found for them. Our results can be found in Table 6, with plCoP/GNN solving in the last iteration 16906 training problems and 1767 evaluation problems. These are the highest numbers obtained so far with any learning-guided leanCoP-based system.

For training the GNN policy predictor, we use the entropy regularization coefficient ($\alpha=0.7$) that worked best on M2k, without its further tuning on this larger dataset. Note that the resource limits are higher in Table 6 for rlCoP and also a bit different for graphCoP (which was run only for a few iterations), as we took their published results from [25, 32] rather than rerunning the systems. Also, the evaluation of plCoP with GNN was stopped after iteration 8 due to our resource limits and the clear flattening of the performance on the evaluation set (1767 vs 1758 in the 8th vs 7th iteration).

In particular, plCoP was given 20000 inferences per problem, i.e., one tenth of the inference limit used for rlCoP in [25]. For a fair comparison with rlCoP, we thus take the predictors (both XGBoost and GNN) used in the last plCoP iteration (iteration 10 for XGBoost and iteration 8 for GNN) and run plCoP with them on the evaluation set with 200000 inference limit and 2000 bigstep frequency, which corresponds to the limits used for rlCoP in [25]. To ensure that the system has enough time to exhaust its inference limit, we increase the timeout to 6000 seconds. plCoP with XGBoost then solves 1499 of the evaluation problems while plCoP with GNN solves 1907 (58.6%) of them. This is our final evaluation result, which is 17.4% higher than the 1624 evaluation problems solved by rlCoP in the best previously published result so far [25].