-
摘要:
随着人工智能(artificial intelligence,AI)规模的快速增长,深度学习应用程序中出现的错误也日益增多. 现有主流深度学习框架大都建立在动态类型语言Python之上,缺乏类型检查机制,导致许多错误无法在编译阶段通过类型检查加以排除. 为此,提出了一种基于定理证明器Coq的强类型函数式编程风格的深度学习框架. 该框架具有带类型的张量结构和强大的静态类型检查能力. 实验结果表明,该框架能够自动有效检测到深度学习模型中的形状不匹配错误,相较于其他检查工具,在检测能力和速度方面具有更大优势. 进一步地,设计并实现了一套从函数式编程模型到C代码的重写转换规则,实现了从函数式神经网络算子表达式到多核并行OpenMP C代码的转换. 多组实验结果表明,该方法生成的算子C代码与手工编写的代码质量相当,且加入多核并行优化后生成的神经网络算子OpenMP C代码相较于顺序执行的算子C代码,速度提升了4~10倍. 此外,利用该方法生成的C算子具有高安全性,能够有效避免人工编写代码时常见的下标越界和存储分配错误等问题.
Abstract:As the scale of AI grows rapidly, errors in deep learning applications are also increasing. Existing popular deep learning frameworks are mostly built on the dynamically-typed language Python, which lacks type checking mechanisms. This leads to many errors that cannot be eliminated through type checking at the compilation stage. This paper proposes a strongly-typed functional programming style deep learning framework based on the theorem prover Coq. The framework features typed tensor structures and a powerful static type checking capability. The experimental results demonstrate that the framework can automatically, quickly, and effectively detect shape mismatch errors in deep learning models, and it has greater advantages in terms of speed and detection capability compared to other checking tools. Furthermore, this paper designs and implements a set of rewriting rules that translate functional programming models into C code, realizing the translation from functional neural network operator expressions to multi-core parallel OpenMP C code. According to the results of multiple sets of experiments, the C code for operators generated by this method is on par with manually written code. Furthermore, the speed of the generated neural network operator C code with multi-core parallel optimization has been improved by 4-10 times compared with the sequentially executed operator C code. Additionally, the generated C operators are highly secure and can effectively avoid common issues such as out-of-bounds indexing and memory allocation errors in manually written code.
-
网络通信逐渐成为现代社会运作的基础设施,个人、企业及政府机构都依赖网络进行信息和数据的传输,形成了规模庞大的网络大数据. 随之而来的是日益增长的网络安全威胁,黑客攻击、数据泄露等一系列恶意事件在物联网[1]、工业互联网[2]等众多领域中都造成了重大损失. 网络安全问题已经成为全球范围内关注的焦点,对于保护个人隐私、商业机密和国家安全都具有重要意义.
网络安全威胁源于异常的网络访问,例如链接和传输等. 这些访问的特征和目的随场景变化,但均与广泛存在的正常访问存在差异,且在全部访问中占比极低[3]. 现有研究提出了一系列异常访问检测方法,从访问日志文本、访问行为序列等多个角度进行识别. 其中最主流的思路是基于正常访问数据建立常态模型,进而评估待测数据与正常数据的相似度,若低于设定阈值则将其视为异常数据. 在此基础上,基于图结构的检测方法引入了网络实体与访问之间的复杂关联,进一步提高了检测效果[4-6].
然而,异常访问通常仅在部分属性字段中体现出显著的异常特性. 分布式拒绝服务(distributed denial of service,DDoS)攻击在时间方面的属性上呈现出集中的异常特性,但在传输内容方面的异常特性并不显著;SQL(structured query language)注入攻击在内容方面存在明显的异常特性,但在传输协议等方面与正常访问差异不大. DDoS和SQL二者体现异常特性的属性层次并不相同[7-8]. 异常特性在属性字段上的分布差异极大地影响了检测效果. 现有的异常访问检测方法忽略了异常特性仅在部分属性字段上显著的问题,往往将全部属性字段共同嵌入至低维空间,导致正常属性与异常属性相互混合. 不体现异常特性的属性被引入数据表示结果,造成了属性干扰问题,降低了检测效果. 图1展示了属性干扰问题对检测结果的影响.
为解决上述问题,本文提出了MNDetector,将多层网络(multiplex network)结构引入异常访问检测领域. 多层网络不仅能通过层次化的网络结构隔离属性字段之间的干扰,还能建立连接不同层网络的跨层边,捕捉不同层次间可能存在的隐式关联. 通过基于属性字段集的细粒度划分,弱化无关字段间的相互影响,在体现显著异常特性的属性层次进行检测以获得更准确的检测结果. 具体而言,通过对访问数据进行属性字段的频繁集分析,利用内部相关性较强的字段集构建单层网络并添加层间关联,形成多层网络,实现对字段的分层划分. 在此基础上,采用适应多层网络结构的跨层游走计算节点嵌入表示,进而利用分层生成对抗网络(generative adversarial network,GAN)计算未知节点的重构损失与判别结果,实现异常检测.
本文的主要贡献有4个方面:
1)将多层网络结构引入网络异常访问检测领域,提出了面向网络访问数据的多层网络形式化构建方法,解决了传统多层网络构建方法依赖人工定义且难以捕获深层关联的问题.
2)形式化地分析了现有检测方法面临的属性干扰问题,并针对性地提出MNDetector,利用多层网络分隔属性字段,避免异常特性不显著的字段干扰检测.
3)提出了面向多层网络的分层GAN机制以及分层检测结果的融合方法,通过融合各层的重构损失与判别结果,实现了分层信息的综合检测.
4)对分层检测结果进行了案例研究,通过不同层网络的结构差异直观地解释了检测结果,阐释了MNDetector能够获得更优效果的原因.
1. 相关工作
在真实应用场景中,访问数据往往是离散的,无法直接进行多层网络等复杂结构的构建. 此外,多层网络中的每层网络本质上为图结构,图学习的相关研究与本领域研究有着极大的相关性.
1.1 多层网络的构建与学习
多层网络是特殊的异构图,其在多个不同的视角或维度上划分数据样本,分别构建单层网络并在其间添加跨层连边. 多层网络的具体分层逻辑与方法并没有通行标准,在不同领域的应用中可以基于时空尺度、语义层级、先验知识等多种角度构建不同的多层网络,从而面向下游任务实现针对性的数据划分.
与多层网络相近的常用概念有3个:多维网络(multi-dimensional network)、分层网络(multi-network)和多视角图(multi-view graph). 其中,多维网络的概念与多层网络相同,存在二者混用的情况. 分层网络更为常见,即将原始数据构建为多个单层网络结构,但层与层之间没有直接的关联. 例如不同区域的网络拓扑、不同网络平台的用户关联等. 多视角图可以被视为多层网络的子集,其通过每层网络表示单一视角下的数据关联,如社交网络中的关注关系、好友关系、评论关系等. 多视角图中的跨层边往往表示不同视角间的关联,从而描述多个视角的交互模式.
多层网络并未直接划分数据集合,而是从属性字段集的视角出发对数据属进行划分,跨层边则体现了属性字段间的关联紧密程度. 因此其与上述概念均有所差异.
1.1.1 多层网络的构建
将原始数据转换为图结构是多层网络构建的第1步,其主要思想是利用节点表示原始数据中的每个样本,将数据特征转换为节点属性,将样本之间的关联转换为连接节点的边,通过边权重表示样本间的相似程度. Chu等人[9]提出了上述构建过程的核心思路,对于给定的节点组,利用高斯函数计算节点u与节点v之间的边权重wuv,其核心计算过程为
{w_{uv}} = {\text{exp}}\left(\frac{{ - \left\| {{{\boldsymbol h}_u} - {{\boldsymbol h}_v}} \right\|_2^k}}{{2{\varepsilon ^2}}}\right) \text{,} (1) 其中hu与hv为节点u与节点v的属性向量,ε与k均为人为指定的参数.
在此基础上,把若干单层网络连接成多层网络的方法包括人为定义和基于关联进行计算.
人为定义的方法主要依赖人工特征,例如通过单层网络之间的相似度设置层间关联的强弱[10],常用指标有余弦相似度、Jaccard相似度和Dice系数等. 若2层网络之间的相似度超过某个阈值,则为其添加跨层边. 这一思路的典型代表是Park等人[11]提出的DMGI,其定义了属性化的多层网络并将其应用于后续学习任务中.
基于关联的方法则利用应用场景中的关联关系构建跨层边,例如针对不同社交平台用户数据构建的多层网络,在表示相同账户使用人的节点之间添加连边等,因此其应用往往局限于具体场景.
1.1.2 多层网络的学习
Liu等人[12]总结了3类多层网络学习的实现方法.
第1类是把多层网络简单叠加,聚合每层网络中表示相同实体的节点,同时合并重合的边,即把多层网络转换为常规的单层网络,进而直接应用成熟的图学习方法. 这种方法可以直接复用现有的图表示学习方法,但效果不佳.
第2类是分别对每层网络进行嵌入,即针对每层网络复用现有的节点嵌入方法,最终将全部嵌入结果进行简单合并. 其本质是把多层网络看作彼此分离的单层网络,忽略了单层网络之间的关联关系.
第3类是能够进行跨层学习的方法. 相比于前2类方法,其采用的随机游走等机制能在学习过程中直接引入跨层结构信息[13-14].
除此之外,由于网络结构的相似性,部分面向多视角图的异常检测方法也可迁移应用至多层网络检测. 最具代表性的工作是ANOMULY[15],其侧重不同场景下的边结构,将分层计算的节点嵌入作为层次化的节点状态,利用门控循环单元(gate recurrent unit,GRU)捕获网络的时间特性以实现动态多层网络的异常检测. 然而其并未针对性设置多层网络节点间的跨层关联,且未具体分析属性字段,导致检测效果难以进一步上升. 类似地,AnomMAN[16]将不同层次网络的结构与属性嵌入到相同的子空间中,利用注意力机制融合嵌入结果,进而通过重构损失计算对应节点的异常分数.
总的来说,现有研究大多停留在表征学习的领域中,与具体应用场景结合不紧密,难以应用至真实的异常检测任务. 且现有多层网络构建方法大多完全依赖人为定义,可迁移性较差. 这些都为多层网络结构在异常检测领域的应用带来了阻碍.
1.2 图学习
图学习的目标是获取图结构的有效表征以支撑下游任务. 近年来,深度学习技术迅速发展,图深度学习方法被不断提出,正在逐步取代经典方法.
1.2.1 经典图学习方法
最经典的图学习方法是图信号处理(graph signal processing,GSP),其核心思路是将传统信号处理的方法迁移至图结构中[17]. GSP利用邻接矩阵、拉普拉斯矩阵等数据结构表示图,使用矩阵乘法实现滤波器的放缩作用. 这种方式是传统信号处理方法的拓展,不能对图进行有效的分解,且时间开销较大,仅在少数特定领域获得了应用.
在此基础上,研究者针对图结构的特点提出了矩阵分解方法,即对特征矩阵进行分解,在得到的低维矩阵中保留原始特征信息,将其作为图学习的结果. 基于矩阵分解的图学习可以分为基于拉普拉斯矩阵和基于邻接矩阵两大类,但由于这2类方法都需要存取大量矩阵,内存消耗较大,在应用中存在局限.
基于随机游走的图学习方法是应用较广的经典方法. 其通过节点之间的随机游走路径反映关联关系,其中影响力最大的方法是DeepWalk[18]和node2vec[13]. 在此基础上,Chanpuriya等人[19]、Zhai等人[20]针对社交、推荐等多个场景进一步发展了相关方法. 随机游走得到的游走路径和图结构之间存在紧密关联,在稀疏网络中表现优越. 但存在依赖随机概率、路径聚合方式难以选择等问题,需要根据应用场景进行细致调整.
1.2.2 图深度学习方法
图像处理等领域中的深度学习技术被不断迁移至图学习领域. 其代表是SDNE[21]及其改进与应用[22]、图卷积网络(graph convolutional network,GCN)[23]及其优化方法[24]等. 此外,针对拓扑不均衡[25]、子图结构[26]等重要问题也存在相应的学习方法研究. 其中,以GCN为代表的卷积方法成为了图学习的主流. 此类方法将特征矩阵作为输入,利用消息传递机制进行属性聚合,通过多轮迭代实现节点嵌入. 这种思路的进一步发展以SpecAE[27]为代表,其加入了反卷积层,使用高斯混合模型实现图学习. 注意力[28]、动态化[29]、信息瓶颈[30]等机制与理论的引入提高了图学习的有效性和稳定性.
另一种图深度学习的实现方法是将自编码器的思想与图神经网络相结合,变分图自编码器是此类方法的典型[31]. 其将邻接矩阵转换为含有节点属性信息的嵌入,同时使用矩阵的数量积进行解码,将解码后的邻接矩阵与原始邻接矩阵之间的交叉熵作为整体模型的损失函数. 在此基础上,GraphGAN[32]结合了随机游走和生成对抗机制,将图转化为最小生成树,从根节点开始游走,通过改变根节点来获得不同路径,进而通过最小化重构损失实现表征学习.
图深度学习方法避免了经典方法需要手动配置大量参数的问题,具有良好的普适性. 但由于现有模型普遍使用梯度下降等方法进行参数优化,其存在与神经网络相同的易陷入局部最优解、易发生梯度消失等问题. 总的来说,现有的图学习方法大多专注于单层结构,无法有效区分不同视角、不同属性字段并无法捕获其间的关联关系,因此无法直接应用于多层网络的学习.
1.3 异常检测
异常检测任务涉及到的场景非常丰富,且数据特征不同,需要根据具体场景选择相应的检测方法. 在现有方法中,部分研究直接将分类方法迁移应用至异常检测领域. 除此之外,针对异常数据自身的研究可以大体分为3类:基于统计的方法、基于聚类的方法和基于残差分析的方法[33].
1.3.1 基于统计的方法
基于统计的异常检测方法假定数据符合某种特定的统计分布,从而可对全体样本进行拟合以得到正常数据分布,不符合该分布的数据即被视为异常数据.
此类方法中最具代表性的是以扫描统计量作为异常指标的检测方法,Kulldorff统计量[34]、Poisson统计量[35]等一系列指标被逐步提出. Wang等人[36]进一步通过校准的非参数扫描统计量实现了真实场景下异常子图的有效检测.
统计方法是最基础的异常检测方法,在特定领域中有一定应用,但存在泛化性不足的问题.
1.3.2 基于聚类的方法
异常检测任务最基本的特性是数据标签的高偏分布,即绝大多数数据样本均为正常. 针对这种特殊性质,聚类方法被大量应用. 其核心思想是识别远离样本中心的少量样本并将其视为异常. 其中,最常用的是基于欧氏距离的聚类及其改进方法[37],在特征空间、嵌入空间等选定的空间中,距离更近的样本被认为更可能从属同一类别. 基于这一思路的NetWalk[38]使用基于欧氏距离的聚类方法进行异常检测,在多个场景中获得了较高的准确率.
1.3.3 基于残差分析的方法
基于残差分析的方法将原始数据编码后进行重构,由于正常数据占比远大于异常数据,因此重构结果趋向于正常数据模式,从而可以将原始数据与重构数据之间的重构损失作为异常指标.
深度自编码器[39]是此类方法的代表,其通过深度学习拟合正常数据模式以实现非监督的异常检测. 在此基础上,Ding等人[40]提出的AEGIS模型通过图差分编码网络构建编码器与解码器、计算待测节点的重构损失,获得了较高的准确率. Fan等人[41]进一步引入了图正则化项,保持了图数据局部结构的一致性,减少了检测时间并提高了鲁棒性.
总而言之,现有异常检测方法面对不同场景需要进行针对性的调整,迁移性较差,且大多仅作为表征学习的下游任务,与数据表征方法结合不紧密.
2. 问题定义
多层网络可被形式化地定义为图结构Graph={Nl, El, Ecross}l=1, 2, …, m,其中Nl为第l层网络的节点集合,El为其对应的边集合,Ecross为跨层边集合,m为网络层数. 进而异常访问检测可被转化为多层网络上的异常节点检测问题,即寻找特定的节点集合,其中节点的属性与其余节点显著不同.
各类基于图神经网络的检测方法推动了检测效果的提升,为多层网络异常检测提供了有效工具,但同时带来了严重的属性干扰问题.
2.1 图异常检测的属性干扰
以AnomMAN[16]和AnomalyDAE[42]等被广泛运用的基于重构的检测方法为例,当处理节点属性时,均方误差等损失函数会使相邻节点的属性表征趋同;当处理边结构时,迭代训练在使损失趋于零的同时会使得重构结构与原始结构相同,从而边重构方法同样会导致相邻节点的属性表征趋同.
在此过程中,节点u的属性表征可表示为
{\boldsymbol h}_u^{{\text{(}}t + 1{\text{)}}} = \sigma \left(\displaystyle\sum\limits_{n \in N{e_s}(u)} {{c_n}{\boldsymbol h}_n^{{\text{(}}t{\text{)}}} {{\boldsymbol W}^{{\text{(}}t{\text{)}}}}} \right) \text{,} (2) 其中{\boldsymbol h}_n^{{\text{(}}t{\text{)}}}为节点n在第t次迭代后的属性表征向量,cn为对应的权重,W(t)为可训练参数,σ为可选择的激活函数,Nes(u)为节点u的s阶之内的邻居节点集合.
对于相邻节点u与v,当训练使得损失趋于零时,其表征向量趋于相等. 由于在2次迭代后节点u可捕获到其2s阶之内的邻居信息,因此不失一般性地,可以使用相邻节点表征的关系作为训练结束的标志,即hu=hv. 从而在每次迭代中,模型将趋向于
{c_u}\left(\displaystyle\sum\limits_{n \in N{e_s}(u)} {{\boldsymbol h}_n^{(t)} {{\boldsymbol W}^{(t)}}} \right) = {c_v}\left(\displaystyle\sum\limits_{n \in N{e_s}(v)} {{\boldsymbol h}_n^{(t)} {{\boldsymbol W}^{(t)}}} \right) . (3) 针对每次具体的迭代过程,将hn按维度展开,考察第i个字段,可将式(3)转写为
{c_u}{{\boldsymbol W}_i}\left(\displaystyle\sum\limits_{n \in N{e_s}(u)} {{{h}_{ni}}} \right) = {c_v}{{\boldsymbol W}_i}\left(\displaystyle\sum\limits_{n \in N{e_s}(v)} {{{h}_{ni}}} \right) \text{,} (4) 其中Wi为模型参数矩阵的第i列,hni为节点n的第i维属性值.
对于固定的节点u与节点v,当u和v的邻居节点属性之和存在较大偏差时,模型训练会使得Wi变小,乃至趋近向量0,从而降低该属性字段的影响. 而当属性之和偏差较小时,Wi则会远离向量0,从而强化该字段的影响.
一般而言,对于能够体现异常特性的属性字段,由于取值与异常与否呈强相关,字段上各节点的属性和偏差较大,而不体现异常特性的属性字段则反之. 这使得图学习过程强化了不体现异常特性的属性字段的影响,抑制了异常特性显著的属性字段的影响,降低检测效果,造成属性干扰问题.
2.2 属性干扰的表现与影响
针对UNSW-NB15数据集[43]所构建的溯源图,考察每个属性字段对异常标签的区分度及其邻居节点属性和的波动性之间的关联. 该数据集的详细介绍如4.1.1节所示.
具体地,以每个字段对异常标签的信息增益代表其对异常的区分能力,使用变异系数作为取值波动性的评估标准. 图2展示了每个字段上信息增益与变异系数的关系,为保证展示效果清晰,信息增益低于0.1的字段被去除.
图2中,DoS与Generic是2类不同的异常访问. 从图2中可以看出,变异系数相差较大的属性字段信息增益也较高,这意味着对异常检测提供更多信息的字段被抑制,异常特性不显著的字段则产生了更大的影响,即属性干扰问题的存在对检测产生了负面影响.
另一方面,针对不同类型的异常访问,具有异常区分度的属性字段并不完全一致. 这意味着对各类异常进行统一检测时,无法准确定位最具区分度的属性字段,从而影响了综合检测效果.
进一步地,选取信息增益最高的字段,设置异常数据占比为10%,以F1分数作为综合检测指标,将离散值展开成为独热码,使用最基础的GCN进行异常检测. 随后,基于信息增益从高至低地增加使用的字段并更新检测结果. 图3展示了对应的F1分数变化趋势.
由图3可见,仅采用若干具有更高信息增益的属性字段即可达到良好的检测效果,在使用约15个字段时即可达到最优. 随着独热码带来的新字段的引入,检测效果有所降低. 这种降低即不体现异常特性的属性字段干扰综合检测的直观效果.
3. MNDetector的框架设计
为解决属性干扰对综合检测的影响,本文提出了MNDetector. 图4展示了MNDetector的框架,可分为3个主要环节:首先构建多层网络结构,随后对多层网络进行学习来获得节点的表征向量,最终使用分层的GAN实现异常检测.
3.1 基于关联的多层网络构建
利用多层网络分隔不同语义层次的属性字段可以很好地屏蔽字段间的相互影响. 为了利用多层网络实现异常访问检测,首先需要基于访问数据构建多层网络. 图5展示了多层网络构建的过程. 针对原始数据中的字段,利用关联分析获取属性字段频繁集,进而基于相关性较强的字段构建单层网络,最后添加层间关联.
3.1.1 频繁集构建
为了获取属性字段之间存在的隐含关系,通过逐层搜索的迭代方法计算数据属性中的项集关系[44]. 在此基础上,计算属性字段之间的关联规则.
具体而言,在将离散值转换为独热码并删除无效值后,计算每个字段a在全部数据中的出现概率P(a):
P(a) = \frac{{count(a)}}{{\displaystyle\sum\limits_{field \in F} {count(field)} }} \text{,} (5) 其中F为全部属性字段的集合,函数count表示字段非空的数据条目数.
将所有P(a)不为0的字段合并为候选集,在其中剔除概率过小的字段即可组成频繁项集. 将单一字段的统计频率替换成频繁项集的统计频率,通过多轮迭代即可获得全部的频繁项集. 其去重后对应的字段集即为构建每层网络的基础.
3.1.2 网络构建
在每层网络中,节点代表访问行为,节点属性代表访问行为在对应属性字段上的值. 进而利用L2范数计算边权重,基于高斯距离形成亲和矩阵,完成对单层网络的构建.
具体地,对于第l层上的节点u与节点v,基于节点属性通过式(6)计算同层节点间的边权重.
w_{uv}^{(l)} = \exp\left(\frac{{ - \left\| {{\boldsymbol h}_u^{(l)} - {\boldsymbol h}_v^{(l)}} \right\|_2^2}}{{2{\varepsilon ^2}}}\right) . (6) 在获取全部的单层网络之后,通过通用的基于条件概率的置信度添加跨层关联. 也就是,针对任意2层网络,将层间置信度作为层间关联的构建概率,从而遍历全部节点即可完成跨层边的添加.
3.2 基于跨层游走的多层网络节点表示
图6展示了多层网络的节点表示方法. 基于所构建的多层网络,采用跨层有偏随机游走的方法获取同层节点序列和跨层节点序列,利用全部的节点序列计算中心节点表示.
在每层网络中,利用邻接矩阵表示网络的结构信息,当节点u与节点v之间存在边时,基于式(7)计算从u到v的游走概率.
P(v|u) = \frac{{{\alpha _{pq}}{w_{uv}}}}{c} \text{,} (7) 其中c为归一化常数. 参数αpq由节点关系以及参数p和q决定,若节点处于同一层且属性完全一致,则取其为p的倒数;若节点处于同一层且互为邻居,则取其为1;若节点处于不同层且由跨层边相连,则取其为q的倒数.
显然,参数p和q可调整随机游走的偏向性. 当p较小时,游走倾向于在同一层上进行,中心节点表示中包含了更多的同层结构信息;当q较小时,随机游走倾向于在不同层上进行,中心节点表示中包含了更多的跨层结构信息. 不妨令u为游走路径的中心节点,可利用式(8)基于获取到的全部路径计算中心节点的表示.
{{\boldsymbol h}_u} = \mathop {mean}\limits_{path} \left(\frac{{1 - \gamma }}{{len - 1}}\left(\displaystyle\sum\limits_{n \in {N_{path}},n \ne u} {{{\boldsymbol h}_n}} \right) + \gamma {{\boldsymbol h}_{u{\text{,raw}}}}\right) \text{,} (8) 其中,hu,raw表示节点u的原始属性,path表示游走路径,len表示路径长度,Npath表示路径中的节点集合,\gamma 表示中心节点权重.
由于网络层次划分的依据是属性字段集的关联,因此相较于同层路径,处理跨层路径时应以更低的权重引入跨层信息.
3.3 基于分层GAN的异常检测
多层网络具有分层结构,因此需针对每层网络分别设置GAN,利用不同层次对应的属性进行训练.
图7展示了具体的检测方法. 在训练良好的生成器与判别器后,即可使用生成器获取未知节点的重构损失,使用判别器获取未知节点的判别结果,将生成器和判别器二者融合获得层次化的检测结果,最终将各层检测结果融合成为综合检测结果.
具体地,利用层内的节点进行训练以获得适应不同层数据分布的生成器与判别器,每个单独的GAN的总体损失为
loss={E}_{{\boldsymbol{x}}\sim {P}_{\text{data}}(\boldsymbol x)}(\mathrm{lb}D(\boldsymbol x))+ {E}_{\boldsymbol z\sim {P}_{\text{noise}}(\boldsymbol z)}(\mathrm{lb}(1-D(G(\boldsymbol z))))\text{,} (9) 其中G代表生成器,D代表判别器,x代表输入数据向量,z代表噪声向量,Pdata(x)代表数据自身的分布,{P}_{\text{noise}}(\boldsymbol z) 代表噪声分布.
在各层训练结束后,首先将待测节点的表征向量h作为判别器的输入,得到判别器的判别结果ResD. 同时将h作为生成器的输入,得到生成器的生成结果hG,将h和hG之间的欧氏距离作为生成器的重构损失. 由于不同层的属性数量和属性值有所差异,不同层上节点的重构损失数值无法直接进行比较. 因此需将重构损失归一化,记为ResG,进而利用式(10)计算最终的异常检测结果Res.
Res = \beta \times Re{s_D} + (1 - \beta ) Re{s_G} \text{,} (10) 其中参数β可控制对结构信息或属性信息的侧重程度.
在一些层次的网络中,部分数据样本并未体现出有效差异,即其在对应的属性字段上的值几乎完全一致,这导致图中存在近乎全连接的庞大子图. 这种情况意味着本层网络并未体现出异常区分度,因此相关层次检测结果不被用于最终检测结果的融合.
3.4 复杂度分析
MNDetector将传统单层图扩展为多层网络,相较于常规的图异常检测方法,其时间、空间开销均有所上升.
记N为单层网络节点数目,E为未形成近乎全连接图的层次中最大的边数目,m为网络层数,len为游走路径长度. 游走与嵌入阶段的时间复杂度可估算为O(len×mN)=m×O(len×N),即单层方法的m倍. 由于各层字段的并集即为全部字段,空间复杂度的上升仅体现为更多路径的储存消耗,从而同样为单层检测方法的m倍. 在检测阶段,针对单层网络构建的GAN的时空开销与单层图方法无异,而空间复杂度来源于GAN的储存需求,二者均为单层方法的m倍.
综上所述,MNDetector相较于常规的检测方法,其时间、空间复杂度均有所提高,其扩大倍数为多层网络层数. 考虑到具体场景中所构建的多层网络往往低于10层,因此二者没有数量级上的显著差异.
4. 实验结果与分析
4.1 实验设置
4.1.1 数据集
采用了4个公开数据集进行实验.
1)KDD[45](KDD CUP 99). 该数据集模拟了完整的局域网系统,采用不同的攻击方式对虚拟系统进行攻击,汇总了网络连接流量数据及其特征.
2)NSL[45](NSL-KDD). 该数据集在KDD CUP 99数据集的基础上进行精简,更简要地描述了网络环境.
3)UNSW[43](UNSW-NB15). 该数据集通过模拟网络攻击并对网络数据包进行捕获,经过筛选后组成了包含9种攻击类型的网络访问记录.
4)TOR[46](ISCXTor2016). 该数据集包括描述Tor(the onion router)网络连接的各方面特征,如连接建立、数据传输等,常用于研究和分析匿名网络.
表1展示了上述数据集的详细参数.
表 1 数据集参数Table 1. Parameters of Datasets数据集 特征数 异常类别数 KDD 41 39 NSL 42 39 UNSW 49 9 TOR 29 1 4.1.2 基线方法
采用了6种基线方法.
1)OC-SVM[47]. 传统异常检测方法的代表,其基本思想是构建最优分类超平面,从而划分正常节点与异常节点. 该方法的检测效果可以作为任务难易程度的判断依据.
2)DAGMM[48]. 基于自编码器的异常检测方法的代表,其首先通过自编码器压缩网络,获取数据表示结果并输入估计网络,得到最终的检测结果.
3)AnoGAN[49]. 基于GAN的传统异常检测方法的代表,其学习正样本的潜在分布模式,依据判别结果进行反向传播优化,将判别器的输出作为异常值.
4)BiGAN[50]. 基于GAN的图异常检测方法的代表. 其学习额外的编码器,在最终异常检测的同时将生成器和编码器的输出作为判别器的输入,以此来获得更加准确的检测结果.
5)AnomMAN[16]. 基于多视角图的异常检测方法的代表,是当前针对层次化图结构进行检测的最优方法. 其针对不同层次的图分别进行属性矩阵与邻接矩阵的嵌入,进而计算各节点的异常分数.
6)AnomalyDAE[42]. 基于图自编码器的异常节点检测方法的代表. 其分别针对属性矩阵与邻接矩阵进行编码与解码,融合重构损失以实现异常检测.
OC-SVM作为传统方法,参数量显著低于MNDetector和其余的基线方法. 此外,由于嵌入、检测模型的参数往往与输入属性维度呈正比,因此多层网络结构的引入不会改变参数量的数量级. 在多层网络检测所独有的结果融合阶段不需要学习,仅需要引入若干超参数,不会影响模型总体参数量. 因此,除OC-SVM外的基线方法的参数量与MNDetector的参数量保持了一致的数量级.
4.1.3 参数设置
由于原始数据中异常数据占比较高,为模拟真实的异常检测应用场景,本文对原始数据进行采样,使得数据中异常数据占比为5%.
记单个GAN对应的属性空间维度为dim,MNDetector所使用的生成器由dim×512的全连接层、ReLU激活层以及512×dim的全连接层组成. 其对应的判别器由4层神经网络组成,分别为dim×512的全连接层、ReLU激活层、512×1的全连接层以及sigmoid激活层,全局训练轮次为10 000. 在计算边权重时ε=0.1以降低距离较远的节点之间的影响,式(7)中p=1,q=0.8,以促使模型更多地获取跨层信息. 为处理同层、跨层路径信息重要性不同的问题,对于式(8)中的参数,针对同层路径,\gamma =0.5;针对跨层路径,\gamma =0.8. 由于跨层随机游走涉及多个网络层,采用的属性字段为跨层路径中心节点所在层的字段. 对式(10)中的参数,β=0.5,以平衡结构信息和属性信息.
4.1.4 评价指标
采用准确率(accuracy)、精确率(precision)、召回率(recall)、F1分数(F1_score)对实验结果的性能进行评价. 记检测结果真阳性数为TP、假阳性数为FP、真阴性数为TN、假阴性数为FN,从而
accuracy = \frac{{TP + TN}}{{TP + TN + FP + FN}} \text{,} (11) precision = \frac{{TP}}{{TP + FP}} \text{,} (12) recall = \frac{{TP}}{{TP + FN}} \text{,} (13) F1\_score = \frac{{2 \times precision \times recall}}{{precision + recall}} . (14) 4.2 综合检测
在4个数据集上对MNDetector与基线方法的检测效果进行对比,表2展示了相应的综合检测结果.
表 2 各数据集上的综合检测结果Table 2. Comprehensive Detection Results on Various Datasets模型 KDD NSL 准确率 召回率 精确率 F1分数 准确率 召回率 精确率 F1分数 OC-SVM[47] 0.978 1 0.770 4 0.787 9 0.779 1 0.979 6 0.763 0 0.817 5 0.789 3 DAGMM[48] 0.987 0 0.881 5 0.862 3 0.871 8 0.990 4 0.933 3 0.881 1 0.906 4 AnoGAN[49] 0.994 4 0.940 7 0.947 8 0.944 2 0.994 4 0.937 0 0.951 1 0.944 0 BiGAN[50] 0.994 0 0.922 2 0.957 0 0.939 3 0.992 2 0.909 6 0.932 4 0.920 9 AnomMAN[16] 0.995 9 0.954 1 0.964 4 0.959 2 0.995 6 0.951 9 0.959 0 0.955 4 AnomalyDAE[42] 0.993 0 0.964 1 0.902 9 0.932 5 0.996 2 0.977 8 0.948 5 0.962 9 MNDetector(本文) 0.998 0 0.979 3 0.980 2 0.979 7 0.998 1 0.981 7 0.980 8 0.981 2 模型 TOR UNSW 准确率 召回率 精确率 F1分数 准确率 召回率 精确率 F1分数 OC-SVM[47] 0.978 5 0.770 4 0.793 9 0.782 0 0.970 8 0.658 3 0.731 5 0.693 0 DAGMM[48] 0.989 1 0.888 9 0.892 9 0.890 9 0.990 6 0.920 8 0.894 7 0.907 6 AnoGAN[49] 0.989 1 0.874 1 0.905 6 0.889 6 0.993 8 0.945 4 0.931 1 0.938 2 BiGAN[50] 0.993 9 0.931 1 0.945 5 0.938 2 0.992 9 0.945 8 0.915 3 0.930 3 AnomMAN[16] 0.996 2 0.954 4 0.969 9 0.962 1 0.996 4 0.953 3 0.974 4 0.963 7 AnomalyDAE[42] 0.996 1 0.963 0 0.959 4 0.961 2 0.990 8 0.966 7 0.865 7 0.913 4 MNDetector(本文) 0.997 5 0.974 8 0.975 5 0.975 1 0.996 8 0.962 5 0.973 9 0.968 2 注:黑体数值表示对应指标下的最优结果. 4.2.1 KDD,NSL,TOR的检测结果
在KDD,NSL与TOR数据集上,MNDetector在全部指标上都超过了基线方法,相较于基线方法的平均效果,MNDetector实现了约8个百分点的提升.
为了进一步分析MNDetector的有效性,在KDD数据集中选取了表3所示的2个样本进行案例研究. 该数据集被构建为4层的网络.
表 3 KDD 数据集中所选取样本的信息Table 3. Information of the Selected Samples in KDD Dataset属性字段或信息 样本1 样本2 第1层网络上的属性 0,tcp,http,SF,181, 5450 ,0,0,00,tcp,private,REJ,
0,0,0,0,0第2层网络上的属性 0,0,1,0,0,0,0,0,0,0,0,0,0 0,0,0,0,0,0,0,0,0,0,0,0,0 第3层网络上的属性 8,8,0.00,0.00,0.00,
0.00,1.00,0.00,0.00255,1,0.00,0.00,1.00,
1.00,0.00,0.53,0.00第4层网络上的属性 9,9,1.00,0.00,0.11,0.00,
0.00,0.00,0.00,0.00,0.00255,1,0.00,0.53,1.00,
0.00,0.00,0.00,1.00,1.00样本标签 正常 异常 MNDetector检测结果 正常 异常 各基线方法检测结果 正常 正常 样本1和样本2在第2层上的属性高度相似,而在第3层与第4层上的属性仅有少数字段存在差异,仅在第1层上差异较为显著. 这说明样本2只在第1层上显著地体现出异常特性,在其他属性字段的层面上与正常样本相似. 而各基线方法需汇总全部属性字段,使得样本2中不体现异常特性的字段干扰了检测结果,导致其被错误地识别为正常样本.
相应地,对于MNDetector,尽管在第2层上未能成功将样本2识别为异常,但由于样本2在其他层次上体现出了显著的异常特性,因此得到的最终检测结果认定样本2为异常数据.
可以看出,基于多层网络的异常检测本质上是将原始数据按照不同的属性层次进行划分,弱化不同字段之间的关联,消除异常属性中表现正常的部分对总体检测结果的影响,从而解决属性干扰问题.
4.2.2 UNSW的检测结果
从表2可以看出,在UNSW数据集上,MNDetector的召回率和精确率略低于AnomalyDAE和AnomMAN,但准确率和F1分数更高,因此在综合评价上MNDetector优于所有基线方法.
MNDetector与基线方法的检测效果差异较小的原因可能是UNSW数据集中的异常特性在各属性字段上的分布较为均匀,即异常数据在各属性字段层次上没有明显差异. 这使得MNDetector无法将异常特性不显著的属性字段排除在检测过程之外,且并未成功分割出异常特性最集中的字段,使得精确率与召回率偏低.
异常数据在UNSW数据集上的分布规律在4.3节所介绍的分层检测结果中也有体现.
4.3 分层检测
4.3.1 数据集分层结果
表4展示了所构建的多层网络中各层网络对应的属性字段数. 由于离散属性字段被转换为独热码,因此各层字段数之和超过了原始属性字段数量.
表 4 多层网络各层属性字段数Table 4. Number of Attribute Fields per Layer in Multiplex Networks数据集 第1层 第2层 第3层 第4层 第5层 第6层 KDD 22 11 9 10 NSL 22 11 9 10 UNSW 131 31 5 5 18 TOR 7 4 4 4 4 1 4.3.2 分层检测结果
表5展示了MNDetector在各数据集、各层次上的检测结果.
表 5 各数据集上的分层检测结果Table 5. Layer-Wise Detection Results on Various Datasets网络层次 KDD NSL 准确率 召回率 精确率 F1分数 准确率 召回率 精确率 F1分数 第1层 0.995 9 0.948 1 0.969 7 0.958 8 0.995 8 0.941 5 0.973 9 0.957 4 第2层 0.950 4 0.007 4 1.00 0 0.014 7 0.950 7 0.014 8 1.00 0 0.029 2 第3层 0.995 6 0.964 4 0.949 0 0.956 6 0.995 1 0.963 7 0.940 7 0.952 1 第4层 0.996 5 0.954 1 0.976 3 0.965 1 0.996 7 0.956 3 0.976 6 0.966 3 综合检测 0.998 0 0.979 3 0.980 2 0.979 7 0.998 1 0.981 7 0.980 8 0.981 2 网络层次 TOR UNSW 准确率 召回率 精确率 F1分数 准确率 召回率 精确率 F1分数 第1层 0.995 2 0.948 1 0.955 2 0.951 6 0.996 1 0.941 7 0.979 2 0.960 1 第2层 0.996 3 0.958 5 0.966 4 0.962 4 0.992 5 0.883 3 0.963 6 0.921 7 第3层 0.962 4 0.351 9 0.772 4 0.483 5 0.991 3 0.925 0 0.902 4 0.913 6 第4层 0.950 6 0.011 9 1.00 0 0.023 5 0.994 3 0.939 2 0.945 5 0.942 3 第5层 0.951 9 0.045 2 0.859 2 0.085 9 0.993 2 0.933 3 0.930 2 0.931 7 第6层 0.993 7 0.966 7 0.912 6 0.938 9 综合检测 0.997 5 0.974 8 0.975 5 0.975 1 0.996 8 0.962 5 0.973 9 0.968 2 注:黑体数值表示对应指标下的最优检测结果. 除了在UNSW数据集上的检测外,MNDetector在其他数据集上的综合效果均为最优. 这说明相比于仅针对单一层次进行检测,将全部层次进行综合带来了更多的信息,有助于获得更优的检测结果. 此外,虽然模型各层检测效果不及总体效果,但在部分层次上依旧相对准确,这说明异常性质显著的属性字段已经提供了足够多的信息,能够支撑相对准确的检测.
与表2的检测结果相似,在UNSW数据集上,模型总体检测效果并不完全优于各层检测效果. 这验证了其异常特性在各属性字段上表现较为平均,不在某一层次上显著突出. 在进行细粒度划分时,模型在各层上的表现相差不大,导致综合检测并不完全优于分层检测.
此外,可以看出KDD和NSL数据集对应的第2层,以及TOR数据集对应的第3~5层上的检测结果极差,而UNSW数据集上却没有这种现象. 为对此进行进一步分析,需考察所构建的多层网络的具体结构. 表6展示了各层网络包含的边数目.
表 6 各层次网络中边的数目Table 6. Number of Edges in Each Layer of Network数据集 第1层 第2层 第3层 第4层 第5层 第6层 KDD 6 855 455 326 15 076 46 097 NSL 6 770 466 692 15 765 40 997 UNSW 15 154 9 893 15 225 17 965 10 296 TOR 14 231 76 892 263 183 468 028 463 203 52 700 注:黑体数值表示对应层次下显著偏大的边数目. 结合分层语义以及表6可以看出,上述层次相关的属性字段包含是否登录成功、是否为超级用户等信息. 这些字段与对于单一的访问行为而言属于基础性信息,无法体现访问目的,不具有异常区分度. 因此,在这些层次上边的数目远大于其他层次,形成了近乎全连接的图. 这意味着全部访问在相关属性字段上的值几乎一致,在这些层次上难以学习到异常属性分布,导致检测精确率数值为1但综合效果极差. 而在综合检测中,此类层次的结果被屏蔽,从而杜绝了不体现异常特性的属性字段对检测造成的干扰.
表6同样展示出,UNSW数据集所构建的多层网络中不存在近似全连接的层次,即多层网络结构并未将干扰检测的属性字段排除,这也是其综合检测结果相较于基线方法提升不高的原因.
4.4 消融实验
以F1分数作为性能评价指标,选取KDD和TOR数据集分别作为入侵检测和匿名流量检测的代表进行消融实验. 表7展示了消融实验的结果.
表 7 消融实验的F1分数Table 7. F1 Scores of Ablation Experiments实验设置 数据集 KDD TOR 不采用重构损失 0.950 1 0.949 5 不采用判别结果 0.951 3 0.940 2 不采用同层路径 0.878 4 0.796 3 不采用跨层路径 0.928 8 0.948 0 完整的MNDetector 0.982 1 0.973 9 注:黑体数值表示对应数据集下的最优检测结果. 由表7不难看出,从节点嵌入的角度而言,综合同层与跨层路径能够有效提升检测效果;从结果融合的角度而言,综合利用生成器和判别器的检测效果优于单独使用的效果. 不同数据集上仅采用生成器或判别器的检测效果互有优劣,这可能是由于异常样本同时在结构信息和属性信息上体现出异常,而这二者分别是生成器和判别器的侧重点.
当仅采用层内路径进行检测时,多层网络结构退化为失去跨层关联的分层网络,引起了检测效果的降低. 而当仅采用跨层路径时,模型对同一层次内节点关联的挖掘严重不足,引起了最大程度的效果降低.
5. 结 论
当前频繁出现的网络安全威胁的核心问题是异常访问. 访问数据的属性包含反映不同方面特性的字段,然而只有部分字段体现出显著的异常特性. 现有检测方法通常采用全部属性字段进行统一检测,引入了区分度较弱的字段,造成属性干扰问题,影响检测效果. 为解决这一问题,将多层网络结构引入了异常访问检测领域,提出基于多层网络的异常访问检测方法MNDetector. 利用相关性紧密的属性字段构建单层网络,在此基础上添加层间关联,形成多层网络结构. 随后基于跨层游走获取同层和跨层节点序列,实现节点表示. 最后在不同层次上分别训练GAN,结合重构损失与判别结果共同实现异常检测.
实验验证了MNDetector在多个公开数据集上的检测效果超过当前的最优方法. 同时,分层检测结果验证了MNDetector能够有效融合各层检测结果,并能够排除不显著体现异常特性的属性字段的干扰. 此外,消融实验结果证实了MNDetector所采用的检测机制的有效性. 为深入探究其获得更佳检测效果的原因,本文还进行了案例研究,通过分析实验结果,详细说明了MNDetector的有效性和检测优势.
未来的研究计划从以下3个方面展开:
1)相比于单层结构,多层网络结构具有更高的复杂度,能够挖掘更多的深层关联. 拟引入互信息等度量方式,探索更复杂的多层网络异常检测方法.
2)多层网络结构能拆分数据集属性字段的语义层次. 拟对现有异常访问行为检测的公开数据集进行语义分析,结合具体场景增进对各属性字段的理解,并进一步对数据集进行优化与整合.
3)基于多层网络异常检测的有效性,拟结合异常访问行为的具体特征,分析异常特性显著或不显著的属性字段的语义含义,为进一步的检测提供指导.
作者贡献声明:袁子淇提出论文总体思路并撰写论文;孙庆赟对研究思路及论文进行调整与优化;周号益对研究方法提出具体建议;朱祖坤完成实验验证并撰写论文;李建欣总体把控研究方向并提供指导性建议与工作支持.
-
表 1 数组的基本操作函数
Table 1 Basic Operation Functions of Array
函数 功能 符号表示 mkvSeq 构造数组/张量 ⊞ let_binding 中间变量值绑定 tlet x := e in y idx 根据下标索引访问数组
第i个元素a |[ i ] max 求数组元素最大值 - sum 求数组元素的和 ∑ 表 2 数值型的基本操作函数
Table 2 Basic Operation Functions of Numerical Type
函数 功能 zero,one 分别代表实数R0,R1 negate 数值型元素取反的操作 add/sub/mul/div 2个数值型元素的加/减/乘/除操作 scal 实数与数值型元素的乘积操作 div_n 数值型元素除以自然数的操作 pow/log/pExp 数值型元素的幂次方/对数/指数操作 sqrt 数值型元素的平方根操作 leExp/gtExp 2个数值型元素的小于等于/大于关系 表 3 函数式神经网络算子表达式
Table 3 Functional Neural Network Operator Expression
分类 函数 功能
元素操作ReLU1d/ReLU2d/
ReLU3d/ReLU4d对不同维度的张量元素取激活函数ReLU Softmax1d/Softmax2d/
Softmax3d/ Softmax4d对不同维度的张量元素取激活函数Softmax Tanh2d/Tanh4d 对不同维度的张量元素取激活函数Tanh Tadd2d/Tadd4d 对相同维度张量元素相加 Tmul2d/Tmul4d 对相同维度张量元素相乘 复合操作 Conv2d/Conv4d 不同维度张量的卷积操作 Avgpool2d/Avgpool3d/
Avgpool4d不同维度张量的平均池化操作 Maxpool2d/Maxpool3d/Maxpool4d 不同维度张量的最大池化操作 Linear/Linear2d 不同维度张量全连接操作 NLLLoss2d 损失函数NLLLoss ConvTranspose2d/
ConvTranspose4d反卷积操作,扩大张量尺寸 重塑操作 Flatten3d/Flatten4d 平铺操作 Truncl1d/Truncl2d 向左/右截断张量k个元素 Padl/Padr 向左/向右填充k个元素 Concat 连接2个张量 表 4 带类型的神经网络模型
Table 4 Typed Neural Network Model
分类 模型 介绍
CNNLeNet 一个经典神经网络模型,由2个卷积层和
3个全连接层组成AlexNet 一种经典的深度CNN模型,由5个卷积层和
3个全连接层组成ResNet-34 一种经典的残差CNN模型 GoogLeNet 一种网中网的深度CNN模型,引入了
Inception模块VGG-16 深度CNN模型,适用于迁移学习 DenseNet-121 一种稠密CNN模型,引入了DenseBlock块与
前面所有层连接GM DCGAN 一种深度卷积生成对抗网络 VAE 一种深度生成模型,由1个编码器和
1个解码器组成RNN LSTM 一种特殊的递归神经网络,引入了3个门和1个细胞状态以处理序列中的长期依赖关系 表 5 形状错误检测结果
Table 5 Shape Error Detection Results
表 6 中间命令式组合子
Table 6 Intermediate Imperative Combinators
函数 具体实现 mkvSeql Definition mkvSeql {n:nat} {d:data} (f:fin n -> acc d -> comm) (out:acc(ary n d)) := for (fun i:fin n => f i out|{i}). mkvParl Definition mkvParl {n:nat} {d:data} (f:fin n -> acc d -> comm) (out:acc(ary n d)):= parfor out (fun i o => f i o). letl Definition letl{s t}(e:exp s)(f:exp s -> acc t -> comm)(out:acc t) := f e out. maxl Definition maxl {n:nat} (xs:exp (ary n num)) (f:exp num -> acc num -> comm) (c : exp num -> comm) := new (fun tmp => let (w,v) := tmp in (w |:= xs |[0]) ; (for (fun i => If (gtExp xs|[i] v) (f xs|[i] w, f v w)) ; c v)). suml Definition suml {n:nat} (xs : exp (ary n num)) (f:exp num -> acc num -> comm) (c : exp num -> comm) := new (fun tmp => let (w,v) := tmp in (w |:= zero) ; (for (fun i => f (add xs|[i] v) w)) ; c v). 表 7 测试结果
Table 7 Test Results
算子操作 张量规模 顺序执行时长/s 并行执行时长/s 加速比 生成代码 手工编写 生成代码 手工编写 生成代码 手工编写 Conv2d (p, s = 1) 700×700
300×3005.910 935 6.978 041 0.720 788 0.823 746 8.20 8.47 Avgpool2d (k = 2) 8 000×8 000 0.130 755 0.142 020 0.016 803 0.059 553 7.78 2.38 Maxpool2d (k = 2) 8 000×8 000 0.141 180 0.065 849 0.022 787 0.047 422 6.20 1.39 ReLU2d 8 000×8 000 0.081 935 0.082 872 0.022 103 0.023 369 3.71 3.55 Linear2d 2 000×3 000 3 000×4 000 13.760 259 13.848 600 1.355 773 1.418 254 10.15 9.76 -
[1] Paszke A, Gross S, Massa F, et al. Pytorch: An imperative style, high-performance deep learning library[J]. Advances in Neural Information Processing Systems, 2019, 32: 8024−8035
[2] Abadi M, Agarwal A, Barham P, et al. Tensorflow: Large-scale machine learning on heterogeneous distributed systems[J]. arXiv preprint, arXiv: 1603.04467, 2016
[3] Jia Yangqing, Shelhamer E, Donahue J, et al. Caffe: Convolutional architecture for fast feature embedding[C]//Proc of the 22nd ACM Int Conf on Multimedia. New York: ACM, 2014: 675−678
[4] Gulli A, Pal S. Deep Learning with Keras[M]. Birmingham: Packt Publishing Ltd, 2017
[5] Wu Dangwei, Shen Beijun, Chen Yuting. An empirical study on tensor shape faults in deep learning systems[J]. arXiv preprint, arXiv: 2106.02887, 2021
[6] Jhoo H Y, Kim S, Song W, et al. A static analyzer for detecting tensor shape errors in deep neural network training code[C]//Proc of the 44th ACM/IEEE Int Conf on Software Engineering. New York: ACM, 2022: 337−338
[7] Lagouvardos S, Dolby J, Grech N, et al. Static analysis of shape in TensorFlow programs[C/OL]//Proc of the 34th European Conf on Object-Oriented Programming (ECOOP 2020). Dagstuhl, Germany: Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2020[2024-03-10]. https://drops.dagstuhl.de/storage/00lipics/lipics-vol166-ecoop2020/LIPIcs.ECOOP.2020.15/LIPIcs.ECOOP.2020.15.pdf
[8] Dolby J, Shinnar A, Allain A, et al. Ariadne: Analysis for machine learning programs[C/OL]//Proc of the 2nd ACM SIGPLAN Int Workshop on Machine Learning and Programming Languages. New York: ACM, 2018[2024-03-10]. https://arxiv.org/pdf/1805.04058
[9] Hattori M, Sawada S, Hamaji S, et al. Semi-static type, shape, and symbolic shape inference for dynamic computation graphs[C]//Proc of the 4th ACM SIGPLAN Int Workshop on Machine Learning and Programming Languages. New York: ACM, 2020: 11−19
[10] 纪泽宇,张兴军,付哲,等. 分布式深度学习框架下基于性能感知的DBS-SGD算法[J]. 计算机研究与发展,2019,56(11):2396−2409 doi: 10.7544/issn1000-1239.2019.20180880 Ji Zeyu, Zhang Xingjun, Fu Zhe, et al. Performance-Aware based dynamic batch size SGD for distributed deep learning framework[J]. Journal of Computer Research and Development, 2019, 56(11): 2396−2409 (in Chinese) doi: 10.7544/issn1000-1239.2019.20180880
[11] Zhao Tian, Huang Xiaobing, Cao Yu. Deepdsl: A compilation-based domain-specific language for deep learning[J]. arXiv preprint, arXiv: 1701.02284, 2017
[12] Wang Liang, Zhao Jianxin. Architecture of Advanced Numerical Analysis Systems: Designing a Scientific Computing System Using OCaml[M]. Berlin: Springer, 2023
[13] INRIA. The coq proof assistant[EB/OL]. 1997[2022-09-15]. https://coq.inria.fr/
[14] Steuwer M, Fensch C, Lindley S, et al. Generating performance portable code using rewrite rules: From high-level functional expressions to high-performance OpenCL code[J]. ACM SIGPLAN Notices, 2015, 50(9): 205−217 doi: 10.1145/2858949.2784754
[15] Atkey R, Steuwer M, Lindley S, et al. Strategy preserving compilation for parallel functional code[J]. arXiv preprint, arXiv: 1710.08332, 2017
[16] 麻莹莹,陈钢. 基于Coq的矩阵代码生成技术[J]. 软件学报,2022,33(6):2224−2245 Ma Yingying, Chen Gang. Matrix code generation technology based on Coq[J]. Journal of Software, 2022, 33(6): 2224−2245 (in Chinese)
[17] Verma S, Su Zhendong. Shapeflow: Dynamic shape interpreter for tensorflow[J]. arXiv preprint, arXiv: 2011.13452, 2020
[18] Huang A, Hashimoto J, Paszke A, et al. Hasktorch[EB/OL]. 2019[2024-04-13]. https://github.com/hasktorch/hasktorch
[19] Paszke A, Gross S, Chintala S, et al. Automatic differentiation in pytorch[J/OL]. 2017[2024-05-15]. https://api.semanticscholar.org/CorpusID:40027675
[20] Thompson S. Haskell: The Craft of Functional Programming[M]. Boston: Addison-Wesley, 2011
[21] Roesch J, Lyubomirsky S, Weber L, et al. Relay: A new ir for machine learning frameworks[C]//Proc of the 2nd ACM SIGPLAN Int Workshop on Machine Learning and Programming Languages. New York: ACM, 2018: 58−68
[22] Roesch J, Lyubomirsky S, Kirisame M, et al. Relay: A high-level compiler for deep learning[J]. arXiv preprint, arXiv: 1904.08368, 2019
[23] Hattori M, Kobayashi N, Sato R. Gradual tensor shape checking[C]//Proc of the 32nd European Symp on Programming. Berlin: Springer, 2023: 197−224
[24] Eremondi J, Tanter É, Garcia R. Approximate normalization for gradual dependent types[J]. Proceedings of the ACM on Programming Languages, 2019, 3(88): 1−30
[25] Lehmann N, Tanter É. Gradual refinement types[J]. ACM SIGPLAN Notices, 2017, 52(1): 775−788 doi: 10.1145/3093333.3009856
[26] Vazou N, Tanter É, Van Horn D. Gradual liquid type inference[J]. Proceedings of the ACM on Programming Languages, 2018, 2(132): 1−25
[27] Liu A, Bernstein G L, Chlipala A, et al. Verified tensor-program optimization via high-level scheduling rewrites[J]. Proceedings of the ACM on Programming Languages, 2022, 6(55): 1−28
[28] Ragan-Kelley J, Barnes C, Adams A, et al. Halide: A language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines[J]. ACM SIGPLAN Notices, 2013, 48(6): 519−530 doi: 10.1145/2499370.2462176
[29] Danvy O, Millikin K, Nielsen L R. On one-pass CPS transformations[J]. Journal of Functional Programming, 2007, 17(6): 793−812 doi: 10.1017/S0956796807006387
[30] 马振威,陈钢. 基于Coq记录的矩阵形式化方法[J]. 计算机科学,2019,46(7):139−145 doi: 10.11896/j.issn.1002-137X.2019.07.022 Ma Zhenwei, Chen Gang. Matrix formalization based on Coq record[J]. Computer Science, 2019, 46(7): 139−145 (in Chinese) doi: 10.11896/j.issn.1002-137X.2019.07.022
[31] 麻莹莹,马振威,陈钢. 基于Coq的分块矩阵运算的形式化[J]. 软件学报,2021,32(6):1882−1909 Ma Yingying, Ma Zhenwei, Chen Gang. Formalization of block matrix operations based on Coq[J]. Journal of Software, 2021, 32(6): 1882−1909 (in Chinese)
[32] Shi Zhengpu, Xie Guojun, Chen Gang. CoqMatrix: Formal matrix library with multiple models in Coq[J]. Journal of Systems Architecture, 2023, 143: 102986 doi: 10.1016/j.sysarc.2023.102986
[33] Mahboubi A, Tassi E. Mathematical components[EB/OL]. 2021[2024-05-15]. https://math-comp.github.io/
[34] Boldo S, Lelay C, Melquiond G. Coquelicot: A user-friendly library of real analysis for Coq[J]. Mathematics in Computer Science, 2015, 9: 41−62 doi: 10.1007/s11786-014-0181-1
[35] LeCun Y, Bottou L, Bengio Y, et al. Gradient-based learning applied to document recognition[J]. Proceedings of the IEEE, 1998, 86(11): 2278−2324 doi: 10.1109/5.726791
[36] Tai Cheng, Xiao Tong, Zhang Yi, et al. Convolutional neural networks with low-rank regularization[J]. arXiv preprint, arXiv: 1511.06067, 2015
[37] He Kaiming, Zhang Xiangyu, Ren Shaoqing, et al. Deep residual learning for image recognition[C]//Proc of the 29th IEEE Conf on Computer Vision and Pattern Recognition. Piscataway, NJ: IEEE, 2016: 770−778
[38] Simonyan K, Zisserman A. Very deep convolutional networks for large-scale image recognition[J]. arXiv preprint, arXiv: 1409.1556, 2014
[39] DiPietro R, Hager G D. Deep learning: RNNs and LSTM[M]//Handbook of Medical Image Computing and Computer Assisted Intervention. San Diego: Elsevier, 2020: 503−519
[40] McCann B. github[EB/OL]. [2023-09-05]. https://github.com/pytorch/examples
[41] Spolsky J. stackoverflow [EB/OL]. [2024-02-22]. https://stackoverflow.com/questions