Thus, assuming *λ* is a vector of the score of each strategy, the highest probability permutation indexes the strategies in decreasing order of scores. Conversely, the highest probability permutation can be obtained efficiently by sorting the indices of *λ* with respect to their corresponding values in decreasing order. Cao et al. [4] have presented a proof of Theorem 1, and Cheng et al. [5] have discussed some further interesting details.

*Example 1.* Let *λ* = [1, 9]- , *π*(1) = [1, 2] and *π*(2) = [2, 1]- . Then,

$$\Pr(\mathcal{II} = \pi^{(1)}; \lambda) = \frac{\lambda\_{\pi\_1^{(1)}}}{\lambda\_{\pi\_1^{(1)}} + \lambda\_{\pi\_2^{(1)}}} \cdot \frac{\lambda\_{\pi\_2^{(1)}}}{\lambda\_{\pi\_2^{(1)}}} = \frac{1}{1 + 9} \cdot \frac{9}{9} = \frac{1}{10}.$$

Similarly, Pr(*Π* = *π*(2);*λ*)=9/10.

**Theorem 2.** Perm(c*λ*) = Perm(*λ*)*, for any scalar constant* c > 0*.*

In other words, the Plakett-Luce distribution is invariant to the scale of the parameter vector.

**Lemma 1.** Perm(exp(*λ* + c)) = Perm(exp(*λ*))*, for any scalar constant* c ∈ R*.*

Lemma 1 follows from Theorem 2, and shows the same distribution is translation invariant if the parameter is exponentiated. Cao et al. [4] give proofs of both.

#### **3 A Maximum Likelihood Model**

We model a strategy schedule as a ranking of known strategies, where each strategy is constructed by a parameter setting and time allocation. A ranking therein is a permutation of strategies, with each strategy retaining its time allocation irrespective of the ordering. We construct, in this section, a model for inference of such permutations that is linear in the parameters.

Suppose we have a repository of N theorems which we test against each of our M known strategies to build a data-set D = {(*π*(i), *x*(i))} N i=1, where *π*(i) is a desirable ordering of strategies for theorem i and *x*(i) is a feature vector representation of the theorem. In Sect. 9, we detail how we instantiated D for our experiments, which serves as an example for any other implementation. We assume that *π*(i) has Plakett-Luce distribution conditioned on *x*(i) such that

$$\Pr(\pi; x, \omega) = \text{Perm}(\varLambda(x, \omega)), \tag{1}$$

where *ω* is a parameter the model must learn and *Λ*(·) is a vector-valued function of range RM >0. We use the notation Λ(·)i to index into the value of *Λ*(·). We

represent our prover strategies with feature vectors {*d*(j)} M j=1. To calculate the score of strategy j using Λ(·)j , we specify

$$A(\mathbf{z}^{(i)}, \omega)\_j = \exp\left(\phi(\mathbf{z}^{(i)}, \mathbf{d}^{(j)})^\mathsf{T}\omega\right) \tag{2}$$

to ensure that the scores are positive valued, where *φ* is a suitable basis expansion function. Assuming the data is i.i.d, the likelihood of the parameter vector is given by

$$\mathcal{L}(\omega) = p(\mathcal{D}; \omega) = \prod\_{i=1}^{N} \Pr(\pi^{(i)}; A(x^{(i)}, \omega)).\tag{3}$$

An *ω*ˆ that maximizes this likelihood can then be used to forecast the distribution over permutations for a new theorem *x*∗ by evaluating Perm(*Λ*(*x*∗, *ω*ˆ )) for all permutations. This would incur factorial complexity; however, we are often only interested in the most likely permutation, which can be retrieved in polynomial time. Specifically for strategy scheduling the permutation with the highest predicted probability should reflect the orderings in the data. For this purpose, we use Theorem 1 to find the highest probability permutation *π*∗ by sorting the values of {*Λ*(*x*∗, *ω*ˆ )j} M j=1 in descending order.

*Remark 1.* A method named ListNet designed to rank documents for search queries using the Plakett-Luce distribution is evaluated by Cao et al. [4]. Their evaluation uses a linear basis expansion. We can derive a similar construction in our model by setting

$$\phi(\mathbf{z}^{(i)}, \mathbf{d}^{(j)}) = [\mathbf{z}^{(i)\mathsf{T}}, \mathbf{d}^{(j)\mathsf{T}}]^\mathsf{T}.\tag{4}$$

*Remark 2.* The likelihood in Equation (3) can be maximized by minimizing the negative log likelihood (*ω*) = − log L(*ω*), which (as shown by Sch¨afer and H¨ullermeier [26]) is convex and therefore can be minimized using gradient-based methods. The minima may, however, be unidentifiable due to translation invariance, as demonstrated by Lemma 1. This problem is eliminated in our Bayesian model by the use of a Gaussian prior, as explained in Sect. 4.

*Example 2.* Let there be N = 2 theorems and M = 2 strategies. Let the theorems and strategies be characterized by univariate values such that x(1) = 1, x(2) = 2, d(1) = 1 and d(2) = 2.

Suppose strategy d(1) is ideal for theorem x(1) and strategy d(2) for x(2), as shown on the right, where a + indicates the preferred strategy. d(1) d(2) x(1) + − x(2) − +

This is evidently an example of a parity problem [34], and hence cannot be modelled by a simple linear expansion using the basis function mentioned in Remark 1. A solution in this instance is to use

$$
\phi(x^{(i)}, d^{(j)}) = x^{(i)} \cdot d^{(j)}.
$$

The parameter ω is then one-dimensional, and the required training data takes the form D = {([1, 2]-, 1),([2, 1]-, 2)}. We find that L(w) is convex, with maxima at ˆω = 0.42 as shown in Fig. 1.

**Fig. 1.** The likelihood function in Example 2.

#### **4 Bayesian Inference**

We place a Gaussian prior distribution on the parameter *ω* of the model described in Sect. 3. This has two advantages: first, the posterior mode is identifiable, as noted by Johnson et al. [11] and demonstrated in Example 3 on page 7; second, the parameter is regularized. With this prior specified as the normal distribution

$$
\omega \sim \mathcal{N}(m\_0, \mathbf{S\_0}), \tag{5}
$$

and assuming *π* is independent of D given (*x*, *ω*), the posterior predictive distribution is

$$p(\boldsymbol{\pi}|\boldsymbol{x}^\*, \mathcal{D}) = \int p(\boldsymbol{\pi}|\boldsymbol{x}^\*, \boldsymbol{\omega}) p(\boldsymbol{\omega}|\mathcal{D}) d\boldsymbol{\omega},$$

which may be approximated by sampling from the posterior,

$$
\omega^s \sim p(\omega|\mathcal{D}),
\tag{6}
$$

to obtain

$$p(\boldsymbol{\pi}|\boldsymbol{x}^\*, \mathcal{D}) \approx \frac{1}{S} \sum\_{s=1}^S p(\boldsymbol{\pi}|\boldsymbol{x}^\*, \boldsymbol{\omega}^s). \tag{7}$$

Given a new theorem *x*∗, to find the permutation of strategies with the highest probability of success, using the approximation above would require its evaluation for every permutation of *π*. This process incurs factorial complexity. We instead make a Bayes point approximation [16] using the mean values of the samples such that,

$$\begin{array}{rcl}p(\pi|x^\*,\mathcal{D}) \approx & p(\pi|x^\*,\langle\omega^s\rangle) \quad \text{using Eq. (7)}\\ =& \Pr(\pi|A(x^\*,\langle\omega^s\rangle)) \text{ using Eq. (1),}\end{array}$$

where · denotes mean value. The mean of the Plakett-Luce parameter for Bayesian inference has been used in prior work [8] to obtain good results. Furthermore, using that, the highest probability permutation can be obtained by using Theorem 1, thereby incurring only the cost of sorting the items. This saving is substantial when generating a strategy schedule, because it saves on prediction time, which is important for the following reason.

#### **Algorithm 1.** Metropolis-Hastings Algorithm

Suppose we have generated samples {*ω*(1)*,..., ω*(*i*) } from the *target distribution p*. Generate *ω*(*i*+1) as follows.

1: Generate candidate value *ω*˙ ∼ *q*(*ω*(*i*) ), where *q* is the *proposal distribution*.

2: Evaluate *r* ≡ *r*(*ω*(*i*) *, ω*˙ ) where

$$r(x,y) = \min\left\{\frac{p(y)}{p(x)}\frac{q(x|y)}{q(y|x)}, 1\right\}.$$

3: Set

*ω*(*i*+1) = *ω*˙ with probability *r ω*(*i*) with probability 1 − *r.*

*Remark 3.* While benchmarking and in typical use, a prover is allocated a fixed amount of time for a proof attempt, and any time taken to predict a strategy schedule must be accounted for within this allocation. Time taken for this prediction is time taken away from the prover itself which could have been invested in the proof search. Therefore, it is essential to minimize schedule prediction time. It is particularly wise to favour a saving in prediction time at the cost of model optimization and training time.

*Remark 4.* In our implementation we set *m*0 = 0. This has the effect of prioritizing smaller weights *ω* in the posterior. Furthermore, we set *S*0 = η*I*, η ∈ R, where *I* is the identity matrix. Consequently, the hyperparameter η controls the strength of the prior, since the entropy of the Gaussian prior scales linearly by log |*S*0|.

*Remark 5.* A specialization of the Plakett-Luce distribution using the Thurstonian interpretation admits a Gamma distribution conjugate prior [8]. That, however, is unavailable to our model when parametrized as shown in Eq. (1).

#### **5 Sampling**

We use the Markov chain Monte Carlo (MCMC) Metropolis-Hastings algorithm [38] to generate samples from the posterior distribution. In MCMC sampling, one constructs a Markov chain whose stationary distribution matches the target distribution p. For the Metropolis-Hastings algorithm, stated in Algorithm 1, this chain is constructed using a proposal distribution y|x ∼ q, where q is set to a distribution that can be conveniently sampled from.

Note that while calculating r in Algorithm 1, the normalization constant of the target density p cancels out. This is to our advantage; to generate samples *ω*s from the posterior, which is, by Eq. (3) and Eq. (5),

$$\begin{split}p(\omega|\mathcal{D}) &\propto p(\mathcal{D}|\omega)p(\omega) \\ &= \mathcal{L}(\omega)\mathcal{N}(m\_{\mathbf{0}}, \mathbf{S\_{0}}),\end{split} \tag{8}$$

the posterior only needs to be computed in this unnormalized form.

In this work, we choose a random walk proposal of the form

$$q(\omega'|\omega) = \mathcal{N}(\omega'|\omega, \Sigma\_q),\tag{9}$$

and tune Σq for efficient sampling simulation. We start the simulation at a local mode *ω*ˆ , and set N (*ω*ˆ , Σq) to approximate the local curvature of the posterior at that point using methods by Rossi [25]. Specifically, our procedure for computing Σq is as follows.

#### 1. First, writing the posterior from Eq. (8) as

$$p(\omega|\mathcal{D}) = \frac{1}{Z}e^{-E(\omega)},$$

where Z is the normalization constant, we have

$$E(\omega) = -\log \mathcal{L}(\omega) - \log \mathcal{N}(m\_\mathbf{0}, \mathbf{S\_0}).\tag{10}$$

We find a local mode *ω*ˆ by optimizing E(*ω*) using a gradient-based method.

2. Then, using a Laplace approximation [2], we approximate the posterior in the locality of this mode to

$$\mathcal{N}(\hat{\omega}, H^{-1}), \text{ where } H = \nabla \nabla E(\omega)|\_{\hat{\omega}}.$$

is the Hessian matrix of E(*ω*) evaluated at that local mode.

3. Finally, we set

$$
\Sigma\_q = s^2 \, H^{-1}
$$

in Eq. (9), where s is used to tune all the length scales. We set this value to s2 = 2.38 based on the results by Roberts and Rosenthal [24].

*Remark 6.* When calculating r in Algorithm 1 during sampling, to evaluate the unnormalized posterior at any point *ω*s we compute it from Equation (10) as exp(−E(*ω*s))—it is therefore the only form in which the posterior needs to be coded in the implementation.

*Example 3 (Gaussian Prior).* To demonstrate the effect of using a Gaussian prior, we build upon Example 2, with the data taking the form

$$\mathcal{D} = \{ ([1,2]\mathsf{I},1), ([2,1]\mathsf{I},2) \}.$$

We perform basis expansion as explained in Sect. 6 with prior parameter η = 1.0, kernel σ = 0.1 and ς = 2 centres. Thus, the model parameter is

$$
\omega = [\omega\_1, \omega\_2]^\mathsf{T}, \quad \omega \in \mathbb{R}^2.
$$

The unnormalized negative log posterior E(ω1, ω2), as defined in Eq. (10), is shown in Fig. 2b; and the negative log likelihood (ω1, ω2) = − log L(ω1, ω2) as mentioned in Remark 2, is shown in Fig. 2a. Note the contrast in the shape of the two surfaces. The minimum is along the top-right portion in Fig. 2a, which is flat and leads to an unidentifiable point estimate, whereas in Fig. 2b, the minimum is in a narrow region near the centre. The Gaussian prior, in informal terms, has lifted the surface up, with an effect that increases in proportion to the distance from the origin.

**Fig. 2.** Comparison of the shape of the likelihood and the posterior functions.

#### **6 Basis Expansion**

Example 2 shows how the linear expansion in Remark 1 is ineffective even in very simple problem instances. The maximum likelihood bilinear model presented by Sch¨afer and H¨ullermeier [26] is related to our model defined in Sect. 2 with the basis performing the Kronecker (tensor) product *φ*(x, d) = x ⊗ d. Their results show such an expansion produces a competitive model, but falls behind in comparison to their non-linear model.

To model non-linear interactions between theorems and strategies, we use a *Gaussian kernel* for the basis expansion.

