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

doi:10.3969/j.issn.1671-1122.2021.11.002

信息网络安全 ›› 2021, Vol. 21 ›› Issue (11): 9-16.doi: 10.3969/j.issn.1671-1122.2021.11.002

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

熊焰¹, 程传虎²(), 武建双³, 黄文超¹

1.中国科学技术大学计算机科学与技术学院,合肥 230026
2.中国科学技术大学网络空间安全学院,合肥 230026
3.合肥天帷信息安全技术有限公司,合肥 230009

收稿日期:2021-06-21 出版日期:2021-11-10 发布日期:2021-11-24
通讯作者: 程传虎 E-mail:cchpersonal@163.com
作者简介:熊焰（1960—）,男,安徽,教授,博士,主要研究方向为计算机网络与信息安全、移动计算与移动网络、分布式处理|程传虎（1993—）,男,河南,硕士研究生,主要研究方向为软件自动化验证、机器学习|武建双（1984—）,男,山西,硕士,主要研究方向为网络安全等级保护|黄文超（1982—）,男,湖北,副教授,博士,主要研究方向为信息安全、人工智能、移动计算、网络与系统安全自动化验证
基金资助:
国家自然科学基金(61972369)

Research on Premise Selection Technology Based on Machine Learning Classification Algorithm

XIONG Yan¹, CHENG Chuanhu²(), WU Jianshuang³, HUANG Wenchao¹

1. Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China
2. Department of Cyberspace Security, University of Science and Technology of China, Hefei 230026, China
3. Hefei Tianwei Information Security Technology Co., Ltd, Hefei 230009, China

Received:2021-06-21 Online:2021-11-10 Published:2021-11-24
Contact: CHENG Chuanhu E-mail:cchpersonal@163.com

摘要/Abstract

摘要：

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

关键词: 定理自动证明, 前提选择, LDA主题提取, Coq证明助手

Abstract:

Premise selection is the key technology to improve the success rate of automatic theorem provf. 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 k-nearest neighbor algorithm and naive Bayes algorithm to further 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.

Key words: automatic theorem proving, premise selection, LDA topics extraction, Coq proof assistant

中图分类号:

TP309

熊焰, 程传虎, 武建双, 黄文超. 基于机器学习分类算法的前提选择技术研究[J]. 信息网络安全, 2021, 21(11): 9-16.

XIONG Yan, CHENG Chuanhu, WU Jianshuang, HUANG Wenchao. Research on Premise Selection Technology Based on Machine Learning Classification Algorithm[J]. Netinfo Security, 2021, 21(11): 9-16.

图/表 7

图1

图2

图3

表1

图4

图5

图6

参考文献 16

[1]	BLANCHETTE J C, KALISZYK C, PAULSON L C, et al. Hammering Towards QED[J]. Journal of Formalized Reasoning, 2016, 9(1):101-148.
[2]	BARRETT C, TINELLI C. Satisfiability Modulo Theories[M]. Cham: Springer, 2018.
[3]	ZHANG Hengruo, FU Ming. Design and Implementation of CoQ Automatic Proof Strategy Based on Z3[J]. Journal of Software, 2017, 28(4):819-826.
	张恒若, 付明. 基于Z3的Coq自动证明策略的设计和实现[J]. 软件学报, 2017, 28(4):819-826.
