Automatic theorem provers, which today are no longer new things, can be said to be powerful tools in, for example, high-assurance design and verification of systems. Humans certainly need theorem provers’ help for many types of today’s complex systems, as the existence of 35,000 machine-generated proofs that underlie a safety-critical system with which I’m familiar would indicate. However, the proof engines also need human help, which has heretofore been realized via trial-and-error choices of heuristics. The evolution of machine learning has brought the computer to bear on finding such aids to automatic proof. The authors show “that sufficient information is available from simple feature measurements of a conjecture and axioms to determine a good choice of heuristic, and that the choice process can be automatically learned.”

The paper is superbly organized, the heart of it comprising four parts: “The Problem,” “Machine Learning Methods,” “Experiments,” and “Results.” But surrounding these are a substantive introduction, a “Further Experiment,” and “Discussion and Further Work.” The E theorem prover and some of its associated heuristics figure prominently in this paper, and its treatment here has certainly widened my formal methods horizons. Regarding machine learning, the section on training, optimization, and test data explicates the authors’ solid methodology, which will support their results’ credibility. The machine learning complement of the paper is equally detailed and well written.

The scope and detail of this outstanding paper are amazingly achieved within 30-odd pages. I strongly commend this paper, even to such relatively faint-hearted persons as myself (who derived a great deal from it).