基于符号权重的一阶逻辑前提选择方法

刘清华; 李瑞杰; 朱绪胜; 陈代鑫

doi:10.3969/j.issn.0258-2724.20220478

基于符号权重的一阶逻辑前提选择方法

doi: 10.3969/j.issn.0258-2724.20220478

1.
成都飞机工业（集团）有限责任公司，四川成都 610091
2.
西南交通大学交通运输与物流学院，四川成都 611756

基金项目: 国家自然科学基金（72101217）

详细信息

作者简介:
刘清华（1992—），女，工程师，博士，研究方向为自动推理，E-mail：qhliu@my.swjtu.edu.cn

通讯作者:
李瑞杰（1990—），男，讲师，博士，研究方向为智能控制，E-mail：ruijie-li@swjtu.edu.cn

中图分类号: TP399
计量
- 文章访问数: 299
- HTML全文浏览量: 86
- PDF下载量: 37
- 被引次数: 0
出版历程
- 收稿日期: 2022-07-12
- 修回日期: 2023-03-14
- 网络出版日期: 2023-05-05
- 刊出日期: 2023-03-24

First-Order Logical Premise Selection Method Based on Symbol Weight

1.
Avic Chengdu Aircraft Industrial (Group) Co. Ltd., Chengdu 610091, China
2.
School of Transportation and Logistics, Southwest Jiaotong University, Chengdu 611756, China

摘要

摘要:
为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力，首先，提出符号权重计算公式，基于符号在问题中出现的频率获取不同符号对应的权重；其次，提出相关度计算公式，利用分配的符号权重计算问题中前提和结论间的相关度；同时，研究自适应相关度边界，用于判断前提与给定的结论是否相关；最后，在自动定理证明器中交互地结合前提选择和自动推理两个过程，可在充分选择相关前提的情况下及时停止前提选择过程. 实验结果表明：在最优情况下，新提出的前提选择方法能够把参与证明的平均前提数量从1876个降低到174个；与广泛使用的前提选择方法E-SInE和Vampire-SInE相比，使用新方法能够帮助自动定理证明器E在MPTP2078基准测试集上分别提高19.49%和10.49%的证明率.
- 前提选择 /
- 自动定理证明 /
- 一阶逻辑
Abstract:
To enhance the ability of automated theorem provers to select relevant premises from large-scale premises of first-order logic problems, a symbol weight calculation formula is first proposed, obtaining various weights corresponding to different symbols based on the frequency of symbols in the problem. Secondly, the correlation calculation formula is proposed, using assigned symbol weights to compute the correlation between a premise and the conjecture in a problem. At the same time, the adaptive correlation boundary is studied, which is used to determine whether the premise is correlated with the given conjecture. Finally, both processes of premise selection and automated reasoning are interactively combined in automated theorem provers, achieving the goal of stopping the premise selection process in time when the relevant premises are fully selected. The experimental results show that in the optimal case, the proposed premise selection method can reduce the average number of premises involving in proving process from 1876 to 174, and compared with widely used premise selection methods E-SInE and Vampire-SInE in automated theorem provers, the propoed method can help the automated theorem prover E improve the proof rate by 19.49% and 10.49% respectively on the MPTP2078 benchmark.
- premise selection /
- automated theorem proving /
- first-order logic

HTML全文

表 1 MPTP2078问题库描述

Table 1. Description of MPTP2078 benchmark 个

项目	公式	结论	最小前提	最大前提	平均前提	符号
数量	4564	2078	10	4563	1876	784

下载: 导出CSV

表 2 参与实验的基于符号的前提选择方法的说明

Table 2. Description of symbol-based premise selection methods in experiments

前提选择方法	说明
no-selection	不使用任何前提选择
SInE^[19]	基于触发关系的前提选择
LightWeight^[18]	基于符号轻量相关性的前提选择
SymbolWeight	新提出的基于符号权重的前提选择

下载: 导出CSV

表 3 自动定理证明器E在SymbolWeight下的证明性能

Table 3. Performance of automated theorem prover E with SymbolWeight

$ K $	证明数量/个	平均选择前提数量/个	选择精确度	选择度
2	288	13.0	0.358	0.054
4	599	22.6	0.336	0.060
6	818	33.3	0.322	0.054
8	862	44.5	0.309	0.053
10	920	55.9	0.302	0.055
12	932	68.4	0.295	0.057
14	967	81.1	0.288	0.059
16	980	94.0	0.285	0.060
18	1003	106.3	0.280	0.061
20	1014	117.3	0.278	0.061
22	1028	128.7	0.275	0.064
24	1045	140.7	0.271	0.068
26	1057	151.5	0.268	0.070
28	1071	162.4	0.265	0.074
30	1077	174.2	0.264	0.076

下载: 导出CSV

表 4 自动定理证明器E在不同的基于符号的前提选择方法下的证明性能

Table 4. Performance of automated theorem prover E with different symbol-based premise selection methods

前提选择方法	证明数量/个	证明率/%
no-selection	663	30.90
E-SInE	672	32.34
Vampire-SInE	859	41.34
SymbolWeight	1077	51.83

下载: 导出CSV

参考文献(29)