[4]	MENG Jia, PAULSON L C. Lightweight Relevance Filtering for Machine-generated Resolution Problems[J]. Journal of Applied Logic, 2009, 7(1):41-57. doi: 10.1016/j.jal.2007.07.004 URL
[5]	JONES K S. A Statistical Interpretation of Term Specificity and Its Application in Retrieval[J]. Journal of Documentation, 1972, 28(1):11-21. doi: 10.1108/eb026526 URL
[6]	ROEDERER A, PUZIS Y, SUTCLIFFE G. Divvy: An ATP Meta-system Based on Axiom Relevance Ordering[C]// Springer. International Conference on Automated Deduction, August 2-7, 2009, Montreal, QC, Canada. Heidelberg: Springer, 2009: 157-162.
[7]	JAKUBŮV J, URBAN J. Hammering Mizar by Learning Clause Guidance[EB/OL]. https://arxiv.org/pdf/1904.01677.pdf, 2019-04-02.
[8]	FÄRBER M, KALISZYK C. Random Forests for Premise Selection[C]// Springer. International Symposium on Frontiers of Combining Systems, September 21-24, 2015, Wroclaw, Poland. Cham: Springer, 2015: 325-340.
[9]	PIOTROWSKI B, URBAN J. ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback[C]// Springer. International Joint Conference on Automated Reasoning, July 14-17, 2018, Oxford, UK. Cham: Springer, 2018: 566-574.
[10]	KÜHLWEIN D, VAN LAARHOVEN T, TSIVTSIVADZE E, et al. Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics[C]// Springer. International Joint Conference on Automated Reasoning, June 26-29, 2012, Manchester, UK. Heidelberg: Springer, 2012: 378-392.
[11]	KALISZYK C, URBAN J. Mizar 40 for Mizar 40[J]. Journal of Automated Reasoning, 2015, 55(3):245-256. doi: 10.1007/s10817-015-9330-8 URL
[12]	URBAN J, SUTCLIFFE G, PUDLÁK P, et al. MaLARea SG1-machine Learner for Automated Reasoning with Semantic Guidance[C]// Springer. International Joint Conference on Automated Reasoning, August 12-15, 2008, Sydney, Australia. Heidelberg: Springer, 2008: 441-456.
[13]	PIOTROWSKI B, URBAN J. Stateful Premise Selection by Recurrent Neural Networks[EB/OL]. https://arxiv.org/abs/2004.08212, 2020-03-11.
[14]	CHVALOVSKÝ K, JAKUBŮV J, SUDA M, et al. ENIGMA-NG: Efficient Neural and Gradient-boosted Inference Guidance for E[C]// Springer. International Conference on Automated Deduction, August 27-30, 2019, Natal, Brazil. Cham: Springer, 2019: 197-215.
[15]	FERREIRA D, FREITAS A. Premise Selection in Natural Language Mathematical Texts[EB/OL]. https://www.researchgate.net/publication/343296926_Premise_Selection_in_Natural_Language_Mathematical_ Texts, 2020-12-11.
[16]	KALISZYK C, URBAN J, MICHALEWSKI H, et al. Reinforcement Learning of Theorem Proving[EB/OL]. https://arxiv.org/pdf/1805.07563.pdf, 2018-12-03.

	Math Classes	CoRN
定理（引理）数量	2730	4941
特征数量	63629	90378
依赖数量	30053（2415 unique）	30531（4363 unique）

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

Research on Premise Selection Technology Based on Machine Learning Classification Algorithm

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 7

参考文献 16

相关文章 15

编辑推荐

Metrics

本文评价

[1]	朱艳华, 廖方宇, 胡良霖, 王志强. 科学数据安全标准规范关键问题探索[J]. 信息网络安全, 2021, 21(11): 1-8.
[2]	赵小林, 赵斌, 赵晶晶, 薛静锋. 基于攻击识别的网络安全度量方法研究[J]. 信息网络安全, 2021, 21(11): 17-27.
[3]	夏喆, 罗宾, 徐桂彬, 肖新秀. 智能电网中支持细粒度访问控制的隐私保护数据聚合方案[J]. 信息网络安全, 2021, 21(11): 28-39.
[4]	王健, 于航, 韩臻, 韩磊. 基于智能合约的云存储共享数据访问控制方法[J]. 信息网络安全, 2021, 21(11): 40-47.
[5]	雷雨, 刘佳, 李军, 柯彦. 一种基于条件生成对抗网络的图像隐写方法研究与实现[J]. 信息网络安全, 2021, 21(11): 48-57.
[6]	李桐, 周小明, 任帅, 徐剑. 轻量化移动边缘计算双向认证协议[J]. 信息网络安全, 2021, 21(11): 58-64.
[7]	李坤昌, 石润华, 李恩. 智能电网中数据聚合与用户查询隐私保护研究[J]. 信息网络安全, 2021, 21(11): 65-74.
[8]	于克辰, 郭莉, 姚萌萌. 基于区块链的高价值数据共享系统设计[J]. 信息网络安全, 2021, 21(11): 75-84.
[9]	吴佳洁, 吴绍岭, 王伟. 基于TCN和注意力机制的异常检测和定位算法[J]. 信息网络安全, 2021, 21(11): 85-94.
[10]	谭茹涵, 左黎明, 刘二根, 郭力. 基于图像特征融合的恶意代码检测[J]. 信息网络安全, 2021, 21(10): 90-95.
[11]	肖帅, 张翰林, 咸鹤群, 陈飞. 一种面向物联网设备的口令认证密钥协商协议[J]. 信息网络安全, 2021, 21(10): 83-89.
[12]	胡景秀, 杨阳, 熊璐, 吴金坛. 国密算法分析与软件性能研究[J]. 信息网络安全, 2021, 21(10): 8-16.
[13]	程顺航, 李志华. 基于MRC的威胁情报实体识别方法研究[J]. 信息网络安全, 2021, 21(10): 76-82.
[14]	马骁, 蔡满春, 芦天亮. 基于CNN改进模型的恶意域名训练数据生成技术[J]. 信息网络安全, 2021, 21(10): 69-75.
[15]	吴佳明, 熊焰, 黄文超, 武建双. 一种基于距离导向的模糊测试变异方法[J]. 信息网络安全, 2021, 21(10): 63-68.