Enigma: Efficient Learning-Based Inference Guiding Machine
INTELLIGENT COMPUTER MATHEMATICS(2017)
摘要
ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many previous proof searches are classified as positive and negative based on their participation in the proofs. An efficient classification model is trained on this data, classifying a clause as useful or un-useful for the proof search. This learned classification is used to guide next proof searches prioritizing useful clauses among other generated clauses. The approach is evaluated on the E prover and the CASC 2016 AIM benchmark, showing a large increase of E's performance.
更多查看译文
关键词
Proof Search, Clause Selection, Saturation-based Theorem Provers, leanCoP, Skolem Symbols
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络