[1]	DARWICHE A. Compiling knowledge into decomposable negation normal form[C]//Proceedings of the Sixteenth International Joint Conference on Artifical Intelligence. New York: ACM, 1999: 284-289.
[2]	KERN C, GREENSTREET M R. Formal verification in hardware design: a survey[J]. ACM Transactions on Design Automation of Electronic Systems, 1999, 4(2): 123-193. doi: 10.1145/307988.307989
[3]	JACKSON D, SCHECHTER I, SHLYAHTER H. Alcoa: the alloy constraint analyzer[C]//Proceedings of the 22nd International Conference on Software Engineering. New York: ACM, 2000: 730-733.
[4]	LEROY X. Formal verification of a realistic compiler[J]. Communications of the ACM, 2009, 52(7): 107-115.
[5]	KLEIN G, ELPHINSTONE K, HEISER G, et al. seL4: Formal verification of an OS kernel[C]//Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. New York: ACM, 2009: 207-220
[6]	KAUTZ H, SELMAN B. Planning as satisfiability[C]// Proceedings of the 10th European Conference on Artificial Intelligence. New York: ACM, 1992: 359-363.
[7]	RINTANEN J, HELJANKO K, NIEMELÄ I. Planning as satisfiability: parallel plans and algorithms for plan search[J]. Artificial Intelligence, 2006, 170(12/13): 1031-1080.
[8]	LARRABEE T. Test pattern generation using boolean satisfiability[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992, 11(1): 4-15. doi: 10.1109/43.108614
[9]	WOOD R G, RUTENBAR R A. FPGA routing and routability estimation via Boolean satisfiability[J]. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 1998, 6(2): 222-231. doi: 10.1109/92.678873
[10]	EGGERSGLUSS S, DRECHSLER R. Efficient data structures and methodologies for SAT-based ATPG providing high fault coverage in industrial application[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2011, 30(9): 1411-1415. doi: 10.1109/TCAD.2011.2152450
[11]	CLARKE E, KROENING D, LERDA F. A tool for checking ANSI-C programs[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springe, 2004: 168-176.
[12]	LENAT D. CYC: a large-scale investment in knowledge infrastructure[J]. Communications of the ACM, 1998, 38(11): 33-38.
[13]	NILES I, PEASE A. Towards a standard upper ontology[C]//Proceedings of the international conference on Formal Ontology in Information Systems. New York: ACM, 2001: 2-9.
[14]	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
[15]	SUTCLIFFE G, PUZIS Y. SRASS-A semantic relevance axiom selection system[C]//International Conference on Automated Deduction. Berlin: Springer, 2007: 295-310.
[16]	PUDLÁK P. Semantic selection of premisses for automated theorem proving[C]//Cade-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. Bremen: [s.n.], 2007: 1-18.
[17]	ROEDERER A, PUZIS Y, SUTCLIFFE G. Divvy: an ATP meta-system based on axiom relevance ordering[C]//International Conference on Automated Deduction. Berlin: Springer, 2009: 157-162.
[18]	MENG J, 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
[19]	HODER K, VORONKOV A. Sine Qua Non for large theory reasoning[C]//International Conference on Automated Deduction. Berlin: Springer, 2011: 299-314.
[20]	ALAMA J, HESKES T, KÜHLWEIN D, et al. Premise selection for mathematics by corpus analysis and kernel methods[J]. Journal of Automated Reasoning, 2014, 52(2): 191-213. doi: 10.1007/s10817-013-9286-5
[21]	KALISZYK C, URBAN J, VYSKOCIL J. Efficient semantic features for automated reasoning over large theories[C]//Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Palo Alto: AAAI Press, 2015: 3084-3090.
[22]	PIOTROWSKI B, URBAN J. ATPboost: learning premise selection in binary setting with ATP feedback[C]//International Joint Conference on Automated Reasoning. Cham: Springer, 2018: 566-574.
[23]	IRVING G, SZEGEDY C, ALEMI A A, et al. Deep-math−deep sequence models for premise selection[C]// Proceedings of the 30th International Conference on Neural Information Processing Systems. New York: Curran Associates Inc. , 2016: 2243-2251.
[24]	WANG M Z, TANG Y H, WANG J, et al. Premise selection for theorem proving by deep graph embedding[C]//Proceedings of the 31st International Conference on Neural Information Processing Systems. New York: ACM, 2017: 2787-2797.
[25]	CROUSE M, ABDELAZIZ I, CORNELIO C, et al. Improving graph neural network representations of logical formulae with subgraph pooling[C]// KDD’20 Deep Learning on Graphs Workshop. San Diego: [s.n.], 2019: 1-7.
[26]	LIU Q H, XU Y, HE X X. Attention recurrent cross-graph neural network for selecting premises[J]. International Journal of Machine Learning and Cybernetics, 2022, 13(5): 1301-1315. doi: 10.1007/s13042-021-01448-9
[27]	刘清华,徐扬,吴贯锋,李瑞杰. 基于边权重图神经网络的一阶逻辑前提选择[J]. 西南交通大学学报,2022,57(6): 1368-1375. doi: 10.3969/j.issn.0258-2724.20210134 LIU Q H, XU Y, WU G F, et al. Edge-eighted-based graph neural network for first-order premise selection[J]. Journal of Southwest Jiaotong University, 2022, 57(6): 1368-1375. doi: 10.3969/j.issn.0258-2724.20210134
[28]	HARRISON J. Handbook of practical logic and automated reasoning[M]. Cambridge: Cambridge University Press, 2009.
[29]	LIU Q H, WU Z S, WANG Z H, et al. Evaluation of axiom selection techniques[C]// 10th International Joint Conference on Automated Reasoning. Paris: CEUR-WS, 2020: 63-75.