**Definition 3 (Gaussian Kernel).** *A Gaussian kernel* κ *is defined by*

$$\kappa(\mathbf{y}, \mathbf{z}) = \exp\left(-\frac{||\mathbf{y} - \mathbf{z}||^2}{2\sigma^2}\right), \quad \text{for } \sigma > 0.1$$

The Gaussian kernel κ(*y*, *z*) effectively represents the inner product of *y* and *z* in a Hilbert space whose bandwidth is controlled by σ. Smaller values of σ correspond to a higher bandwidth, more flexible, inner product space. Larger values of σ will reduce the kernel to a constant function, as detailed in [30]. For our ranking model, we must tune σ to balance between over-fitting and under-performance.

We use the Gaussian kernel for basis expansion by setting

$$\phi(x,d) = \left[\kappa\left([x^{\mathsf{T}},d^{\mathsf{T}}]^{\mathsf{T}},c^{(1)}\right),\ldots,\kappa\left([x^{\mathsf{T}},d^{\mathsf{T}}]^{\mathsf{T}},c^{(C)}\right)\right]^{\mathsf{T}},$$

where {*c*(i)} C i=1 is a collection of *centres*. By choosing centres to be themselves composed of theorems *x*(.) and strategies *d*(.) , such that *c*(.) = [*x*(.)- , *d*(.)- ] - , the basis expansion above represents each data item with a non-linear inner product against other known items.

To find the relevant subset of D from which centres should be formed, we follow the method described in the steps below.

$$
\Gamma\_{i,j} = \phi(\mathbf{c}^{(i)})\_j = \kappa(\mathbf{c}^{(i)}, \mathbf{c}^{(j)}) .
$$

This method is inspired by the procedure used in Relevance Vector Machines [35] for a similar purpose.

*Remark 7 (score).* For a strategy that succeeds in proving a theorem, the score for the pair is the fraction of the time allocation left unconsumed by the prover. For an unsuccessful strategy-theorem combination, we set the score to a value close to zero.

*Remark 8 (*ς*).* The parameter ς is another tunable parameter which, in similar fashion to the parameter σ earlier in this section, controls the model complexity introduced by the basis expansion. Both variables must be tuned together.

#### **7 Model Selection and Time Allocations**

From Remark 8, ς and σ are hyperparameters that control the complexity introduced into our model through the Gaussian basis expansion; and Remark 4 introduces η, the hyperparameter that controls the strength of the prior. The final model is selected by tuning them. Tuning must aim to avoid overfitting to the training data; and to maximize, during testing, either the savings in proof-search time or the number of theorems proved. However, we do not have a closed-form expression relating these parameters to this aim, thus any combination of the parameters can be judged only by testing them.

In this work we have used *Bayesian optimization* [29] to optimize these hyperparameters. Bayesian optimization is a black-box parameter optimization method that attempts to search for a global optimum within the scope of a set resource budget. It models the optimization target as a user-specified *objective function*, which maps from the parameter space to a loss metric. This model of the objective function is constructed using *Gaussian Process* (GP) regression [22], using data generated by repeatedly testing the objective function.

Our specified objective function maps from the hyperparameters (ς, σ, η) to a loss metric ξ. We use cross-validation within the training data while calculating ξ to penalize hyperparameters that over-fit. Hyperparameters are tuned at training time only, after which they are fixed for subsequent testing. The final test set is never used for any hyperparameter optimization.

In the method presented thus far we are only permuting strategies with fixed time allocations to build a sequence for a strategy schedule. In this setting, the number of theorems proved cannot change, but the time taken to prove theorems can be reduced. Therefore, with this aim, a useful metric for ξ is the total time taken by the theorem prover to prove the theorems in the cross-validation test set.

However, we can take further advantage of the hyperparameter tuning phase to additionally tune the times allocated to each strategy, by treating these times as hyperparameters. Therefore, for each strategy *d*(i) we create a hyperparameter ν(i) ∈ (0, 1) which sets the proportion of the proof time allocated to that strategy. We can then optimize our model to maximize the number of theorems proved; a count of the remaining theorems is then a viable metric for ξ. Note that once the ν(·) are set, time allocation for *d*(i) is fixed to ν(i) , irrespective of its order in the strategy schedule.

*Remark 9.* Our results include two types of experiment:

# **8 Training Data and Feature Extraction**

Our chosen theorem prover, iLeanCoP, is shipped with a fixed strategy schedule consisting of 5 strategies. It splits the allocated proof time across the first four strategies by 2%, 60%, 20% and 10%. However, only the first strategy is complete and therefore usually expected to take up its entire time allocation. The remaining strategies are incomplete, and may exit early on failure. Therefore, the fifth and final strategy, which we refer to as the fallback strategy, is allocated all the remaining time.

**Emulating iLeanCop.** We have constructed a dataset by attempting to prove every theorem in our problem library using each of these strategies individually. With this information, the result of any proof attempt can be calculated by emulating the behaviour of iLeanCoP. This is how we evaluate the predicted schedules—we emulate a proof attempt by iLeanCoP using that schedule for each theorem in the test set. For a faithful emulation of the fallback strategy, it is always attempted last, and therefore any new schedule is only a permutation of the first four strategies. Our experiments allocate a time of 600 s per theorem. The dataset is built to ensure that, within this proof time, any such strategy permutation can be emulated. We kept a timeout of 1200 s per strategy per theorem when building the dataset, which is more than sufficient for current experiments and gives us headroom for future experiments with longer proof times.

**Strategy Features.** Each strategy in iLeanCoP consists of a time allocation and parameter settings; the parameters are described by Otten [19]. We use a one-hot encoding feature representation for strategies based on the parameter setting as shown in Table 1. Another feature noting the completeness of each strategy is also shown. Another feature (not shown in the table) contains the time allocated to each strategy. Note the fallback strategy is used in prover emulation but not in the schedule prediction.

**Table 1.** Features of the four main strategies.

**Theorem Features.** The TPTP problem library contains a large, comprehensive collection of theorems and is designed for testing automated theorem provers. The problems are taken from a range of domains such as Logic Calculi, Algebra, Software Verification, Biology and Philosophy, and presented in multiple logical forms. For iLeanCoP, we select the subset in first-order form, denoted there as FOF. In version 7.1.0, there are 8157 such problems covering 43 domains. Each problem consists of a set of formulae and a goal theorem. The problems are of varying sizes. For example, the problem named HWV134+1 from the Hardware Verification domain contains 128975 formulae, whilst SET703+4 from the Set Theory domain contains only 12.

We have constructed a dataset containing features extracted from the firstorder logic problems in TPTP (see Appendix A). Here, we describe how those features were developed.

In deployment, a prover using our method to generate strategy schedules would have to extract features from the goal theorem at the beginning of a proof attempt. To minimize the computational overhead of feature extraction, in keeping with our goal noted in Remark 3, we use features that can be collected when the theorem is parsed by the prover. The collection of features developed in this work is based on the authors' prior experience, and later we will briefly examine the quality of each feature to discard the uninformative ones. We extract the following features, which are all considered candidates for the subsequent feature selection process.

**Quantifier Alternations:** A count of the number of times the quantifiers flip between the existential and universal. When calculated by examining only the sequence of lexical symbols, the count may be inaccurate. An accurate count is obtained by tracking negations during parsing while collecting quantifiers. We extract both as candidates.

**Feature Selection and Pre-processing.** We examine the degree of association between the individual theorem features described above and the speed with which the strategies solve each theorem; for this we use the Maximal Information Coefficient (MIC) measure [23]. For every theorem we calculate the score, as defined in Remark 7, averaged over all strategies. This score is paired with each feature to calculate its MIC. Most lexical symbols achieve an MIC close to zero. We selected the features with relatively high MIC for the presented work, and these are shown in Fig. 3.

The two features based on quantifier alternations are clearly correlated, but both meet the above criterion for selection. Correlations can also be expected between the other features. Furthermore, our features range over different scales. For example, the maximal function arity in TPTP averages 2, whereas the number of predicate symbols averages 2097. It is desirable to remove these correlations to alleviate any burden on the subsequent modelling phase, and to standardize the features to zero mean and unit variance to create a feature space with similar length-scales in all dimensions. The former is achieved by *decorrelation*, the latter by *standardization*, and both together by a *sphering transformation*.

**Fig. 3.** MIC between selected features and scores.

We transform our extracted features as such using Zero-phase Component Analysis (ZCA), which ensures the transformed data is as close as possible to the original [6].

**Coverage.** As mentioned above, we run iLeanCoP on every first-order theorem in TPTP with each strategy allocated 1200 s. Although every theorem in intuitionistic logic also holds for classical logic, the converse does not hold. For that reason and because of the limitations of iLeanCoP, many theorems remain unproved by any strategy. We exclude these theorems from our experiments, leaving us with a data-set of 2240 theorems.

#### **9 Experiments**

We present two experiments in this work, as noted in Remark 9. In this section, we describe our experimental apparatus in detail.

As noted in Sect. 8, our data contains:

This data needs to be presented to our model for training in the form of D = {(*π*(i), *x*(i))} N i=1, as described in Sect. 3. Since the two experiments have slightly different goals, we specialize D according to each.

When aiming to predict schedules that minimize the time taken to prove theorems, a natural value for *π*(i) is the index order that sorts strategies in increasing amounts of time taken to prove theorem i. However, some strategies may fail to prove theorem i within their time allocation. In that case, we consider the failed strategies equally bad and place them last in the ordering in *π*(i). Furthermore, we create additional items (*π*(i), *x*(i)) in D, by permuting the positions of the failed strategies in *π*(i) to create multiple *π*(i).

When the goal is only to prove more theorems, the strategies that succeed are all considered equally ranked above the failed strategies. In this mode, the successful strategies are similarly permuted in the data, in addition to those that failed.

In each experiment, a random one-third of the N theorems are separated into a *holdout* test set *N*˙ , leaving behind a training set *N*¨ . This training set is first used for hyperparameter tuning using BO. As explained in Sect. 7, each hyperparameter combination is tested with five-fold cross-validation within *N*¨ , to penalize instances that overfit to *N*¨ . This results in estimated optimum values for the hyperparameters. These are used to set the model, which is then trained on *N*¨ and then finally evaluated on *N*˙ . The whole process is repeated ten times with new random splits *N*˙ and *N*¨ to create one set of ten results for that experiment.

### **10 Results**

Each experiment, repeated ten times, is conducted in two phases: first, hyperparameter optimization; and second, model training and evaluation. The bounds on the search space in the first phase were always the same (see Appendix A). The holdout test set contained 747 theorems. A proof time of 600 s was emulated.

#### **10.1 Experiment 1: Optimizing Proof Attempt Time**

The results are shown in Fig. 4. The total prediction time for all 747 theorems, averaged across the trials, is 0.14 s.

The times across proof attempts are not normally distributed, for both the unmodified iLeanCoP schedule and the predicted ones, as confirmed by a Jarque-Bera test. Therefore, we used the right-tailed Wilcoxon signed-rank test for a pair-wise comparison of the times taken for each theorem by the original schedule in iLeanCoP versus the predicted schedules, resulting in a p-value of less

**Fig. 4.** Results of Experiment 1. Proof times are compared with precision 10*−*6s.

than 10−6 in each trial, confirming the alternate hypothesis that the reduction in time taken to prove each theorem comes from a distribution with median greater than zero. This confirms that the time savings are statistically significant. Furthermore, we note from Fig. 4 a saving of more than 50% in the total proof-time in each trial.

#### **10.2 Experiment 2: Proving More Theorems**

We set our hyperparameter search to find time allocations for strategies. The resulting predicted schedules have gains and losses when compared to the original schedule, as shown in the four facets of Fig. 5. However, there is a consistent gain in the number of theorems proved and a gain of five theorems on average, evident from the mean values in (†) and (‡).

**Fig. 5.** Comparison of the proof attempts by the original (orig.) and predicted (pred.) schedules in Experiment 2. Theorems which are proved by pred. but could not be proved by orig. are counted in †, and the vice versa in ‡.

#### **11 Related Work**

Prior work on machine learning for *algorithm selection*, such as that introduced by Leyton-Brown et al. [13], is a precursor to our work. In that topic, the machine learning methods must perform the task of selecting a good algorithm from within a portfolio to solve the given problem instance. Typically, as was the case in the work by Leyton-Brown et al. [13], the learning methods predict the runtime of all algorithms, and then pick the fastest predicted one. This line of enquiry has been extended to select algorithms for SMT solvers—a recent example is MachSMT by Scott et al. [28]. The machine learning models in MachSMT are trained by considering all the portfolio members in pairs for each problem in the training set. This method is called *pairwise ranking*, which contrasts from our method, called *list-wise ranking*, in which we consider the full list of portfolio members all together.

In terms of the machine learning task, the work on scheduling solvers bears greater similarity to our presented work. In MedleySolver, for example, Pimpalkhare et al. [20] frame this task as a multi-armed bandit problem. They predict a sequence of solvers as well as the time allocation for each to generate schedules for the goal problems. MedleySolver is able to solve more problems than any individual solver would on its own.

With an approach that contrasts with ours, H˚ula et al. [10] have made use of Graph Neural Networks (GNNs) for solver scheduling. They produce a regression model to predict, for the given problem, the runtime of all the solvers; which is used as the key to sort the solvers in increasing order of predicted runtime to build a schedule. This is an example of *point-wise ranking*. The authors use GNNs to automatically discover features for machine learning. They combine this feature extraction with training of the regression model. They achieve an increase in the number of problems solved as well as a reduction in the total proof time. Meanwhile, our use of manual feature engineering combined with statistical methods for selection and normalization has certain advantages. For one, we can analyse our features and derive a subjective interpretation of their efficacy. Additionally, our features effectively impart our domain knowledge onto the model. Such domain knowledge may not be available in the data itself. Manual feature engineering such as ours can be combined with automatic feature extraction to reap the benefits of both.

