Machine Learning for First-Order Theorem Proving Learning to Select a Good Heuristic

被引:54
作者
Bridge, James P. [1 ]
Holden, Sean B. [1 ]
Paulson, Lawrence C. [1 ]
机构
[1] Univ Cambridge, Comp Lab, Cambridge CB3 0FD, England
基金
英国工程与自然科学研究理事会;
关键词
Automatic theorem proving; Machine learning; First-order logic with equality; Feature selection; Support vector machines; Gaussian processes; CLASSIFICATION; SAT;
D O I
10.1007/s10817-014-9301-5
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
We applied two state-of-the-art machine learning techniques to the problem of selecting a good heuristic in a first-order theorem prover. Our aim was to demonstrate 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. Selecting from a set of 5 heuristics, the learned results are better than any single heuristic. The same results are also comparable to the prover's own heuristic selection method, which has access to 82 heuristics including the 5 used by our method, and which required additional human expertise to guide its design. One version of our system is able to decline proof attempts. This achieves a significant reduction in total time required, while at the same time causing only a moderate reduction in the number of theorems proved. To our knowledge no earlier system has had this capability.
引用
收藏
页码:141 / 172
页数:32
相关论文
共 49 条
[1]  
[Anonymous], 1961, PRINCIPLES NEURODYNA
[2]  
[Anonymous], 2007, CEUR Workshop Proceedings. ESARLT 257, P45
[3]  
[Anonymous], 1973, Pattern Classification and Scene Analysis
[4]  
[Anonymous], 2006, Pattern recognition and machine learning
[5]  
Bache K., 2013, UCI Machine Learning Repository
[6]   Assessing the accuracy of prediction algorithms for classification: an overview [J].
Baldi, P ;
Brunak, S ;
Chauvin, Y ;
Andersen, CAF ;
Nielsen, H .
BIOINFORMATICS, 2000, 16 (05) :412-424
[7]  
Bridge J.P., 2010, UCAMCLTR792 U CAMBR
[8]  
Christianini N., 2000, INTRO SUPPORT VECTOR, P189
[9]   Biomarker discovery in microarray gene expression data with Gaussian processes [J].
Chu, W ;
Ghahramani, Z ;
Falciani, F ;
Wild, DL .
BIOINFORMATICS, 2005, 21 (16) :3385-3393
[10]   A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY [J].
DAVIS, M ;
PUTNAM, H .
JOURNAL OF THE ACM, 1960, 7 (03) :201-215