Bridge and colleagues have developed a methodology of machine learning for theorem proving that uses real-valued features of the problem at hand and determines in a rigorous manner and with fewer preconceptions the possible connections between feature values and the best heuristic to use. They have chosen the five most-used heuristics from the E theorem prover, using as learning methods support vector machines or Gaussian processes; then, they applied their methodology to a large collection of problems taken from the Thousands of Problems for Theorem Provers (TPTP) library as a training set from which to learn.

Rather than learning the form of the heuristic itself, they make use of known good heuristics (as mentioned, the five most used) and learn to select an appropriate one. Also, instead of using accuracy to measure performance, they show as a better parameter to use the Matthews correlation coefficient. The difference is that accuracy only takes into account the true positives and the true negatives (the sum of them divided by the size of number of tests), whereas the Matthews correlation coefficient uses also the false positives and false negatives, and the denominator is far more than only the crude size of tests, instead using the square root of all combinations of products of sums among true and false positives, and true and false negatives.

They demonstrate that machine learning can effectively be applied to theorem proving. While they did not study the sharing factor specifically in terms of its effectiveness in identifying a heuristic, they have found that dynamic features in general have provided little or no increase in performance when used in addition to static features.

I strongly recommend this paper to specialists and advanced students of machine learning and automatic theorem proving.