# **12 Conclusions**

We have presented a method to specialize, for the given goal theorem, the sequence of strategies in the schedule used in each proof attempt. A Bayesian machine learning model is trained in this method using data generated by testing the prover of interest. When evaluated with the iLeanCoP prover using the TPTP library as a benchmark, our results show a significant reduction in the time taken to prove theorems. For theorems that are successfully proved, the average time saving is above 50%. The prediction time is on average low enough to have a negligible impact on the resources subtracted from the proof search itself.

We also extend this method to optimize time allocations to each strategy. In this setting, our results show a notable increase in the number of theorems proved.

This work shows, by example, that Bayesian machine learning models designed specifically to augment heuristics in theorem provers, with detailed consideration of the computational compromises required in this setting, can deliver substantial improvements.

**Acknowledgments.** Initial investigations for this work were co-supervised by Prof. Mateja Jamnik, Computer Laboratory, University of Cambridge, UK.

This work was supported by: the UK Engineering and Physical Sciences Research Council (EPSRC) through a Doctoral Training studentship, award reference 1788755; and the ERC Advanced Grant ALEXANDRIA (Project GA 742178). For the purpose of open access, the author has applied a Creative Commons Attribution (CC-BY-4.0) licence to any Author Accepted Manuscript version arising.

Computations for this work was performed using resources provided by the Cambridge Service for Data Driven Discovery (CSD3) operated by the University of Cambridge Research Computing Service, provided by Dell EMC and Intel using Tier-2 funding from the Engineering and Physical Sciences Research Council (capital grant EP/P020259/1), and DiRAC funding from the Science and Technology Facilities Council.

#### **A Implementation, Code and Data**

This work is implemented primarily in Matlab [36]. All experiments can be reproduced using the code, data and instructions available at [15]. The hyperparameter search space in all experiments was restricted to ς ∈ [10, 300], σ ∈ [0.01, 100.0] and η ∈ [1, 100].

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# A Framework for Approximate Generalization in Quantitative Theories

Temur Kutsia(B) and Cleo Pau

RISC, Johannes Kepler University Linz, Linz, Austria<EMAIL_ADDRESS>
Abstract. Anti-unification aims at computing generalizations for given terms, retaining their common structure and abstracting differences by variables. We study quantitative anti-unification where the notion of the common structure is relaxed into "proximal" up to the given degree with respect to the given fuzzy proximity relation. Proximal symbols may have different names and arities. We develop a generic set of rules for computing minimal complete sets of approximate generalizations and study their properties. Depending on the characterizations of proximities between symbols and the desired forms of solutions, these rules give rise to different versions of concrete algorithms.

Keywords: Generalization · Anti-unification · Quantiative theories · Fuzzy proximity relations

## 1 Introduction

Generalization problems play an important role in various areas of mathematics, computer science, and artificial intelligence. Anti-unification [12,14] is a logicbased method for computing generalizations. Being originally used for inductive and analogical reasoning, some recent applications include recursion scheme detection in functional programs [4], programming by examples in domainspecific languages [13], learning bug-fixing from software code repositories [3,15], automatic program repair [7], preventing bugs and misconfiguration in services [11], linguistic structure learning for chatbots [6], to name just a few.

In most of the existing theories where anti-unification is studied, the background knowledge is assumed to be precise. Therefore, those techniques are not suitable for reasoning with incomplete, imprecise information (which is very common in real-world communication), where the exact equality is replaced by its (quantitative) approximation. Fuzzy proximity and similarity relations are notable examples of such extensions. These kinds of quantitative theories have many useful applications, some most recent ones being related to artificial intelligence, program verification, probabilistic programming, or natural language processing. Many tasks arising in these areas require reasoning methods and computational tools that deal with quantitative information. For instance, approximate inductive reasoning, reasoning and programming by analogy, similarity detection in programming language statements or in natural language texts could benefit from solving approximate generalization constraints, which is a theoretically interesting and challenging task. Investigations in this direction have been started only recently. In [1], the authors proposed an anti-unification algorithm for fuzzy similarity (reflexive, symmetric, min-transitive) relations, where mismatches are allowed not only in symbol names, but also in their arities (fully fuzzy signatures). The algorithm from [9] is designed for fuzzy proximity (i.e., reflexive and symmetric) relations with mismatches only in symbol names.

In this paper, we study approximate anti-unification from a more general perspective. The considered relations are fuzzy proximity relations. Proximal symbols may have different names and arities. We consider four different variants of relating arguments between different proximal symbols: unrestricted relations/functions, and correspondence (i.e. left- and right-total) relations/functions. A generic set of rules for computing minimal complete sets of generalizations is introduced and its termination, soundness and completeness properties are proved. From these rules, we obtain concrete algorithms that deal with different kinds of argument relations. We also show how the existing approximate anti-unification algorithms and their generalizations fit into this framework.

*Organization:* In Sect. 2 we introduce the notation and definitions. Section 3 is devoted to a technical notion of term set consistency and to an algorithm for computing elements of consistent sets of terms. It is used later in the main set of anti-unification rules, which are introduced and characterized in Sect. 4. The concrete algorithms obtained from those rules are also described in this section. In Sect. 5, we discuss complexity. Section 6 offers a high-level picture of the studied problems and concludes.

An extended version of this work can be found in the technical report [8].

## 2 Preliminaries

