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

Command Generation Technology for Formal Proof

随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于注意力机制的命令预测框架,将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).