“Large theory” problems in Automated Theorem Proving (ATP) have been defined as having many functions and predicates, and many axioms of which only a few are required for the proof of a theorem. One key to solving large theory problems is selecting a subset of the axioms that is adequate for finding a proof. The main contribution of this paper is metrics for evaluating axiom selection techniques without having to run an ATP system on the problem formed from the selected axioms and the problem's conjecture. This paper additionally presents three new axiom selection techniques. The new techniques, and the axiom selection in the Vampire ATP system, are evaluated using the metrics.
1. Introduction In the third step of this process, a proof indicates an adequate selection (the quality of which can then be evaluated), and a countermodel indicates an inadequate selection. As the development of axiom selection techniques progresses, this approach requires repeating steps 2 and 3 to evaluate progress. Evaluation needs to be done on large corpora, making this a time consuming process. As a consequence, to move things along faster, it is often necessary to impose a small time limit on each ATP system run. Time limits (and other practical forms of incompleteness) cause timeouts, and a timeout in the third step provides no information - the selection might be inadequate, or the selection might be adequate but the reduced problem is too hard because too many (unnecessary) axioms were selected, or the time limit is too small. The results are also influenced by the choice of ATP system. Overall, this process for evaluating axiom selection techniques is problematic.
The main contribution of this paper is metrics for evaluating axiom selection techniques
without having to run an ATP system on the reduced problems. While the “proof is in the
pudding” and it is eventually necessary to evaluate by running an ATP system, the metrics
described in this paper provide a first-pass evaluation that allows axiom selection techniques
to be rapidly tested and refined. The approach has the advantage of being independent of a
chosen ATP system. This paper additionally presents three new axiom selection techniques.
The new techniques and the axiom selection [
This paper is structured as follows: Section 2 describes the evaluation metrics. Section 3 describes a relatedness measure between formulae, and the three new axiom selection techniques that are based on that measure. Section 4 provides evaluation results, including an initial evaluation of the metrics themselves. Section 5 concludes.
The axiom selection evaluation metrics measure how precisely a set of selected axioms matches
a known minimally adequate set of axioms. Two types of axiom selection techniques are
considered:
• Ranking techniques, which take the problem’s axioms as input, rank them according to
how likely they are judged to be necessary for a proof, and select the axioms that are ranked
above some cut-of criterion. This technique is used in, e.g., Isabelle’s Sledgehammer [
In this work the MPTP2078 corpus1, based on the Mizar Mathematical Library [
In order to extract minimally adequate sets of axioms for each problem, Vampire and E [
The pruney problems provide minimally adequate sets of axioms against which selected sets of axioms can be compared. The smallest fraction of axioms in a minimally adequate set ranges from 0.01 to 1.0 for the bushy problems, and from 0.0002 to 0.36 for the chainy problems. The average fractions are 0.29 and 0.01, respectively. These fractions show that precise axiom selection could significantly reduce the number of axioms that need to be used, which in turn normally significantly reduces the search space of an ATP system. As might be expected, the numbers are more extreme for the larger chainy problems.
Define the following basic measures: • The N umber of Axioms in a Problem: NAxP. • The N umber of axioms Selected: NSel. • The N umber of axioms U sed in a Proof, i.e., the cardinality of a minimally adequate set:
NUiP. NUiP is 0 if no axioms need to be used, i.e., the conjecture is a theorem. • In a ranked list of axioms, the number of axioms down to the lowest ranked axiom in a minimally adequate set, i.e., the N umber of axioms N eeded from the Ranking: NNRa.
The axiom selection evaluation metrics are listed below. In all cases the range is [0.0, 1.0]. Precision. If the axiom selection technique selects an adequate set of axioms, i.e., a superset of one or more of the known minimally adequate sets of axioms, then: • If the minimum NUiP = 0, and NSel= 0, then 1.00 • Else the maximum NUiP/NSel If the selection technique selects an inadequate set then the precision is 0.00. Larger values are better. The intuition here is of a probability that using the selection will result in a proof (which is 0.00 if an inadequate set is selected). Selectivity. NSel/NAxP. This measures the fraction of axioms selected. 1.00 results from selecting all the axioms - the base case. Smaller values are better, provided an adequate set of axioms is selected.
Ranking precision. (Applicable to only ranking techniques.) If the axiom selection technique selects an adequate set of axioms, then: • If the minimum NUiP = 0, and NSel= 0, then 1.00 • Else the maximum NNRa/NSel If the technique selects an inadequate set, then 0.00. This measures how precisely the technique chooses the “best ones” from the ranked list of axioms. Larger values are better. Ranking density. (Applicable to only ranking techniques.) If NUiP = NNRa = 0, then 1.00, else NUiP/NNRa. This measures the quality of the ranking - axioms in a minimally adequate set should be ranked highly, which in turn allows a smaller number to be selected if the ranking precision is good. Larger values are better.
Average precision/selectivity/ranking precision/ranking density. For a set of problems, the average over the problems.
Adequacy. For a set of problems, the fraction of problems for which the axiom selection technique selects an adequate set of axioms. Larger values are better.
Adequate precision/selectivity/ranking precision/ranking density. For a set of problems, the average over the problems for which the axiom selection technique selects an adequate set of axioms.
The motivation for developing these metrics was based on a need to evaluate new axiom selection techniques being developed by the first three authors. These techniques are described in this section, and their performance according to the metrics is evaluated in Section 4. It turns out that a very simple technique performs surprisingly well on the MPTP2078 corpus.
All of the new techniques are based on how strongly two formulae are related (as is the case in many axiom selection techniques). In this work a novel measure of relatedness is used, which is described in Section 3.1. The individual new techniques are then described in Sections 3.2 to 3.4.
The relatedness between two formulae is computed first as a dissimilarity between the two formulae, which is also later converted to a similarity.
The dissimilarity between two terms or atoms is an extended version of the Hutchinson
distance [
Divide into two parts, and : = {,1 ↦→ ,1, . . . , , ↦→ , } = {,1 ↦→ ,1, . . . , , ↦→ , } where , and , are the substituted variables, , are substituting variables, and , are substituting functional terms. Let • be a weight for variables (currently set to 13), • be a weight function for non-variable symbols (currently set to 2 for all symbols), • (, ∆) be the set of occurrences of the variable in ∆ , • (, ∆) be the depth of a particular occurrence of the variable in ∆ , e.g., (, (, ()) = 1 for the first occurrence and 2 for the second occurrence, • (, ∆) be × (| (, ∆) | + ∑︀∈ (,Δ) (, ∆)) , i.e., the weighted sum of the number of occurrences of in ∆ and the depths of the occurrences of in ∆ , e.g., (, (, ()) = × (2 + (1 + 2)) = 5, • (∆) be the sum of the weights (using ) of the non-variable symbols occurring in ∆ , • () be a continuous increasing function R ↦→ R such that (0) = 0 and (1 + 2) ≤ (1) + (2) for 1, 2 ≥ 0 (currently set to ( + 1)).
Then, and are functions that map and to real numbers:
( ) = ∑︁ ((, , ∆ ) − (, , ∆)) =1 ( ) = ∑︁(| (, , ∆) | × (, ))
=1 ( ) measures the diference between the usage of substituting variables in ∆ and the usage of substituted variables in ∆ , over the substitutions made in ∆ by . ( ) measures the total function symbol weight of the substituting terms, over the substitutions made in ∆ by . The dissimilarity between two terms or atoms ∆ 1 and ∆ 2 is then: (∆ 1, ∆ 2) = √︁
[( 1) + ( 2)]2 + [ ( 1 ) + ( 2 )]2 The dissimilarity measures the combined substitution “efort” required to convert the least general generalization to those terms or atoms.
3The values of 1 and 2 for and were adopted from their use in E, place greater emphasis on non-variable substitutions, and are small enough to avoid large dissimilarity values. The use of ( + 1) for () below was motivated by it’s common adoption as a continuous increasing function, to usefully dampen the impact of variable substututions on dissimilarity values. (4) (5) (6)
Let Φ 1 and Φ 2 be two formulae, containing the atoms {∆ 1,1, . . . , ∆ 1,} and {∆ 2,1, . . . , ∆ 2,} respectively. Let ̸=∞ be the set of pairs (∆ 1,, ∆ 2, ) for which (∆ 1,, ∆ 2, ) ̸= ∞. If ̸=∞ = ∅, i.e., all pairs of atoms in Φ 1 and Φ 2 are infinitely dissimilar, then the dissimilarity (Φ 1, Φ 2) = ∞. Otherwise: (Φ 1, Φ 2) = ∑︀ (Δ1,,Δ2,)∉=∞ (∆ 1,, ∆ 2, ) |̸=∞| × × |̸=∞| The first term is the average dissimilarity between pairs of atoms that are not infinitely dissimilar. The second term penalizes the first by the excess of atom pairs whose dissimilarity is infinite. Intuitively, the dissimilarity between two formulae measures the extent to which inference between them might not be possible by virtue of the dissimilarity of their atoms.
For two formulae Φ 1 and Φ 2, their similarity (Φ 1, Φ 2) is defined in the context of a set of formulae ℱ , Φ 1, Φ 2 ∈ ℱ :
(ℱ ) = ,∈ℱ ((, ) ̸= ∞) (Φ 1, Φ 2, ℱ ) = max(0, (ℱ ) − (Φ 1, Φ 2)) If the dissimilarity is 0, then the similarity is the largest dissimilarity that is not ∞. If the dissimilarity is greater than 0 and not ∞, then the similarity is the diference between the largest dissimilarity that is not ∞ and the dissimilarity. If the dissimilarity is ∞ or is equal to the largest dissimilarity that is not ∞, then the similarity is 0. 3.2. Q∞ This axiom selection technique takes a problem consisting of a conjecture and axioms , and selects all axioms Φ ∈ such that (, Φ) ̸= ∞. This simply means that each axiom contains at least one atom whose predicate symbol matches that of an atom in the conjecture.
This axiom selection technique views the formulae of a problem as nodes of a complete
undirected graph, with the similarities between the formulae as the edge weights. Spectral clustering
[
The initial centroids for the clustering are extracted from a feature matrix consisting of the
eigenvectors of the normalized graph Laplacian matrix [
To determine the number of clusters for a problem in the MPTP2078 corpus, the three step process was applied to each problem with the number of clusters ranging from two to half the number of formulae in the problem. The precision was computed each time, and the best number of clusters recorded. A median regression line was fitted to this data (separately for the bushy and chainy problems), as shown in Figure 1. The upper two plots are for a problem set of 325 smaller problems (see Section 4 for details of the testing problem sets), and the lower plot is for the 1551 bushy problems. While the fit of the regression lines is awful, they were used to set the number of clusters for problems in the corpus, based on the number of formulae in each problem. For the 1551 bushy problems it turns out that two clusters is always optimal, regardless of the number of axioms. It was not possible to compute a regression line for the 1369 chainy problems with the time and computing resources available.
This axiom selection technique views the formulae of a problem as nodes of a complete undirected graph, with the similarities between the formulae as the edge weights. Figure 2 provides a simple illustrative example, in which C is the conjecture and As are the axioms (the figure omits edges that do not afect the example). Starting at the conjecture, a greedy tree is built by iteratively visiting all the axioms most similar to the current leaves of the tree, until axioms that have no similarity (or equivalently, infinite dissimilarity) to the conjecture are reached. These infinitely dissimilar nodes are ignored. In Figure 2 the thicker edges are those that are followed, and the axioms with thicker circles are those at which the tree growth stops because they have no similarity to the conjecture. At that stage the light grey axioms are in the tree. As a final step, all the unvisited axioms most similar to the axioms in the greedy tree are added to the tree. In Figure 2, that adds the dark grey axioms to the tree. The axioms in the tree are selected those are the non-white axiom in the Figure 2..
The new axiom selection techniques and the axiom selection in the Vampire ATP system were evaluated using the metrics. No particular efort was moade to optimize the implementation of the new selection techniques; rather, the evaluation aimed to demonstrate the usefulness of the metrics, and as such no CPU times are presented below. Two problem sets from each of the bushy and chainy parts of the MPTP2078 corpus were used. The first set was selected by taking the 325 chainy problems with less than 500 axioms and for which minimally adequate axiom sets of axioms (pruney problems) are known, and taking the corresponding 325 bushy problems. The second set was the 1551 bushy problems and 1369 chainy problems for which minimally adequate axiom sets (pruney problems) are known. The smaller set was useful for initial quick testing, and also necessary because some of the new techniques could not analyse the chainy problems set with the time and computing resources available.
Tables 1 and 2 show the results, including a row for the base case in which all axioms are selected. The columns are the Precision (Prcn), Selectivity (Sely), Ranking precision (RPrn), Ranking density (RDen), Adequacy (Adeq), and the Adequate precision/selectivity/ranking precision/ranking density.
For the smaller set of 325 bushy problems Q∞ performs the best, with the highest precision and lowest selectivity. It also has a 74% adequacy. Moving up to the 325 chainy problems Q∞ and Vampire have the highest precision, with Q∞ having slightly higher selectivity, and Vampire better adequacy. For the 1551 bushy problems Q∞ is again the top performer, now in terms of precision, selectivity, and adequacy. Spectral clustering also performs reasonably well, with a better precision than Vampire, and with the cluster containing the conjecture (recall from Section 3.3 that two clusters is optimal, and hence used here) containing 69% of the axioms on average. Finally, for the 1369 chainy problems Q∞ and Vampire again have the highest precision, with Vampire having the best selectivity and adequacy. Overall, Q∞ performs the best on the bushy problems, with Vampire doing slightly better on the chainy problems. It is surprising that the very simple Q∞ technique performs as well as it does, when compared to the mature (and more complex) Vampire selection technique.
The adequacy numbers have to be viewed carefully - it is easy to get an optimal adequacy simply by selecting all axioms and thus having pessimal selectivity. It is interesting to contrast the average and adequate precision values. The average precision for the base case is better than that of some of the selection techniques because of the zero precision assigned when an inadequate set of axioms is selected. An adequate precision close to the base case, as for, e.g., Spectral Clustering and Greedy Tree+NN on both sets of 325 problems, indicates that doing the axiom selection is probably wasted efort.
There is a correlation, but not a particularly strong correlation, between the number of axioms in a problem and the precision of the Vampire and Q∞ axiom selections, e.g., around 40% for the chainy problems. This suggests that the axiom selection techniques might scale well to larger problems.
Overall, the precision values are disappointingly low, especially for the chainy problems. For Q∞ the ranking density is similarly low, so that even with perfect ranking precision the raw precision cannot be very good. Figure 3 shows the distributions of the precision values for the chainy problems. In each plot the left set of points are for those problems where an adequate set of axioms was selected, and the right set of point are for those problems where an inadequate set of axioms was selected. For the majority of problems the precision in less that 0.1, i.e., less than 10% of selected axioms are used in a proof.
As was noted in the introduction to this paper, while metrics such as those presented in this paper are useful for quick evaluation of axiom selection techniques, the “proof is in the pudding”. The quality of the metrics needs to be established by comparing them with eventual ATP system performance. An initial evaluation of the precision metric has been performed by using the Vampire and Q∞ axiom selections, and looking at the performance of E on the resultant reduced problems. This was done for the 1551 bushy problems and 1369 chainy problems for which there are known minimally adequate axiom sets, so that the precision could be computed. The testing was done with a 300s CPU time limit on computers with a dual-core Intel(R) Xeon(R) E5-2609 2.50GHz CPU, 8GB memory, and running the CentOS Linux release 7.6.1810 operating system. The results are shown in Table 3.
In all four cases the precision of the unsolved problems is much lower than for the solved problems - the precision metric aligns correctly with the solvability of the reduced problems. The numbers of problems with precision 0.00 and 1.00 also align with the numbers of solutions, with higher numbers of solved problems with precision 1.00, and higher numbers of unsolved problems with precision 0.00. Overall, these results indicate that the precision metric does correctly evaluate the quality of the axiom selection.
The attentive reader might have noticed that there are some solved problems with precision 0.00, which is weird because the precision should be 0.00 only if the selected axioms are not an adequate set (Section 2.2). This indicates that these experiments revealed some new minimally adequate sets of axioms for some problems in the MPTP2078 corpus, and thus that some further 1551 Bushy problems # Problems Avg Prcn # Prcn 0.00 # Prcn 1.00 1369 Chainy problems # Problems Avg Prcn # Prcn 0.00 # Prcn 1.00 pruney problems need to be created.
The main contribution of this paper is metrics for evaluating axiom selection techniques without having to run an ATP system on the reduced problems. Three new axiom selection techniques have also been presented. Results from evaluating the new techniques and the axiom selection in the Vampire ATP system have been presented.
Future work includes a more comprehensive evaluation of the metrics, to confirm that the
metrics do provide a meaningful evaluation of the axiom selection techniques. It will also be
interesting to apply the metrics to the axiom selection techniques found in other ATP systems
such as E, GKC [
The results show that there is lots of room for further research and improvement in axiom
selection. We are currently investigating the use of network propagation [