前提选择是解决自动定理证明器面对大规模问题时性能降低的有效方法。当前面向一阶逻辑中前提选择的主流图神经网络忽略了逻辑公式图内部的节点顺序信息。针对此问题，将一种面向高阶逻辑公式的保序方法拓展到一阶逻辑中，并提出了一种基于treelet的图神经网络模型。该模型在信息聚合时一部分聚合中心节点的父、子节点信息，另一部分聚合节点顺序信息。实验分析表明：基于treelet的图神经网络模型在前提选择任务中比最优的主流图神经网络模型的分类准确率提高了约2%。

Premise selection is an efficient method to address the performance degradation of automated theorem provers when facing large-scale problems. Currently, the mainstream graph neural networks for premise selection in first-order logic ignore the node order information inside logic formula graphs. To solve the above problem, an order-preserving method for higher-order logical formulas is extended to first-order logic, and a treelet-based graph neural network model is proposed. The model aggregates the information of neighbor nodes in two parts: One part aggregates parent and child node information of the central node, the other part aggregates the order information of the central node. Experimental analysis shows that, compared with the optimal mainstream graph neural network model, the treelet-based graph neural network model improves the classification accuracy by about 2% in the premise selection task. 


相关文章

[1]	陈子雄, 陈旭, 景永俊, 宋吉飞. 基于图神经网络的源代码漏洞检测研究综述[J]. 计算机工程与科学, 2024, 46(10): 1775-1792.
[2]	陈昌奉, 赵宏州, 周恺卿. 基于图神经网络的代码抄袭检测方法[J]. 计算机工程与科学, 2024, 46(10): 1815-1824.
[3]	张悦, 张磊, 刘佰龙, 梁志贞, 张雪飞. 基于时空Transformer的多空间尺度交通预测模型[J]. 计算机工程与科学, 2024, 46(10): 1852-1863.
[4]	袁佳伟, 赵进. 基于图神经网络的OMCI模型相似性计算[J]. 计算机工程与科学, 2024, 46(09): 1576-1586.
[5]	吴斯琦, 赵清华, 于雨晨. 基于元学习的图神经网络冷启动推荐[J]. 计算机工程与科学, 2024, 46(09): 1675-1684.
[6]	王谢中, 陈旭, 景永俊, 王叔洋. 基于异构图神经网络的半监督网站主题分类[J]. 计算机工程与科学, 2024, 46(04): 635-646.
[7]	余天赐, 高尚. 融合多结构信息的代码注释生成模型[J]. 计算机工程与科学, 2024, 46(04): 667-675.
[8]	李清风, 金柳, 马慧芳, 张若一. 双视图对比学习引导的多行为推荐方法[J]. 计算机工程与科学, 2024, 46(04): 707-715.
[9]	孙庆骁, 刘轶, 杨海龙, 王一晴, 贾婕, 栾钟治, 钱德沛. GNNSched：面向GPU的图神经网络推理任务调度框架[J]. 计算机工程与科学, 2024, 46(01): 1-11.
[10]	周菊香, 周明涛, 甘健侯, 徐坚. 多阶段时序和语义信息增强的问题生成模型[J]. 计算机工程与科学, 2023, 45(10): 1847-1857.
[11]	杨春霞, 桂强, 马文文, 徐奔, . 融合图游走信息的图注意力网络方面级情感分析[J]. 计算机工程与科学, 2023, 45(10): 1858-1865.
[12]	曹健, 陈怡梅, 李海生, 蔡强, . 基于图神经网络的行人轨迹预测研究综述[J]. 计算机工程与科学, 2023, 45(06): 1040-1053.
[13]	王扬, 陈智斌. 一种求解CVRP的动态图转换模型[J]. 计算机工程与科学, 2023, 45(05): 859-868.
[14]	罗可劲, 刘广聪, 杨文浩. 基于多任务学习的图神经网络推荐模型研究[J]. 计算机工程与科学, 2023, 45(04): 726-733.
[15]	杨春霞, 姚思诚, 宋金剑, . 基于词共现的方面级情感分析模型[J]. 计算机工程与科学, 2022, 44(11): 2071-2079.