面向形式化证明的命令生成技术  

Command Generation Technology for Formal Proof

作　　者：莫广帅 熊焰[2] 黄文超[2] MO Guang-Shuai;XIONG Yan;HUANG Wen-Chao(Cyberspace Security,University of Science and Technology of China,Hefei 230027,China;School of Computer Science and Technology,University of Science and Technology of China,Hefei 230027,China)

机构地区：[1]中国科学技术大学网络空间安全学院,合肥230027 [2]中国科学技术大学计算机科学与技术学院,合肥230027

出　　处：《计算机系统应用》2022年第1期273-278,共6页Computer Systems & Applications

基　　金：国家自然科学基金(61972369)。

摘　　要：随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于注意力机制的命令预测框架,将LSTM与Coq结合,预测定理证明过程中的策略和参数.实验结果表明本文提出的模型在生成命令的准确度方面高于现有工作(本工作预测命令准确率为28.31%).With the continuous increase in software scale, software security faces increasingly severe challenges. As an effective means of detecting software system security, formal proof aims to use mathematical methods to complete rigorous verification of software attributes. Commonly used formal proof methods prove theorems with pattern matching,which, however, suffer from defects such as incomplete strategy generation. This study proposes a command prediction framework based on the attention mechanism. It combines long short-term memory(LSTM) with Coq to predict the strategies and parameters during theorem proving. The experimental results show that the model proposed in this study is superior to existing ones in the accuracy of command generation(the accuracy of command prediction is 28.31% in this paper).

关 键 词：形式化证明 COQ 命令预测 LSTM 注意力机制 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论] TP309[自动化与计算机技术—计算机科学与技术]