Proximity Relations. Given a set S, a mapping R from S ˆ S to the real interval [0, 1] is called a binary *fuzzy relation* on S. By fixing a number λ, 0 ď λ ď 1, we can define the crisp (i.e., two-valued) counterpart of R, named the λ*-cut* of R, as Rλ :" {ps1, s2q | Rps1, s2q ě λ}. A fuzzy relation R on a set S is called a *proximity relation* if it is reflexive (Rps, sq " 1 for all s P S) and symmetric (Rps1, s2q " Rps2, s1q for all s1, s2 P S). A T-norm ^ is an associative, commutative, non-decreasing binary operation on [0, 1] with 1 as the unit element. We take minimum in the role of T-norm.

Terms and Substitutions. We consider a first-order alphabet consisting of a set of fixed arity function symbols F and a set of variables V, which includes a special symbol \_ (the anonymous variable). The set of *named* (i.e., non-anonymous) variables V\{\_} is denoted by VN. When the set of variables is not explicitly specified, we mean V. The set of terms T pF, Vq over F and V is defined in the standard way: t P T pF, Vq iff t is defined by the grammar t :" x | fpt1,...,tnq, where x P V and f P F is an n-ary symbol with n ě 0. Terms over T pF, VNq are defined similarly except that all variables are taken from VN.

We denote arbitrary function symbols by f, g, h, constants by a, b, c, variables by x, y, z, v, and terms by s, t, r. The *head* of a term is defined as headpxq :" x and headpfpt1,...,tnqq :" f. For a term t, we denote with Vptq (resp. by VNptq) the set of all variables (resp. all named variables) appearing in t. A term is called *linear* if no named variable occurs in it more than once.

The deanonymization operation deanon replaces each occurrence of the anonymous variable in a term by a fresh variable. For instance, deanonpfp\_, x, gp\_qqq " fpy , x, gpyqqq, where y and y are fresh. Hence, deanonptq P T pF, VNq is unique up to variable renaming for all t P T pF, Vq. deanonptq is linear iff t is linear.

The notions of *term depth*, *term size* and a *position in a term* are defined in the standard way, see, e.g. [2]. By t|p we denote the subterm of t at position p and by t[s]p a term that is obtained from t by replacing the subterm at position p by the term s.

A *substitution* is a mapping from VN to T pF, VNq (i.e., without anonymous variables), which is the identity almost everywhere. We use the Greek letters σ, ϑ, ϕ to denote substitutions, except for the identity substitution which is written as *Id*. We represent substitutions with the usual set notation. *Application* of a substitution σ to a term t, denoted by tσ, is defined as \_σ :" \_, xσ :" σpxq, fpt1,...,tnqσ :" fpt1σ, . . . , tnσq. Substitution *composition* is defined as a composition of mappings. We write σϑ for the composition of σ with ϑ.

Argument Relations and Mappings. Given two sets N " {1,...,n} and M " {1,...,m}, a binary *argument relation* over N ˆ M is a (possibly empty) subset of N ˆ M. We denote argument relations by ρ. An argument relation ρ Ď N ˆ M is (i) *left-total* if for all i P N there exists j P M such that pi, jq P ρ; (ii) *right-total* if for all j P M there exists i P N such that pi, jq P ρ. *Correspondence relations* are those that are both left- and right-total.

An *argument mapping* is an argument relation that is a partial injective function. In other words, an argument mapping π from N " {1,...,n} to M " {1,...,m} is a function π : In -→ Im, where In Ď N, Im Ď M and |In|"|Im|. Note that it can be also the empty mapping: π : H -→ H. The inverse of an argument mapping is again an argument mapping.

Given a proximity relation R over F, we assume that for each pair of function symbols f and g with Rpf,gq " α > 0, where f is n-ary and g is m-ary, there is also given an argument relation ρ over {1,...,n}ˆ{1,...,m}. We use the notation f "ρ R,α g. These argument relations should satisfy the following conditions: ρ is the empty relation if f or g is a constant; ρ is the identity if f " g; f "ρ R,α g iff g "ρ´1 R,α f, where ρ´1 is the inverse of ρ.

*Example 1.* Assume that we have four different versions of defining the notion of author (e.g., originated from four different knowledge bases) *author* 1p*first*-name, *middle*-*initial*, *last*-nameq, *author* 2p*first*-name, *last*-nameq, *author* 3p*last*-name, *first*-name, *middle*-*initial*q, and *author* 4p*full*-nameq. One could define the argument relations/mappings between these function symbols e.g., as follows:

$$\begin{aligned} &(a) \mathop{\text{aut}}\nolimits\_{1} \sim\_{\mathbb{R},0,7}^{\{(1,1),(3,2)\}} \mathop{\text{aut}}\nolimits\_{2}, \quad &a \text{other}\_{1} \sim\_{\mathbb{R},0,9}^{\{(3,1),(1,2),(2,3)\}} \mathop{\text{aut}}\nolimits\_{3}, \\ &(a) \mathop{\text{aut}}\nolimits\_{1} \sim\_{\mathbb{R},0,5}^{\{(1,1),(3,1)\}} \mathop{\text{aut}}\nolimits\_{4}, \quad &a \text{other}\_{2} \sim\_{\mathbb{R},0,7}^{\{(1,2),(2,1)\}} \mathop{\text{aut}}\nolimits\_{3}, \\ &(a) \mathop{\text{aut}}\nolimits\_{2} \sim\_{\mathbb{R},0,5}^{\{(1,1),(2,1)\}} \mathop{\text{aut}}\nolimits\_{4}, \quad &a \text{other}\_{3} \sim\_{\mathbb{R},0,5}^{\{(1,1),(2,1)\}} \mathop{\text{aut}}\nolimits\_{4}. \end{aligned}$$

Proximity Relations over Terms. Each proximity relation R in this paper is defined on F Y V such that Rpf,xq " 0 for all f P F and x P V, and Rpx, yq " 0 for all x ‰ y, x, y P V. We assume that R is *strict*: for all w1, w2 P F Y V, if Rpw1, w2q " 1, then w1 " w2. Yet another assumption is that for each f P F, its pR, λq-proximity class {g | Rpf,gq ě λ} is *finite* for any R and λ.

We extend such an R to terms from T pF, Vq as follows:

If Rpt, sq ě λ, we write t »R,λ s. When λ " 1, the relation »R,λ does not depend on R due to strictness of the latter and is just the syntactic equality ". The pR, λq-*proximity class* of a term t is **pc**R,λptq :" {s | s »R,λ t}.

Generalizations. Given R and λ, a term r is an pR, λq-*generalization* of (alternatively, pR, λq-*more general than*) a term t, written as r ÀR,λ t, if there exists a substitution σ such that deanonprqσ »R,λ deanonptq. The strict part of ÀR,λ is denoted by ≺R,λ, i.e., r ≺R,λ t if r ÀR,λ t and not t ÀR,λ r.

*Example 2.* Given a proximity relation R, a cut value λ, constants a "H R,α1 b and b "H R,α2 c, binary function symbols f and h, and a unary function symbol g such that h "{p1,1q,p1,2q} R,α3 f and h "{p1,1q} R,α4 g with αi ě λ, 1 ď i ď 4, we have

The notion of *syntactic generalization* of a term is a special case of pR, λqgeneralization for λ " 1. We write r À t to indicate that r is a syntactic generalization of t. Its strict part is denoted by ≺.

Since R is strict, r À t is equivalent to deanonprqσ " deanonptq for some σ (note the syntactic equality here).

# Theorem 1. *If* r À t *and* t ÀR,λ s*, then* r ÀR,λ s*.*

*Proof.* r À t implies deanonprqσ " deanonptq for some σ, while from t ÀR,λ s we have deanonptqϑ »R,λ deanonpsq for some ϑ. Then deanonprqσϑ »R,λ deanonpsq, which implies r ÀR,λ s. -

Note that r ÀR,λ t and t ÀR,λ s, in general, do not imply r ÀR,λ s due to non-transitivity of »R,λ.

Definition 1 (Minimal complete set of pR, λq-generalizations).  The elements of the* pR, λq*-mcsg of* t1 *and* t2 *are called least general* pR, λq*-generalizations ((*R, λ*)-lggs) of* t1 *and* t2*.*

*This definition directly extends to generalizations of finitely many terms.*

The problem of computing an pR, λq-generalization of terms t and s is called the pR, λq*-anti-unification problem* of t and s. In anti-unification, the goal is to compute their least general pR, λq-generalization.

The precise formulation of the anti-unification problem would be the following: Given R, λ, t1, t2, find an pR, λq-lgg r of t1 and t2, substitutions σ1, σ2, and the approximation degrees α1, α2 such that Rprσ1, t1q " α1 and Rprσ2, t2q " α2. A minimal complete algorithm to solve this problem would compute exactly the elements of pR, λq-mcsg of t1 and t2 together with their approximation degrees. However, as we see below, it is problematic to solve the problem in this form. Therefore, we will consider a slightly modified variant, taking into account anonymous variables in generalizations and relaxing bounds on their degrees.

We assume that the terms to be generalized are ground. It is not a restriction because we can treat variables as constants that are close only to themselves.

Recall that the proximity class of any alphabet symbol is finite. Also, the symbols are related to each other by finitely many argument relations. One may think that it leads to finite proximity classes of terms, but this is not the case. Consider, e.g., R and λ, where h »{p1,1q} R,λ f with binary h and unary f. Then the pR, λq-proximity class of fpaq is infinite: {fpaq} Y {hpa, tq | t P T pF, Vq}. Also, the pR, λq-mcsg for fpaq and fpbq is infinite: {fpxq} Y {hpx, tq | t P T pF, Hq}.

Definition 2.  The* pR, λq*-*relevant proximity class *of* t *is*

**rpc**R,λptq :" {s | s *is a relevant* pR, λq*-proximal term of* t}.

In the example above, position 2 in hpx, tq is irrelevant for generalizing fpaq and fpbq, and hpx, \_q is one of their relevant generalizations. Note that fpxq is also a relevant generalization of fpaq and fpbq, since it contains no irrelevant positions. More general generalizations like, e.g., x, are relevant as well. Similarly, position 2 in hpa, tq is irrelevant for proximity to fpaq and **rpc**R,λpfpaqq " {fpaq, hpa, \_q}. Generally, **rpc**R,λptq is finite for any t due to the finiteness of proximity classes of symbols and argument relations mentioned above.

Definition 3 (Minimal complete set of relevant pR, λq-generalizations). *Given* R*,* λ*,* t1*, and* t2*, a set of terms* T *is a* complete set of relevant pR, λqgeneralizations *of* t1 *and* t2 *if*

*The minimality property is defined as in Definition 1.*

This definition directly extends to relevant generalizations of finitely many terms. We use pR, λq-mcsrg as an abbreviation for minimal complete set of relevant pR, λq-generalization. Like relevant proximity classes, mcsrg's are also finite.

Lemma 1. *For given* R *and* λ*, if all argument relations are correspondence relations, then* pR, λq*-mcsg's and* pR, λq*-proximity classes for all terms are finite.*

*Proof.* Under correspondence relations no term contains an irrelevant position for generalization or for proximity. -

Hence, for correspondence relations the notions of mcsg and mcsrg coincide, as well as the notions of proximity class and relevant proximity class.

For a term r, we define its *linearized version* linprq as a term obtained from r by replacing each occurrence of a named variable in r by a fresh one. For instance, linpfpx, \_, gpy, x, aq, bqq " fpx , \_, gpy , x, aq, bq, where x , x, y are fresh variables. Linearized versions of terms are unique modulo variable renaming.

Definition 4 (Generalization degree upper bound). *Given two terms* r *and* t*, a proximity relation* R*, and a* λ*-cut, the* pR, λq-generalization degree upper bound of r and t, *denoted by* gdubR,λpr, tq*, is defined as follows:*

*Let* α :" max{Rplinprqσ, tq | σ *is a substitution*}*. Then* gdubR,λpr, tq *is* α *if* α ě λ*, and* 0 *otherwise.*

Intuitively, gdubR,λpr, tq " α means that no instance of r can get closer than α to t in R. From the definition it follows that if r ÀR,λ t, then 0 < λ gdubR,λpr, tq ≤ 1 and if r ÀR,λ t, then gdubR,λpr, tq " 0.

The upper bound computed by gdub is more relaxed than it would be if the linearization function were not used, but this is what we will be able to compute in our algorithms later.

*Example 3.* Let Rpa, bq " 0.6, Rpb, cq " 0.7, and λ " 0.5. Then gdubR,λpfpx, bq, fpa, cqq " 0.7 and gdubR,λpfpx, xq, fpa, cqq " gdubR,λpfpx, yq, fpa, cqq " 1.

It is not difficult to see that if rσ »R,λ t, then Rprσ, tq ď gdubR,λpr, tq. In Example 3, for σ " {x -→ b} we have Rpfpx, xqσ, fpa, cqq " Rpfpb, bq, fpa, cqq " 0.6 < gdubR,λpfpx, xq, fpa, cqq " 1.

We compute gdubR,λpr, tq as follows: If r is a variable, then gdubR,λpr, tq " 1. Otherwise, if headprq "ρ R,β headptq, then gdubR,λpr, tq " β ^ - pi,jqPρ gdubR,λpr|i, t|j q. Otherwise, gdubR,λpr, tq " 0.

# 3 Term Set Consistency

The notion of term set consistency plays an important role in the computation of proximal generalizations. Intuitively, a set of terms is pR, λq-consistent if all the terms in the set have a common pR, λq-proximal term. In this section, we discuss this notion and the corresponding algorithms.

Definition 5 (Consistent set of terms). *A finite set of terms* T *is* pR, λqconsistent *if there exists a term* s *such that* s »R,λ t *for all* t P T*.*

pR, λq-consistency of a finite term set T is equivalent to tPT **pc**R,λptq‰H, but we cannot use this property to decide consistency, since proximity classes of terms can be infinite (when the argument relations are not restricted). For this reason, we introduce the operation [ on terms as follows: (i) t [ \_ " \_ [ t " t, (ii) fpt1,...,tnq [ fps1,...,snq " fpt1 [ s1,...,tn [ snq, n ě 0. Obviously, [ is associative (A), commutative (C), idempotent (I), and has \_ as its unit element (U). It can be extended to sets of terms: T1 [ T2 :" {t1 [ t2 | t1 P T1, t2 P T2}. It is easy to see that [ on sets also satisfies the ACIU properties with the set {\_} playing the role of the unit element.

Lemma 2. *A finite set of terms* T *is* pR, λq*-consistent iff* Ű tPT **rpc**R,λptq‰H*. Proof.* p⇒q If s »R,λ t for all t P T, then st P **rpc**R,λptq, where st is obtained from s by replacing all subterms that are irrelevant for its pR, λq-proximity to t by \_. Assume T " {t1,...,tn}. Then st1 [ ··· [ st*n* P Ű tPT **rpc**R,λptq.

p⇐q Obvious, since s »R,λ t for s P Ű tPT **rpc**R,λptq and for all t P T. -

Now we design an algorithm C that computes Ű tPT **rpc**R,λptq without actually computing **rpc**R,λptq for each t P T. A special version of the algorithm can be used to decide the pR, λq-consistency of T.

The algorithm is rule-based. The rules work on states, that are pairs **I**; s, where s is a term and **I** is a finite set of expressions of the form x in T, where T is a finite set of terms. R and λ are given. There are two rules (Z stands for disjoint union):

Rem: Removing the empty set

{x in H} Z **I**; s "⇒ **I**; s{x -→ \_}.

#### Red: Reduce a set to new sets

{x in {t1,...,tm}} Z **I**; s "⇒ {y1 in T1,...,yn in Tn} Y **I**; s{x -→ hpy1,...,ynq}, where m ě 1, h is an n-ary function symbol such that h "ρ*k* R,γ*k* headptkq with γk ě λ for all 1 ď k ď m, and Ti :" {tk|j | pi, jq P ρk, 1 ď k ď m}, 1 ď i ď n, is the set of all those arguments of the terms t1,...,tm that are supposed to be pR, λq-proximal to the i's argument of h.

To compute Ű tPT **rpc**R,λptq, C starts with {x in T}; x and applies the rules as long as possible. Red causes branching. A state of the form H; s is called a success state. A failure state has the form **I**; s, to which no rule applies and **I** ‰ H. In the full derivation tree, each leaf is a either success or a failure state.

*Example 4.* Assume a, b, c are constants, g, f, h are function symbols with the arities respectively 1, 2, and 3. Let λ be given and R be defined so that Rpa, bq ě λ, Rpb, cq ě λ, h "{p1,1q,p1,2q} R,β f, h "{p2,1q} R,γ g with β ě λ and γ ě λ. Then

$$\begin{aligned} \mathbf{r} \mathbf{p} \mathbf{c}\_{\mathcal{R},\lambda}(f(a,c)) &= \{ f(a,c), \, f(b,c), \, f(a,b), \, f(b,b), \, h(b,\\_,\\_) \}, \\ \mathbf{r} \mathbf{p} \mathbf{c}\_{\mathcal{R},\lambda}(g(a)) &= \{ g(a), g(b), h(\\_,a,\\_), h(\\_,b,\\_) \}, \end{aligned}$$

and **rpc**R,λpfpa, cqq[**rpc**R,λpgpaqq " {hpb, a,\_q, hpb, b,\_q}. We show how to compute this set with C: {x in {fpa, cq, gpaq}}; x "⇒Red {y1 in {a, c}, y2 : {a}, y3 in H}; hpy1, y2, y3q "⇒Rem {y1 in {a, c}, y2 : {a}}; hpy1, y2, \_q "⇒Red {y2 in {a}}; hpb, y2, \_q. Here we have two ways to apply Red to the last state, leading to two elements of **rpc**R,λpfpa, cqq [ **rpc**R,λpgpaqq: hpb, a, \_q and hpb, b, \_q.

Theorem 2. *Given a finite set of terms* T*, the algorithm* C *always terminates starting from the state* {x in T}; x *(where* x *is a fresh variable). If* S *is the set of success states produced at the end, we have* {s | H; s P S} " Ű tPT **rpc**R,λptq*.*

*Proof.* Termination: Associate to each state {x1 in T1,...xn in Tn}; s the multiset {d1,...,dn}, where di is the maximum depth of terms occurring in Ti. di " 0 if Ti " H. Compare these multisets by the Dershowitz-Manna ordering [5]. Each rule strictly reduces them, which implies termination.

By the definitions of **rpc**R,λ and [, hps1,...,snq P Ű tP{t1,...,t*m*} **rpc**R,λptq iff h "ρ*k* R,γ*k* headptkq with γk ě λ for all 1 ď k ď m and si P Ű tPT*i* **rpc**R,λptq, where Ti " {tk|j | pi, jq P ρk, 1 ď k ď m}, 1 ď i ď n. Therefore, in the Rem rule, the instance of x (which is hpy1,...,ynq) is in Ű tP{t1,...,t*m*} **rpc**R,λptq iff for each 1 ď i ď n we can find an instance of yi in Ű tPT*i* **rpc**R,λptq. If Ti is empty, it means that the i's argument of h is irrelevant for terms in {t1,...,tm} and can be replaced by \_. (Rem does it in a subsequent step.) Hence, in each success branch of the derivation tree, the algorithm C computes one element of Ű tPT **rpc**R,λptq. Branching at Red helps produce all elements of Ű tPT **rpc**R,λptq. -

It is easy to see how to use C to decide the pR, λq-consistency of T: it is enough to find one successful branch in the C-derivation tree for {x in T}; x. If there is no such branch, then T is not pR, λq-consistent. In fact, during the derivation we can even ignore the second component of the states.

# 4 Solving Generalization Problems

Now we can reformulate the anti-unification problem that will be solved in the remaining part of the paper. R is a proximity relation and λ is a cut value.

Given: R, λ, and the ground terms t1,...,tn, n ě 2.

Find: a set S of tuples pr, σ1,...,σn, α1,..., αnq such that

(When n " 1, this is a problem of computing a relevant proximity class of a term.) Below we give a set of rules, from which one can obtain algorithms to solve the anti-unification problem for four versions of argument relations:

Each of them has also the corresponding linear variant, computing minimal complete sets of (relevant) linear pR, λq-generalizations. They are denoted by adding the superscript lin to the corresponding algorithm name: Alin 1 and Alin 2 .

For simplicity, we formulate the algorithms for the case n " 2. They can be extended for arbitrary n straightforwardly.

The main data structure in these algorithms is an anti-unification triple (AUT) x : T1 fi T2, where T1 and T2 are finite *consistent* sets of ground terms. The idea is that x is a common generalization of all terms in T1 Y T2. A configuration is a tuple A; S; r; α1; α2, where A is a set of AUTs to be solved, S is a set of solved AUTs (the store), r is the generalization computed so far, and the α's are the current approximations of generalization degree upper bounds of r for the input terms.

Before formulating the rules, we discuss one peculiarity of approximate generalizations:

*Example 5.* For a given R and λ, assume Rpa, bq ě λ, Rpb, cq ě λ, h "{p1,1q,p1,2q} R,α f and h "{p1,1q} R,β g, where f is binary, g, h are unary, α ě λ and β ě λ. Then

This example shows that generalization algorithms should take into account not only the heads of the terms to be generalized, but also should look deeper, to make sure that the arguments grouped together by the given argument relation have a common neighbor. This justifies the requirement of consistency of a set of arguments, the notion introduced in the previous section and used in the decomposition rule below.

#### 4.1 Anti-unification for Unrestricted Argument Relations

Algorithms Alin 1 and A1 use the rules below to transform configurations into configurations. Given R, λ, and the ground terms t1 and t2, we create the initial configuration {x : {t1} fi {t2}}; H; x; 1; 1 and apply the rules as long as possible. Note that the rules preserve consistency of AUTs. The process generates a finite complete tree of derivations, whose terminal nodes have configurations with the first component empty. We will show how from these terminal configurations one collects the result as required in the anti-unification problem statement.

#### Tri: Trivial

{x : H fi H} Z A; S; r; α1; α2 "⇒ A; S; r{x -→ \_}; α1; α2.

#### Dec: Decomposition

{x : T1 fi T2} Z A; S; r; α1; α2 "⇒ {yi : Qi1 fi Qi2 | 1 ď i ď n} Y A; S; r{x -→ hpy1,...,ynq}; α1 ^ β1; α2 ^ β2,

where T1 Y T2 ‰ H; h is n-ary with n ě 0; y1,...,yn are fresh; and for j " 1, 2, if Tj " {t j 1,...,tj m*j* }, then

#### Sol: Solving

{x : T1 fi T2} Z A; S; r; α1; α2 "⇒ A; {x : T1 fi T2} Y S; r; α1; α2, if Tri and Dec rules are not applicable. (It means that at least one Ti ‰ H and either there is no h as it is required in the Dec rule, or at least one Qij from Dec is not pR, λq-consistent.)

Let expand be an *expansion operation* defined for sets of AUTs as

$$\mathtt{exprand}(S) \coloneqq \{ x : \bigcap\_{t \in T\_1} \mathtt{rep}\_{\mathcal{R}, \lambda}(t) \triangleq \bigcap\_{t \in T\_2} \mathtt{rep}\_{\mathcal{R}, \lambda}(t) \mid x : T\_1 \triangleq T\_2 \in S \}.$$

Exhaustive application of the three rules above leads to configurations of the form H; S; r; α1; α2, where r is a linear term. These configurations are further postprocessed, replacing S by expandpSq. We will use the letter E for expanded stores. Hence, terminal configurations obtained after the exhaustive rule application and expansion have the form H; E; r; α1; α2, where r is a linear term.1 This is what Algorithm Alin 1 stops with.

To an expanded store E " {y1 : Q11 fi Q12,...,yn : Qn1 fi Qn2} we associate two sets of substitutions ΣLpEq and ΣRpEq, defined as follows: σ P ΣLpEq (resp. σ P ΣRpEq) iff dompσq " {y1,...,yn} and yiσ P Qi1 (resp. yiσ P Qi2) for each 1 ď i ď n. We call them the sets of *witness substitutions*.

Configurations containing expanded stores are called *expanded configurations*. From each expanded configuration C " H; E; r; α1; α2, we construct the set SpCq :" {pr, σ1, σ2, α1, α2q | σ1 P ΣLpEq, σ2 P ΣRpEq}.

Given an anti-unification problem R, λ, t1 and t2, the *answer computed by Algorithm* Alin 1 is the set S :" Ym i"1SpCiq, where C1,...,Cm are all of the final expanded configurations reached by Alin 1 for R, λ, t1, and t2. 2

*Example 6.* Assume a, b, c and d are constants with b "H R,0.5 c, c "H R,0.6 d, and f, g and h are respectively binary, ternary and quaternary function symbols with h "{p1,1q,p3,2q,p4,2q} R,0.7 f and h "{p1,1q,p3,3q} R,0.8 g. For the proximity relation R given in this way and λ " 0.5, Algorithm Alin 1 performs the following steps to anti-unify fpa, bq and gpa, c, dq:

$$\begin{split} & \{ x : \{ f(a, b) \} \triangleq \{ g(a, c, d) \} \}; \mathcal{Q}; x; 1; 1 \Longrightarrow\_{\mathsf{Dec}} \\ & \{ x\_1 : \{ a \} \neq \{ a \}, \, x\_2 : \mathcal{Q} \neq \mathcal{Q}, \, x\_3 : \{ b \} \neq \{ d \}, \\ & \qquad \qquad x\_4 : \{ b \} \neq \mathcal{Q}; \{ \mathcal{Q}; h(x\_1, x\_2, x\_3, x\_4); 0.7; 0.8 \Longrightarrow\_{\mathsf{Dec}} \\ & \{ x\_2 : \mathcal{Q} \neq \mathcal{Q}, \, x\_3 : \{ b \} \neq \{ d \}, \, x\_4 : \{ b \} \neq \mathcal{Q} \}; \mathcal{Q}; h(a, x\_2, x\_3, x\_4); 0.7; 0.8 \Longrightarrow\_{\mathsf{Tri}} \\ & \{ x\_3 : \{ b \} \neq \{ d \}, \, x\_4 : \{ b \} \neq \mathcal{Q} \}; \mathcal{Q}; h(a, \\_, x\_3, x\_4); 0.7; 0.8 \Longrightarrow\_{\mathsf{Dec}} \\ & \{ x\_4 : \{ b \} \neq \mathcal{Q} \}; \mathcal{Q}; h(a, \\_, c, x\_4); 0.5; 0.6. \end{split}$$

Here Dec applies in two different ways, with the substitutions {x4 -→ b} and {x4 -→ c}, leading to two final configurations: H; H; hpa, \_, c, bq; 0.5; 0.6 and H; H; hpa, \_, c, cq; 0.5; 0.6. The witness substitutions are the identity substitutions. We have Rphpa, \_, c, bq, fpa, bqq " 0.5, Rphpa, \_, c, bq, gpa, c, dqq " 0.6, Rphpa, \_, c, cq, fpa, bqq " 0.5, and Rphpa, \_, c, cq, gpa, c, dqq " 0.6.

If we had h "{p1,1q,p1,2q,p4,2q} R,0.7 f, then the algorithm would perform only the Sol step, because in the attempt to apply Dec to the initial configuration, the set

1 Note that no side of the AUTs in E in those configurations is empty due to the

condition at the Decomposition rule requiring the Q*ij* 's to be pR, λq-consistent. 2 If we are interested only in linear generalizations *without witness substitutions*, there is no need in computing expanded configurations in Alin 1 .

Q11 " {a, b} is inconsistent: **rpc**R,λpaq " {a}, **rpc**R,λpbq " {b, c}, and, hence, **rpc**R,λpaq [ **rpc**R,λpbq"H.

Algorithm A1 is obtained by further transforming the expanded configurations produced by Alin 1 . This transformation is performed by applying the Merge rule below as long as possible. Intuitively, its purpose is to make the linear generalization obtained by Alin 1 less general by merging some variables.

Mer: Merge

H; {x1 : R11 fi R12, x2 : R21 fi R22} Z E; r; α1; α2 "⇒ H; {y : Q1 fi Q2} Y E; rσ; α1; α2,

where Qi " pR1i [ R2iq‰H, i " 1, 2, y is fresh, and σ " {x1 -→ y, x2 -→ y}.

The answer computed by A1 is defined similarly to the answer computed by Alin 1 .

*Example 7.* Assume a, b are constants, f1, f2, g1, and g2 are unary function symbols, p is a binary function symbol, and h1 and h2 are ternary function symbols. Let λ be a cut value and R be defined as fi "{p1,1q} R,α*i* hi and gi "{p1,2q} R,β*i* hi with αi ě λ, βi ě λ, i " 1, 2. To generalize ppf1paq, g1pbqq and ppf2paq, g2pbqq, we use A1. The derivation starts as

$$\begin{aligned} \{x:\{p(f\_1(a),g\_1(b))\} & \triangleq \{p(f\_2(a),g\_2(b))\}\}; \mathcal{\mathcal{Q}}; \; x; \; 1; \; 1 & \Longrightarrow\_{\mathsf{Dec}}\\ \{y\_1:\{f\_1(a)\} & \triangleq \{f\_2(a)\}, \; y\_2:\{g\_1(b)\} & \triangleq \{g\_2(b)\}\}; \; \mathcal{Q}; \; p(y\_1, y\_2); \; 1; \; 1 & \Longrightarrow\_{\mathsf{Sol}}^2\\ \mathcal{Q}; \; \{y\_1:\{f\_1(a)\} \neq \{f\_2(a)\}, \; y\_2:\{g\_1(b)\} \neq \{g\_2(b)\}\}; \; p(y\_1, y\_2); \; 1; \; 1. \end{aligned}$$

At this stage, we expand the store, obtaining

$$\begin{aligned} \mathcal{Q}; \{ y\_1: \{ f\_1(a), h\_1(a, \\_, \\_) \} \triangleq \{ f\_2(a), h\_2(a, \\_, \\_) \}, \\ y\_2: \{ g\_1(b), h\_1(\\_, b, \\_) \} \triangleq \{ g\_2(b), h\_2(\\_, b, \\_) \}; \, p(y\_1, y\_2); 1; \, 1. \end{aligned}$$

If we had the standard intersection X in the Mer rule, we would not be able to merge y1 and y2, because the obtained sets in the corresponding AUTs are disjoint. However, Mer uses [: we have {fipaq, hipa, \_, \_q} [ {gipbq, hip\_, b, \_q} " {hipa, b, \_q}, i " 1, 2 and, therefore, can make the step

$$\begin{aligned} \mathcal{Q}; \{ y\_1: \{ f\_1(a), h\_1(a, \\_, \\_) \} \models \{ f\_2(a), h\_2(a, \\_, \\_) \}, \\ y\_2: \{ g\_1(b), h\_1(\\_, b, \\_) \} \models \{ g\_2(b), h\_2(\\_, b, \\_) \}; \, p(y\_1, y\_2); \, 1; \, 1 \Longrightarrow\_{\mathsf{Mern}} \\ \mathcal{Q}; \, \{ z: \{ h\_1(a, b, \\_) \} \models \{ h\_2(a, b, \\_) \} \}; \, p(z, z); \, 1; \, 1. \end{aligned}$$

Indeed, if we take the witness substitutions σi " {z -→ hipa, b, \_q}, i " 1, 2, and apply them to the obtained generalization, we get

$$\begin{aligned} p(z,z)\sigma\_1 &= p(h\_1(a,b,\\_),h\_1(a,b,\\_)) \simeq\_{\mathcal{R},\lambda} p(f\_1(a),g\_1(b)),\\ p(z,z)\sigma\_2 &= p(h\_2(a,b,\\_),h\_2(a,b,\\_)) \simeq\_{\mathcal{R},\lambda} p(f\_2(a),g\_2(b)).\end{aligned}$$

Theorem 3. *Given* R*,* λ*, and the ground terms* t1 *and* t2*, Algorithm* A1 *terminates for* {x : {t1} fi {t2}}; H; x; 1; 1 *and computes an answer set* S *such that*

*Proof.  The rules Tri, Dec, and Sol strictly reduce the multiset of depths of AUTs in the first component of the configurations. Mer strictly reduces the number of distinct variables in generalizations. Hence, these rules cannot be applied infinitely often and A1 terminates.

In order to prove (1), we need to verify three properties:

*Soundness:* We show that each rule transforms an pR, λq-generalization into an pR, λq-generalization. Since we start from a most general pR, λq-generalization of t1 and t2 (a fresh variable x), at the end of the algorithm we will get an pR, λq-generalization of t1 and t2. We also show that in this process all irrelevant positions are abstracted by anonymous variables, to guarantee that each computed generalization is relevant.

Dec: The computed h is pR, λq-close to the head of each term in T1 Y T2. Qij 's correspond to argument relations between h and those heads, and each Qij is pR, λq-consistent, i.e., there exists a term that is pR, λq-close to each term in Qij . It implies that xσ " hpy1,...,ynq pR, λq-generalizes all the terms from T1 YT2. Note that at this stage, hpy1,...,ynq might not yet be a relevant pR, λqgeneralization of T1 and T2: if there exists an irrelevant position 1 ď i ď n for the pR, λq-generalization of T1 and T2, then in the new configuration we will have an AUT yi : H fi H.

Tri: When Dec generates y : H fi H, the Tri rule replaces y by \_ in the computed generalization, making it relevant.

Sol does not change generalizations.

Mer merges AUTs whose terms have *nonempty* intersection of **rpc**'s. Hence, we can reuse the same variable in the corresponding positions in generalizations, i.e., Mer transforms a generalization computed so far into a less general one.

*Completeness:* We prove a slightly more general statement. Given two finite consistent sets of ground terms T1 and T2, if r is a relevant pR, λq-generalization for all t1 P T1 and t2 P T2, then starting from {x : T1 fi T2}; H; x; 1; 1, Algorithm A1 computes a pr, σ1, σ2, α1, α2q such that r À r.

We may assume w.l.o.g. that r is a relevant pR, λq-lgg. Due to the transitivity of À, completeness for such an r will imply it for all terms more general than r .

We proceed by structural induction on r . If r is a (named or anonymous) variable, the statement holds. Assume r " hpr 1,...,r nq, T1 " {u1,...,um}, and T2 " {w1,...,wl}. Then h is such that h "ρ*i* R,β*i* headpuiq for all 1 ď i ď m and h "μ*j* R,γ*j* headpwj q for all 1 ď j ď l. Moreover, each r k is a relevant pR, λqgeneralization of Qk1 " Ym i"1{ui|q | pk, qq P ρi} and Qk2 " Yl j"1{wj |q | pk, qq P μj} and, hence, Qk1 and Qk2 are pR, λq-consistent. Therefore, we can perform a step by Dec, choosing hpy1,...,ykq as the generalization term and yi : Qi1 fi Qi2 as the new AUTs. By the induction hypothesis, for each 1 ď i ď n we can compute a relevant pR, λq-generalization ri for Qi1 and Qi2 such that r i À ri.

If r is linear, then the combination of the current Dec step with the derivations that lead to those ri's computes a tuple pr, . . .q P S, where r " hpr1,...,rnq and, hence, r À r.

If r is non-linear, assume without loss of generality that all occurrences of a shared variable z appear as the direct arguments of h: z " r k1 " ··· " r k*p* for 1 ď k1 < ··· < kp ď n. Since r is an lgg, Qk*i*1 and Qk*i*2 cannot be generalized by a non-variable term, thus, Tri and Dec are not applicable. Therefore, the AUTs yi : Qk*i*1 fi Qk*i*2 would be transformed by Sol. Since all pairs Qk*i*1 and Qk*i*2, 1 ď i ď p, are generalized by the same variable, we have [tPQ*j* **rpc**R,λptq‰H, where Qj " Yp i"1Qk*i*j , j " 1, 2. Additionally, r k1 ,...,r k*p* are all occurrences of z in r . Hence, the condition of Mer is satisfied and we can extend our derivation with p ´ 1-fold application of this rule, obtaining r " hpr1,...,rnq with z " rk1 " ··· " rk*p* , implying r À r.

*Minimality:* Alternative generalizations are obtained by branching in Dec or Mer. If the current generalization r is transformed by Dec into two generalizations r1 and r2 on two branches, then r1 " h1py1,...,ymq and r2 " h2pz1,...,znq for some h's, and fresh y's and z's. It may happen that r1 ÀR,λ r2 or vice versa (if h1 and h2 are pR, λq-close to each other), but neither r1 ≺R,λ r2 nor r2 ≺R,λ r1 holds. Hence, the set of generalizations computed before applying Mer is minimal. Mer groups AUTs together maximally, and different groupings are not comparable. Therefore, variables in generalizations are merged so that distinct generalizations are not ≺R,λ-comparable. Hence, (1) is proven.

As for (2), for i " 1, 2, from the construction in Dec follows Rprσi, tiq ď αi. Mer does not change αi, thus, αi " gdubR,λpr, tiq also holds, since the way how αi is computed corresponds exactly to the computation of gdubR,λpr, tiq: r ÀR,λ ti and only the decomposition changes the degree during the computation. -

The corollary below is proved similarly to Theorem 3:

Corollary 1. *Given* R*,* λ*, and the ground terms* t1 *and* t2*, Algorithm* Alin 1 *terminates for* {x : {t1} fi {t2}}; H; x; 1; 1 *and computes an answer set* S *such that*

### 4.2 Anti-unification with Correspondence Argument Relations

Correspondence relations make sure that for a pair of proximal symbols, no argument is irrelevant for proximity. Left- and right-totality of those relations guarantee that each argument of a term is close to at least one argument of its proximal term and the inverse relation remains a correspondence relation. Consequently, in the Dec rule of A1, the sets Qij never get empty. Therefore, the Tri rule becomes obsolete and no anonymous variable appears in generalizations. As a result, the pR, λq-mcsrg and the pR, λq-mcsg coincide, and the algorithm computes a solution from which we get an pR, λq-mcsg for the given anti-unification problem. The linear version Alin 1 works analogously.

#### 4.3 Anti-unification with Argument Mappings

When the argument relations are mappings, we are able to design a more constructive method for computing generalizations and their degree bounds (Recall that our mappings are partial injective functions, which guarantees that their inverses are also mappings.) We denote this algorithm by A2. The configurations stay the same as in before, but the AUTs in A will contain only empty or singleton sets of terms. In the store, we may still get (after the expansion) AUTs with term sets containing more than one element. Only the Dec rule differs from its previous counterpart, having a simpler condition:

#### Dec: Decomposition

{x : T1 fi T2} Z A; S; r; α1; α2 "⇒ {yi : Qi1 fi Qi2 | 1 ď i ď n} Y A; S; r{x -→ hpy1,...,ynq}; α1 ^ β1; α2 ^ β2,

where T1 Y T2 ‰ H; h is n-ary with n ě 0; y1,...,yn are fresh; for j " 1, 2 and for all 1 ď i ď n, if Tj " {tj} then h "π*j* R,β*j* headptj q and Qij " {tj |π*j* piq}, and if Tj " H then βj " 1 and Qij " H.

This Dec rule is equivalent to the special case of Dec for argument relations where mj ď 1. The new Qij 's contain at most one element (due to mappings) and, thus, are always pR, λq-consistent. Various choices of h in Dec and alternatives in grouping AUTs in Mer cause branching in the same way as in A1. It is easy to see that the counterparts of Theorem 3 hold for A2 and Alin 2 as well.

A special case of this fragment of anti-unification is anti-unification for similarity relations in fully fuzzy signatures from [1]. Similarity relations are mintransitive proximity relations. The position mappings in [1] can be modeled by our argument mappings, requiring them to be total for symbols of the smaller arity and to satisfy the similarity-specific consistency restrictions from [1].

#### 4.4 Anti-unification with Correspondence Argument Mappings

Correspondence argument mappings are bijections between arguments of function symbols of the same arity. For such mappings, if h »π R,λ f and h is n-ary, then f is also n-ary and π is a permutation of p1,...,nq. Hence, A2 combines in this case the properties of A1 for correspondence relations (Sect. 4.2) and of A2 for argument mappings (Sect. 4.3): all generalizations are relevant, computed answer gives an mcsg of the input terms, and the algorithm works with term sets of cardinality at most 1.

### 5 Remarks About the Complexity

The proximity relation R can be naturally represented as an undirected graph, where the vertices are function symbols and an edge between them indicates that they are proximal. Graphs induced by proximity relations are usually sparse. Therefore we can represent them by (sorted) adjacency lists. In the adjacency lists, we can also accommodate the argument relations and proximity degrees.

In the rest of this section we use the following notation:

We assume that the given anti-unification problem is represented as a completely shared directed acyclic graph (dag). Each node of the dag has a pointer to the adjacency list (with respect to R) of the symbol in the node.

Theorem 4. *Time complexities of* C *and the linear versions of the generalization algorithms are as follows:*

*Proof (Sketch).* In C, in the case of argument relations, an application of the Red rule to a state **I**; s replaces one element of **I** of size m by at most a new elements, each of them of size m ´ 1. Hence, one branch in the search tree for C, starting from a singleton set **I** of size n, will have the length at most l " n´1 i"0 ai . At each node on it there are at most Δ choices of applying Red with different h's, which gives the total size of the search tree to be at most l´1 i"0 Δi , i.e., the number of steps performed by C in the worst case is OpΔ•a*•n* q. Those different h's are obtained by intersecting the proximity classes of the heads of terms {t1,...,tm} in the Red rule. In our graph representation of the proximity relation, proximity classes of symbols are exactly the adjacency lists of those symbols which we assume are sorted. Their maximal length is Δ. Hence, the work to be done at each node of the search tree of C is to find the intersection of at most n sorted lists, each containing at most Δ elements. It needs Opn · Δq time. It gives the time complexity Opn · Δ · Δ•a*•n* q of C for the relation case.

In the mapping case, an application of the Red rule to a state **I**; s replaces one element of **I** of size m by at most a new elements of the *total* size m ´ 1. Therefore, the maximal length of a branch is n, the branching factor is Δ, and the amount of work at each node, like above, is Opn · Δq. Hence, the number of steps in the worst case is OpΔ•nq and the time complexity of C is Opn· Δ · Δ•nq.

The fact that consistency check is incorporated in the Dec rule in Alin 1 can be used to guide the application of this rule, using the values memoized by the previous applications of Red. The very first time, the appropriate h in Dec is chosen arbitrarily. In any subsequent application of this rule, h is chosen according to the result of the Red rule that has already been applied to the arguments of the current AUT for their consistency check, as required by the condition of Dec. In this way, the applications of Dec and Sol will correspond to the applications of Red. There is a natural correspondence between the applications of Rem and Tri rules. Therefore, Alin 1 will have the search tree analogous to that of C. Hence the complexity of Alin 1 is Opn·Δ·Δ•a*•n* q. Alin 2 does not call the consistency check, but does the same work as C and, hence, has the same complexity Opn · Δ · Δ•nq. -

### 6 Discussion and Conclusion

The diagram below illustrates the connections between different anti-unification problems based on argument relations:

The arrows indicate the direction from more general problems to more specific ones. For the unrestricted cases (left column) we compute mcsrg's. For correspondence relations and correspondence mappings (right column), mcsg's are computed. (In fact, for them, the notions of mcsrg and mcsg coincide). The algorithms for relations (upper row) are more involved than those for mappings (lower row): Those for relations deal with AUTs containing arbitrary sets of terms, while for mappings, those sets have cardinality at most one, thus simplifying the conditions in the rules. Moreover, the two cases in the lower row generalize the existing anti-unification problems:

All our algorithms can be easily turned into anti-unification algorithms for crisp tolerance relations3 by taking lambda-cuts and ignoring the computation of the approximation degrees. Besides, they are modular and can be used to compute only linear generalizations by just skipping the merging rule. We provided complexity estimations for the algorithms that compute linear generalizations (that often are of practical interest).

3 Tolerance: reflexive, symmetric, not necessarily transitive relation. According to Poincaré, a fundamental notion for mathematics applied to the physical world.

In this paper, we did not consider cases when the same pair of symbols is related to each other by more than one argument relation. Our results can be extended to them, that would open a way towards approximate anti-unification modulo background theories specified by shallow collapse-free axioms. Another interesting direction of future work would be extending our results to quantitative algebras [10] that also deal with quantitative extensions of equality.

Acknowledgments. Supported by the Austrian Science Fund, project P 35530.

## References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Guiding an Automated Theorem Prover with Neural Rewriting

Jelle Piepenbrock1,2(B) , Tom Heskes2 , Mikoláš Janota1 , and Josef Urban1

1 Czech Technical University in Prague, Prague, Czech Republic<EMAIL_ADDRESS>2 Radboud University, Nijmegen, The Netherlands

Abstract. Automated theorem provers (ATPs) are today used to attack open problems in several areas of mathematics. An ongoing project by Kinyon and Veroff uses Prover9 to search for the proof of the Abelian Inner Mapping (AIM) Conjecture, one of the top open conjectures in quasigroup theory. In this work, we improve Prover9 on a benchmark of AIM problems by neural synthesis of useful alternative formulations of the goal. In particular, we design the 3SIL (stratified shortest solution imitation learning) method. 3SIL trains a neural predictor through a reinforcement learning (RL) loop to propose correct rewrites of the conjecture that guide the search.

3SIL is first developed on a simpler, Robinson arithmetic rewriting task for which the reward structure is similar to theorem proving. There we show that 3SIL outperforms other RL methods. Next we train 3SIL on the AIM benchmark and show that the final trained network, deciding what actions to take within the equational rewriting environment, proves 70.2% of problems, outperforming Waldmeister (65.5%). When we combine the rewrites suggested by the network with Prover9, we prove 8.3% more theorems than Prover9 in the same time, bringing the performance of the combined system to 90%.

Keywords: Automated theorem proving · Machine learning

## 1 Introduction

Machine learning (ML) has recently proven its worth in a number of fields, ranging from computer vision [17], to speech recognition [15], to playing games [28,40] with *reinforcement learning* (RL) [45]. It is also increasingly applied in automated and interactive theorem proving. Learned predictors have been used for premise selection [1] in hammers [6], to improve clause selection in saturationbased theorem provers [9], to synthesize functions in higher-order logic [12], and to guide connection-tableau provers [21] and interactive theorem provers [2,5,14].

Future growth of the knowledge base of mathematics and the complexity of mathematical proofs will increase the need for proof checking and its better computer support and automation. Simultaneously, the growing complexity of software will increase the need for formal verification to prevent failure modes [10]. Automated theorem proving and mathematics will benefit from more advanced ML integration. One of the mathematical subfields that makes substantial use of automated theorem provers is the field of quasigroup and loop theory [32].

#### 1.1 Contributions

In this paper, we propose to use a neural network to suggest lemmas to the Prover9 [25] ATP system by rewriting parts of the conjecture (Sect. 2). We test our method on a dataset of theorems collected in the work on the Abelian Inner Mapping (AIM) Conjecture [24] in loop theory. For this, we use the AIMLEAP proof system [7] as a reinforcement learning environment. This setup is described in Sect. 3. For development we used a simpler Robinson arithmetic rewriting task (Sect. 4). With the insights derived from this and a comparison with other methods, we describe our own 3SIL method in Sect. 5. We use a neural network to process the state of the proving attempt, for which the architecture is described in Sect. 6. The results on the Robinson arithmetic task are described in Sect. 7.1. We show our results on the AIMLEAP proving task, both using our predictor as a stand-alone prover and by suggesting lemmas to Prover9 in Sect. 7.2. Our contributions are:

# 2 ATP and Suggestion of Lemmas by Neural Rewriting

Saturation-based ATPs make use of the *given clause* [30] algorithm, which we briefly explain as background. A problem is expressed as a conjunction of many initial clauses (i.e., the clausified axioms and the negated goal which is always an equation in the AIM dataset). The algorithm starts with all the initial clauses in the *unprocessed set*. We then pick a clause from this set to be the given clause and move it to the *processed set* and do all inferences with the clauses in the processed set. The newly inferred clauses are added to the unprocessed set. This concludes one iteration of the algorithm, after which we pick a new given

Fig. 1. Schematic representation of the proposed guidance method. In the first phase, we run a reinforcement learning loop to propose actions that rewrite a conjecture. This predictor is trained using the AIMLEAP proof environment. We collect the rewrites of the LHS and RHS of the conjecture. In the second phase, we add the rewrites to the ATP search input, to act as guidance. In this specific example, we only rewrote the conjecture for 1 step, but the added guidance lemmas are in reality the product of many steps in the RL loop.

clause and repeat [23]. Typically, this approach is designed to be *refutationally complete*, i.e., the algorithm is guaranteed to eventually find a contradiction if the original goal follows from the axioms.

This process can produce a lot of new clauses and the search space can become quite large. In this work, we modify the standard loop by adding useful lemmas to the initial clause set. These lemmas are proposed by a neural network that was trained *from zero knowledge* to rewrite the left- and right-hand sides of the initial goal to make them equal by using the axioms as the available rewrite actions. Even though the neural rewriting might not fully succeed, the rewrites produced by this process are likely to be useful as additional lemmas when added to the problem. This idea is schematically represented in Fig. 1.

## 3 AIM Conjecture and the AIMLEAP RL Environment

Automated theorem proving has been applied in the theory surrounding the Abelian Inner Mapping Conjecture, known as the AIM Conjecture. This is one of the top open conjectures in quasigroup theory. Work on the conjecture has been going on for more than a decade. Automated theorem provers use hundreds of thousands of inference steps when run on problems from this theory.

As a testbed for our machine learning and prover guidance methods we use a previously published dataset of problems generated by the AIM conjecture [7]. The dataset comes with a simple prover called AIMLEAP that can take machine learning advice.1 We use this system as an RL environment. AIMLEAP keeps the state and carries out the cursor movements (the cursor determines the location of the rewrite) and rewrites that a neural predictor chooses.

1 https://github.com/ai4reason/aimleap.

The AIM conjecture concerns specific structures in *loop theory* [24]. A loop is a quasigroup with an identity element. A quasigroup is a generalization of a group that does not preserve associativity. This manifests in the presence of two different 'division' operators, one left-division (\) and one right-division (/). We briefly explain the conjecture to show the nature of the data.

For loops, three *inner mapping functions* (left-translation L, right-translation R, and the mapping T) are:

$$\begin{aligned} L(u,x,y) &:= (y\*x) \backslash (y\*(x\*u)) & \quad &T(u,x) := x \backslash (u\*x) \\ R(u,x,y) &:= ((u\*x)\*y) \backslash (x\*y) \end{aligned}$$

These mappings can be seen as measures of the deviation from commutativity and associativity. The conjecture concerns the consequences of these three inner mapping functions forming an Abelian (commutative) group. There are two more notions, that of the *associator* function *a* and the *commutator* function *K*:

$$a(x,y,z) := (x\*(y\*z))\backslash((x\*y)\*z) \qquad\qquad K(x,y) := (y\*x)/(x\*y)$$

From these definitions, the conjecture can be stated. There are two parts to the conjecture. For both parts, the following equalities need to hold for all *u, v, x, y,* and *z* :

$$a(a(x,y,z),u,v) = 1 \qquad \qquad a(x,a(y,z,u),v) = 1 \qquad \qquad a(x,y,a(z,u,v)) = 1$$

where 1 is the identity element. These are necessary, but not sufficient for the two main parts of the conjecture. The first part of the conjecture asks whether a loop modulo its center is a group. In this context, the *center* is the set of all elements that commute with all other elements. This is the case if

$$K(a(x,y,z),u) = 1.$$

The second part of the conjecture asks whether a loop modulo its nucleus is an Abelian group. The *nucleus* is the set of elements that associate with all other elements. This is the case if

$$a(K(x,y),z,u) = 1 \qquad \qquad a(x,K(y,z),u) = 1 \qquad \qquad a(x,y,K(z,u)) = 1$$

#### 3.1 The AIMLEAP RL Environment

Currently, work in this area is done using automated theorem provers such as *Prover9* [24,25]. This has led to some promising results, but the search space is enormous. The main strategy for proving the AIM conjecture thus far has been to prove weaker versions of the conjecture (using additional assumptions) and then import crucial proof steps into the stronger version of the proof. The *Prover9* theorem prover is especially suited to this approach because of its wellestablished *hints* mechanism [48]. The AIMLEAP dataset is derived from this *Prover9* approach and contains around 3468 theorems that can be proven with the supplied definitions and lemmas [7].

There are 177 possible actions in the AIMLEAP environment [7]. We handle the proof state as a tree, with the root node being an equality node. Three actions are cursor movements, where the cursor can be moved to an argument of the current position. The other actions all rewrite the current term at the cursor position with various axioms, definitions and lemmas that hold in the AIM context. As an example, this is one of the theorems in the dataset (\ and = are part of the language):

$$T(T(T(x,T(x,y)\backslash 1),T(x,y)\backslash 1),y) = T((T(x,y)\backslash 1)\backslash 1,T(x,y)\backslash 1)\dots$$

The task of the machine learning predictor is to process the proof state and recognize which actions are most likely to lead to a proof, meaning that the two sides of the starting equation are equal according to the AIMLEAP system. The only feedback that the environment gives is whether a proof has been found or not: there is no intermediate reward (i.e. rewards are *sparse*). The ramifications of this are further discussed in Sect. 5.1.

#### 4 Rewriting in Robinson Arithmetic as an RL Task

To develop a machine learning method that can help solve equational theorem proving problems, we considered a simpler arithmetic task, which also has a treestructured input and *a sparse reward structure*: the normalization of Robinson arithmetic expressions. The task is to normalize a mathematical expression to one specific form. This task has been implemented as a Python RL environment, which we make available.2 The learning environment incorporates an existing dataset, constructed by Gauthier for RL experiments in the interactive theorem prover HOL4 [11]. Our RL setup for the task is also modeled after [11].

In more detail, the formalism that we use as an RL environment is Robinson arithmetic (RA). RA is a simple arithmetic theory. Its language contains the successor function *S*, addition *+* and multiplication *\** and one constant, the 0. The theory considers only non-negative numbers and we only use four axioms of RA. Numbers are represented by the constant 0 with the appropriate number of successor functions applied to it. The task for the agent is to rewrite an expression until there are only nodes of the successor or 0 types. Effectively, we are asking the agent to calculate the value of the expression. As an example, S(S(0)) + S(0), representing 2+1, needs to be rewritten to S(S(S(0))).

The expressions are represented as a tree data structure. Within the environment, there are seven different rewrite actions available to the agent. The four axioms (equations) defining these actions are x +0= x, x + S(y) = S(x + y), x ∗ 0=0 and x ∗ S(y)=(x ∗ y) + x, where the agent can apply the equations in either direction. There is one exception: the multiplication by 0 cannot be applied from right to left, as this would require the agent to introduce a fresh

2 https://github.com/learningeqtp/rewriteRL.

term which is out of scope for the current work. The place where the rewrite is applied is denoted by the location of the *cursor* in the expression tree.

In addition to the seven rewrite actions, the agent can move the cursor to one of the children of the current cursor node. This gives a total number of nine actions. Moving to a child of a node with only one child counts as moving to the left child. After a rewriting action, the cursor is reset to the root of the expression. More details on the actions are in the RewriteRL repository.

## 5 Reinforcement Learning Methods

This section describes the reinforcement learning methods, while Sect. 6 then further explains the particular neural architectures that are trained in the RL loops. We first briefly explain here the approaches that we used as reinforcement learning (RL) baselines, then we go into detail about the proposed 3SIL method.

#### 5.1 Reinforcement Learning Baselines

General RL Setup. For comparison, we used implementations of four established reinforcement learning baseline methods. In reinforcement learning, we consider an *agent* that is acting within an *environment*. The agent can take actions a from the action-space A to change the state s ∈ S of the environment. The agent can be rewarded for certain actions taken in a certain states, with reward given by the *reward function* R : (S×A) → R. The behavior of the environment is given by the *state transition function* P : (S×A) → S. The history of the agent's actions and the environments states and rewards at each timestep t are collected in tuples (st, at, rt). For a given history of a certain agent within an environment, we call the list of tuples (st, at, rt) describing this history an *episode*. The *policy function* π : S→A allows the agent to decide which action to take. The agent's goal is to maximize the return R: the sum of discounted rewards - t≥0 γt rt, where γ is a *discount factor* that allows control over how heavily rewards further in the future should be weighted. We will use Rt when we mean R, but calculated only from rewards from timestep t on. In the end, we are thus looking for a policy function π that maximizes the sum R of (discounted) expected rewards [45].

In our setting, every proof attempt (in the AIM setting) or normalization attempt (in the Robinson arithmetic setting) corresponds to an episode. The reward structure of theorem proving is such that there is only a reward of 1 at the end of a successful episode (i.e. a proof was found in AIM). Unsuccessful episodes get a reward of 0 at every timestep t.

A2C. The first method, *Advantage Actor-Critic*, or *A2C* [27] contains ideas on which the other three RL baseline methods build, so we will go into more detail for this method, while keeping the explanation for the other methods brief. For details we refer to the corresponding papers.

A2C attempts to find suitable parameters for an agent by minimizing a *loss function* consisting of two parts:

$$\mathcal{L} = \mathcal{L}\_{\text{policy}}^{\text{A2C}} + \mathcal{L}\_{\text{value}}^{\text{A2C}} \cdot \mathcal{L}$$

In addition to the policy function π, the agent has access to a *value function* V : S → R, that predicts the sum of future rewards obtained when given a state. In practice, both the policy and the value function are computed by a neural network *predictor*. The parameters of the predictor are set by *stochastic gradient descent* to minimize L. The set of parameters of the predictor that defines the policy function π is named θ, while the parameters that define the value function are named μ. The first part of the loss is the *policy loss*, which for one time step has the form

$$\mathcal{L}\_{\text{policy}}^{\text{A2C}} = -\log \pi\_{\theta}(a\_t|s\_t) A(s\_t, a\_t) \,,$$

where A(s, a) is the *advantage function*. The advantage function can be formulated in multiple ways, but the simplest is as Rt − Vμ(st). That is to say: the advantage of an action in a certain state is the difference between the discounted rewards Rt after taking that action and the value estimate of the current state.

Minimizing LA2C policy amounts to maximizing the log probability of predicting actions that are judged by the advantage function to lead to high reward.

The value estimates Vμ(s) for computing the advantage function are supplied by the *value predictor* Vμ with parameters μ, which is trained using the loss:

$$
\mathcal{L}\_{\text{value}}^{\text{A2C}} = \frac{1}{2} \left( R\_t - \mathcal{V}\_{\mu}(s\_t) \right)^2,
$$

which minimizes the advantage function. The logic of this is that the value estimate at timestep t, Vμ(st), will learn to incorporate the later rewards Rt, ensuring that when later seeing the same state, the possible future reward will be considered. Note that the sets of parameters θ and μ are not necessarily disjoint (see Sect. 6).

Note how the above equations are affected if there is no non-zero reward rt obtained at any timestep. In that case, the value function Vμ(st) will estimate (correctly) that any state will get 0 reward, which means that the advantage function A(s, a) will also be 0 everywhere. This means that LA2C policy will be 0 in most cases, which will lead to no or little change in the parameters of the predictor: learning will be very slow. This is the difficult aspect of the structure of theorem proving: there is only reward at the end of a successful proof, and nowhere else. This implies a possible strategy is to imitate successful episodes, without a value function. In this case, we would only need to train a *policy function*, and no approximate *value function*. This an aspect we explore in the design of our own method 3SIL, which we will explain shortly.

Compared to two-player games, such as chess and go, for which many approaches have been tailored and successfully used [41], theorem-proving has the property that it is hard to collect useful examples to learn from, as only successful proofs are likely to contain useful knowledge. In chess or go, however, one player almost always wins and the other loses, which means that we can at least learn from the difference between the two strategies used by those players. As an example, we executed 2 million random proof attempts on the AIMLEAP environment, which led to 300 proofs to learn from, whereas in a two-player setting like chess, we would get 2 million games in which one player would likely win.

ACER. The second RL baseline method we tested in our experiments is ACER, *Actor-Critic with Experience Replay* [49]. This approach can make use of data from older episodes to train the current predictor. ACER applies corrections to the value estimates so that data from old episodes may be used to train the current policy. It also uses trust region policy optimization [35] to limit the size of the policy updates. This method is included as a baseline to check if using a larger replay buffer to update the parameters would be advantageous.

PPO. Our third RL baseline is the widely used *proximal policy optimization* (PPO) algorithm [36]. It restricts the size of the parameter update to avoid causing a large difference between the original predictor's behavior and the updated version's behavior. The method is related to the above trust region policy optimization method. In this way, PPO addresses the training instability of many reinforcement learning approaches. It has been used in various settings, for example complex video games [4]. With its versatility, the PPO algorithm is well-positioned. We use the PPO algorithm with clipped objective, as in [36].

SIL-PAAC. Our final RL baseline uses only the transitions with positive advantage to train on for a portion of the training procedure, to learn more from good episodes. This was proposed as *self-imitation learning* (SIL) [29]. To avoid confusion with the method that we are proposing, we extend the acronym to SIL-PAAC, for positive advantage actor-critic. This algorithm outperformed A2C on the sparse-reward task Montezuma's Revenge (a puzzle game). As theorem proving has a sparse reward structure, we included SIL-PAAC as a baseline. More information about the implementations for the baselines can be found in the Implementation Details section at the end of this work.

### 5.2 Stratified Shortest Solution Imitation Learning

We introduce stratified shortest solution imitation learning (3SIL) to tackle the equational theorem proving domain. It learns to explicitly imitate the actions taken during the shortest solutions found for each problem in the dataset. We do this by minimizing the cross-entropy −log p(a*solution*|st) between the predictor output and the actions taken in the shortest solution. This is in contrast to the baseline methods, where value functions are used to judge the utility of decisions.

In our procedure this is not the case. Instead, we build upon the assumption for data selection that shorter proofs are better in the context of theorem proving

Input: problem p, policy πθ, problem history H Generate episode by following noisy version of πθ on p If solution, add list of tuples (s, a) to H[p] Keep k shortest solutions in H[p]

#### Algorithm 2. 3SIL

Input: set of problems P, randomly initialized policy πθ, batch size B, number of batches NB, problem history H, number of warmup episodes m, number of episodes f, max epochs ME Output: trained policy πθ, problem history H for e = 0 to ME *−* 1 do if e = 0 then num = m else num = f for i = 0 to num *−* 1 do CollectEpisode(sample(P), πθ, H) (Algorithm 1) end for for i = 0 to NB *−* 1 do Sample B tuples (s, a) with uniform probability for each problem from H Update θ to lower *−* -B b=0 log πθ(ab*|*sb) by gradient descent end for end for

and expression normalization. In a sense, we value decisions from shorter proofs more and explicitly imitate those transitions. We keep a history H for each problem, where we store the current shortest solution (states seen and actions taken) found for that problem in the training dataset. We can also store multiple shortest solutions for each problem if there are multiple strategies for a proof (the number of solutions kept is governed by the parameter k).

During training, in the case k = 1, we sample state-action pairs from each problem's current shortest solution at an equal probability (if a solution was found). To be precise, we first randomly pick a theorem for which we have a solution, and then randomly sample one transition from the shortest encountered solution. This directly counters one of the phenomena that we had observed: the training examples for the baseline methods tend to be dominated by very long episodes (as they contribute more states and actions). This *stratified* sampling method ensures that problems with short proofs get represented equally in the training process.

The 3SIL algorithm is described in more detail in Algorithm 2. Sampling from a noisy version of policy πθ means that actions are sampled from the predictordefined distribution and in 5% of cases a random valid action is selected. This is also known as the -greedy policy (with at 0.05).

Related Methods. Our approach is similar to the imitation learning algorithm DAGGER (Dataset Aggregation), which was used for several games [34] and modified for branch-and-bound algorithms in [16]. The behavioral cloning (BC) technique used in robotics [47] also shares some elements. 3SIL significantly differs from DAGGER and BC because it does not use an outside expert to obtain useful data, because of the stratified sampling procedure, and because of the selection of the shortest solutions for each problem in the training dataset. We include as an additional baseline an implementation of behavioral cloning (BC), where we regard proofs already encountered as coming from an expert. We minimize cross-entropy between the actions in proofs we have found and the predictions to train the predictor. For BC, there is no stratified sampling or shortest solution selection, only the minimization of cross-entropy between actions taken from recent successful solutions and the predictor's output.

Extensions. For the AIM tasks, we introduce two other techniques, *biased sampling* and *episode pruning*. In biased sampling, problems without a solution in the history are sampled 5 times more during episode collection than solved problems to accelerate progress. This was determined by testing 1, 2, 5 and 10 as sampling proportions. For episode pruning, when the agent encountered the same state twice, we prune the episode to exclude the looping before storing the episode. This helps the predictor learn to avoid these loops.

# 6 Neural Architectures

The tree-structured states representing expressions occurring during the tasks will be processed by a neural network. The neural network takes the treestructured state and predicts an action to take that will bring the expression closer to being normalized or the theorem closer to being proven.

Fig. 2. Schematic representation of the creation of a representation of an expression (*an embedding*) using different neural network layers to represent different operations. The figure depicts the creation of a numerical representation for the Robinson arithmetic expression (S(0) + 0). Note that the successor layer and the addition layer consist of trainable parameters, for which the values are set through gradient descent.

There are two main components to the neural network we use: an *embedding* tree neural network that outputs a numerical vector representing the treestructured proof state and a second *processor* network that takes this vector representation of the state and outputs a distribution of the actions possible in the environment.3

Tree neural networks have been used in various settings, such as natural language processing [20] and also in Robinson arithmetic expression embedding [13]. These networks consist of smaller neural networks, each representing one of the possible functions that occur in the expressions. For example, there will be separate networks representing addition and multiplication. The cursor is a special unary operation node with its own network that we insert into the tree at the current location. For each unique constant, such as the constant 0 in RA or the identity element 1 for the AIM task, we generate a random vector (from a standard normal distribution) that will represent this leaf. In the case of the AIM task, these vectors are parameters that can be optimized during training.

At prediction time, the numerical representation of a tree is constructed by starting at the leaves of the tree, for which we can look up the generated vectors. These vectors act as input to the neural networks that represent the parent node's operation, yielding a new vector, which now represents the subtree of the parent node. The process repeats until there is a single vector for the entire tree after the root node is processed (see also Fig. 2).

The neural networks representing each operation consist of a linear transformation, a non-linearity in the form of a rectified linear unit (ReLU) and another linear transformation. In the case of binary operations, the first linear transformation will have an input dimension of *2n* and an output dimension of *n*, where *n* is the dimension of the vectors representing leaves of the tree (the *internal representation size*). The weights representing these transformations are randomly initialized at the beginning of training.

When we have obtained a single vector embedding representing the entire tree data structure, this vector serves as the input to the *predictor* neural network, which consists of three linear layers, with non-linearities (Sigmoid/ReLU) in between these layers. The last layer has an output dimension equal to the number of possible actions in the environment. We obtain a probability distribution over the actions, e.g. by applying the softmax function to the output of this last layer. In the cases where we also need a value prediction, there is a parallel last layer that predicts the state's value (usually referred to as a *two-headed* network [41]). The internal representation size n for the Robinson arithmetic experiments is set to 16, for the AIM task this is 32. The number of neurons in each layer (except for the last one) of the predictor networks is 64.

In the AIM dataset task, an arbitrary number of variables can be introduced during the proof. These are represented by untrainable random vectors. We add a special neural network (with the same architecture as the networks representing unary operations, so from size *n* to *n*) that processes these vectors before they are

3 In the reinforcement learning baselines that we use, this second *processor* network has the additional task of predicting the value of a state.

processed by the rest of the tree neural network embedding. The idea is that this neural network learns to project these new variable vectors into a subspace and that an arbitrary number of variables can be handled. The vectors are resampled at the start of each episode, so the agent cannot learn to recognize specific variables. This approach was partly inspired by the *prime* mechanism in [13], but we use separate vectors for all variables instead of building vectors sequentially. All our neural networks are implemented using the PyTorch library [31].

# 7 Experiments

We first describe our experiments on the Robinson arithmetic task, with which we designed the properties of our 3SIL approach with the help of comparisons with other algorithms. We then train a predictor using 3SIL on the AIMLEAP loop theory dataset, which we evaluate both as a standalone prover within the RL environment and as a neural guidance mechanism for the ATP Prover9.

### 7.1 Robinson Arithmetic Dataset

Dataset Details. The Robinson arithmetic dataset [11] is split into three distinct sets, based on the number of steps that it takes a fixed rewriting strategy to normalize the expression. This fixed strategy, LOPL, which stands for *left outermost proof length*, always rewrites the leftmost possible element. If it takes this strategy less than 90 steps to solve the problem, it is in the *low* difficulty category. Problems with a difficulty between 90 and 130 are in the *medium* category and a greater difficulty than 130 leads to the *high* category. The *high* dataset also contains problems the LOPL strategy could not solve within the time limit. The *low* dataset is split into a training and testing set. We train on the *low* difficulty problems, but after training we also test on problems with a higher difficulty. Because we have a difficulty measure for this dataset, we use a curriculum setup. We start by learning to normalize the expressions that a fixed strategy can normalize in a small amount of steps. This setup is similar to [11].

Training Setup. The 400 problems with the lowest difficulty are the starting point. Every time an agent reaches 95 percent success rate when evaluated on a sample of size 400 from these problems, we add 400 more difficult problems to set of training problems P. One iteration of the *collection* and *training* phase is called an *epoch*. Agents are evaluated after every epoch. The blocks of size 400 are called *levels*. The number of episodes m and f are set to 1000. For 3SIL and BC, the batch size BS is 32 and the number of batches NB is 250. The baselines are configured so that the number of episodes and training transitions is at least as many as the 3SIL/BC approaches. Episodes that take over 100 steps are stopped. ADAM [22] is used as an optimizer.

Fig. 3. The level in the curriculum reached by each method. Each method was run three times. The bold line shows the mean performance and the shaded region shows the minimum and maximum performance. K is the number of proofs stored per problem.

Results on RA Curriculum. In Fig. 3, we show the progression through the training curriculum for behavioral cloning (BC), the RL methods (PPO, ACER) and two configurations of 3SIL. Behavioral cloning simply imitates actions from successful episodes. Of the RL baselines, PPO reaches the second level in one run, while ACER steadily solves the first level and in the best run solves around 80% of the second level. Both methods do not learn enough solutions for the second level to advance to the third. A2C and SIL-PAAC do not reach the second level, so these are left out of the plot. However, they do learn to solve about 70–80% of the first 400 problems. From these results we can conclude that the RL baselines do not perform well on this task in our experiment. We attribute this to the difficulty of learning a good value function due to the sparse rewards (Sect. 5.1). Our hypothesis is that because this value estimate influences the policy updates, the RL methods do not learn well on this task. Note that the two methods with a trust region update mechanism, ACER and PPO, perform better than the methods without this mechanism. From these results, it is clear that 3SIL with 1 shortest proof stored, k = 1, is the best-performing configuration. It reaches the end of the training curriculum of about 5000 problems in 40 epochs. We experimented with k = 3 and k = 4, but these were both worse than k = 2.

Generalization. While our approach works well on the training set, we must check if the predictors generalize to unseen examples. Only the methods that reached the end of the curriculum are tested. In Table 1, we show the results of evaluating the performance of our predictors on the three different test sets: the unseen examples from the *low* dataset and the unseen examples from the *medium* and *high* datasets. Because we expect longer solutions, the episode limits are expanded from 100 steps to 200 and 250 for the *medium* and *high* datasets respectively. For the *low* and *medium* datasets, the second of which contains problems with more difficult solutions than the training data, the predictors solve almost all test problems. For the *high* difficulty dataset, the performance drops by at least 20% points. Our method outperforms the Monte Carlo Tree Search approach used in [11] on the same datasets, which got to 0.954 on the *low* dataset with 1600 iterations and 0.786 on the *medium* dataset (no results on the *high* dataset were reported). These results indicate that this training method might be strong enough to perform well on the AIM rewriting RL task.

Table 1. Generalization with greedy evaluation on the test set for the Robinson arithmetic normalization tasks, shown as average success rate and standard deviation from 3 training runs. Generalization is high on the low and medium difficulty (training data is similar to the low difficulty dataset). With high difficulty data, performance drops.

#### 7.2 AIM Conjecture Dataset

Training Setup. Finally, we train and evaluate 3SIL on the AIM Conjecture dataset. We apply 3SIL (k = 1) to train predictors in the AIMLEAP environment. Ten percent of the AIM dataset is used as a hold-out test set, not seen during training. As there is no estimate for the difficulty of the problems in terms of the actions available to the predictor, we do not use a curriculum ordering for these experiments. The number m of episodes collected before training is set to 2,000,000. These random proof attempts result in about 300 proofs. The predictor learns from these proofs and afterwards the search for new proofs is also guided by its predictions. For the AIM experiments, episodes are stopped after 30 steps in the AIMLEAP environment. The predictors are trained for 100 epochs. The number of collected episodes per epoch f is 10,000. The successful proofs are stored, and the shortest proof for each theorem is kept. NB is 500 and BS is set to 32. The number of problems with a solution in the history after each epoch of the training run is shown in Fig. 4.

Results as a Standalone Prover. After 100 epochs, about 2500 of 3114 problems in the training dataset have a solution in their history. To test the generalization capability of the predictors, we inspect their performance on the holdout test set problems. In Table 2 we compare the success rate of the trained predictors on the holdout test set with three different automated theorem provers: E [37,38], Waldmeister [19] and Prover9. E is currently one of the best overall automated theorem provers [44], Waldmeister is a prover specialized in memoryefficient equational theorem proving [18] and Prover9 is the theorem prover that

Fig. 4. The number of training problems for which a solution was encountered and stored (cumulative). At the start of the training, the models rapidly collect more solutions, but after 100 epochs, the process slows down and settles at about 2500 problems with known solutions. The minimum, maximum and mean of three runs are shown.

is used for AIM conjecture research and the prover that the dataset was generated by. Waldmeister and E are the best performing solvers in competitions for the relevant unit equality (UEQ) category [44].

Table 2. Theorem proving performance on the hold-out test set in fraction of problems solved. Means and standard deviations are the results of evaluations of 3 different predictors from 3 different training runs on the 354 unseen test set problems.

The results show that a single greedy evaluation of the predictor trying to solve the problem in the AIMLEAP environment is not as strong as the theorem proving software. However, the theorem provers got 60 s of execution time, and the execution of the predictor, including interaction with AIMLEAP, takes on average less than 1 s. We allowed the predictor setup to use 60 s, by running attempts in AIMLEAP until the time was up, sampling actions from the predictor's distribution with 5% noise, instead of using greedy execution. With this approach, the predictor setup outperforms Waldmeister.4 Figure 5 shows the overlap between the problems solved by each prover. The diagram shows that each theorem prover found a few solutions that no other prover could find within

4 After the initial experiments, we also evaluated Twee [42], which won the most recent UEQ track: it can prove most of the test problems in 60 s, only failing for 1 problem.

the time limit. Almost half of all problems from the test set that are solved are solved by all four systems.

Fig. 5. Venn diagram of the test set problems solved by each solver with 60 s time limit.

Results of Neural Rewriting Combined with Prover9. We also combine the predictor with *Prover9*. In this setup, the predictor modifies the starting form of the goal, for a maximum of 1 s in the AIMLEAP environment. This produces new expressions on one or both sides of the equality. We then add, as lemmas, equalities between the left-hand side of the goal before the predictor's rewriting and after each rewriting (see Fig. 1). The same is done for the righthand side. For each problem, this procedure yields new lemmas that are added to the problem specification file that is given to *Prover9*.

Table 3. Prover9 theorem proving performance on the hold-out test set when injecting lemmas suggested by the learned predictor. *Prover9* 's performance increases when using the suggested lemmas.

In Table 3, it is shown that adding lemmas suggested by the rewriting actions of the trained predictor improves the performance of *Prover9*. Running *Prover9* for 2 s results in better performance than running it for 1 s, as expected. The combined (1 s + 1 s) system improved on *Prover9's* 2-s performance by 12.7% (= 0.841/0.746), indicating that the predictor suggests useful lemmas. Additionally, 1 s of neural rewriting combined with 59 s of Prover9 search proves almost 8.3% (= 0.902/0.833) more theorems than Prover9 with a 60 s time limit (Table 2).

#### 7.3 Implementation Details