Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Machine learning for first-order theorem proving
Bridge J., Holden S., Paulson L. Journal of Automated Reasoning53 (2):141-172,2014.Type:Article
Date Reviewed: Jun 29 2015

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).

Reviewer:  George Hacken Review #: CR143562 (1509-0812)
Bookmark and Share
  Editor Recommended
Featured Reviewer
 
 
Learning (I.2.6 )
 
 
Feature Evaluation And Selection (I.5.2 ... )
 
 
Gaussian Quadrature (G.1.4 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Learning": Date
Learning in parallel networks: simulating learning in a probabilistic system
Hinton G. (ed) BYTE 10(4): 265-273, 1985. Type: Article
Nov 1 1985
Macro-operators: a weak method for learning
Korf R. Artificial Intelligence 26(1): 35-77, 1985. Type: Article
Feb 1 1986
Inferring (mal) rules from pupils’ protocols
Sleeman D.  Progress in artificial intelligence (, Orsay, France,391985. Type: Proceedings
Dec 1 1985
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy