First-Order Logical Premise Selection Method Based on Symbol Weight
-
摘要:
为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力,首先,提出符号权重计算公式,基于符号在问题中出现的频率获取不同符号对应的权重;其次,提出相关度计算公式,利用分配的符号权重计算问题中前提和结论间的相关度;同时,研究自适应相关度边界,用于判断前提与给定的结论是否相关;最后,在自动定理证明器中交互地结合前提选择和自动推理两个过程,可在充分选择相关前提的情况下及时停止前提选择过程. 实验结果表明:在最优情况下,新提出的前提选择方法能够把参与证明的平均前提数量从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.
-
Key words:
- premise selection /
- automated theorem proving /
- first-order logic
-
表 1 MPTP2078问题库描述
Table 1. Description of MPTP2078 benchmark
个 项目 公式 结论 最小前提 最大前提 平均前提 符号 数量 4564 2078 10 4563 1876 784 表 2 参与实验的基于符号的前提选择方法的说明
Table 2. Description of symbol-based premise selection methods in experiments
表 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 表 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 -
[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.20210134LIU 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.
计量
- 文章访问数: 278
- HTML全文浏览量: 83
- PDF下载量: 37
- 被引次数: 0