基于机器学习分类算法的前提选择技术研究

Research on Premise Selection Technology Based on Machine Learning Classification Algorithm

前提选择是提高定理自动证明成功率的关键技术,可以根据证明目标的相关性选择最有可能成功证明当前猜想的引理。已有的前提选择算法推荐的引理相关度不高,无法进一步提高定理的自动证明能力。针对以上问题,文章提出一种基于机器学习分类算法的组合方案,从公式结构和符号之间的依赖关系出发,提取有效特征向量集,并在k-近邻算法和朴素贝叶斯算法的基础上引入LDA主题词提取技术,进一步捕捉符号和依赖项之间的相关性,使得最后的组合算法预测的准确性更高。实验结果表明,该方案推荐的引理比现有的前提选择算法相关性更高,可以有效提高定理自动证明的成功率。

Premise selection is the key technology to improve the success rate of automatic theorem provfl It can choose the lemma which is most likely to prove the current conjecture successfully according to the relevance of the proving goal.However,the relevance of the lemmas recommended by the existing premise selection algorithm is not high,and the automatic proof ability of the theorem cannot be further improved.To solve the above problems,a combination algorithm based on machine learning classification is proposed.The scheme starts from the relationship between formula structure and symbols,extracts effective feature vector set,and introduces LDA topics extraction techniques on the basis of^-nearest neighbor algorithm and naive Bayes algorithm to farther capture the correlation between symbols and dependencies,which makes the final combination algorithm more accurate.Experimental results show that this method has higher accuracy than that the existing premise selection algorithm,and can effectively improve the success rate of automatic theorem provf.