面向高阶逻辑的形式化自动证明技术研究

作     者：莫广帅 

作者单位：中国科学技术大学 

学位级别：硕士

导师姓名：熊焰;黄文超

授予年度：2021年

学科分类：08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

主      题：形式化证明 自动化 Coq 神经网络 Deep Q Network 

摘      要：当今,软件系统是否可信已经成为一个国家经济能否正常运转的关键因素之一。作为保障软件系统安全的有效手段,形式化方法以数理逻辑为基础,利用规约、建模和验证等手段验证软件的可靠性。相比一阶逻辑,高阶逻辑接受谓词作为参数,描述能力强,更易完成复杂软件模型的构建。在传统的高阶逻辑证明工具中,主要采用手工式的定理证明方法,学习难度大,人工成本高。因此,有研究者提出了融合模式匹配、机器学习等技术的自动化证明方法。但是这些工作在证明定理的过程中存在状态搜索爆炸问题,验证效率低、代价高。本文结合证明辅助工具Coq,针对定理证明过程中的语法树搜索关键技术展开研究,提出一种基于强化学习Deep Q Network(DQN)的动态搜索框架,提高自动证明的效率。本文开展的主要工作有:1.基于注意力机制的命令生成技术。为了预测定理证明过程中的命令(策略和参数),本文结合Gated Recurrent Unit(GRU)、Long Short-Term Memory Network(LSTM)等深度学习网络,设计了一种形式化命令预测技术。传统的命令生成方法存在命令生成不灵活、准确率不高等问题,本文有效地提取了定理中的信息,依据证明目标、上下文前提和当前策略三个特征,构建向量,针对策略和参数分别设计了相应的预测模型。在训练的过程中,模型结合注意力机制,捕捉重要的信息,减少了无用信息的干扰。实验结果表明,本文模型预测的证明命令在准确度方面高于现有工作。2.面向高阶逻辑的定理语法树搜索技术。为了解决在定理证明过程中搜索空间爆炸的问题,本文结合强化学习DQN,提出一种基于动态策略的定理证明框架。与监督学习相比,该方法不需要数据集进行神经网络训练,DQN能够自动优化当前的选择,找到正确的证明路径,完成证明的定理。为了将复杂的证明过程抽象成一个简单的、易交互的过程,本文将提取到的目标和上下文信息保存在定理树的节点中,以供DQN进行学习。本文设计了一种独热编码,解决了当前证明状态难以提取成特征向量的难题。此外,本文设计了检测算法以防止DQN算法在搜索定理树的过程中产生循环,避免证明的失败。在形式化项目CompCert中的实验表明,本工作证明定理的成功率达到了 14.5%.