递归神经网络的Monte Carlo验证

版权归作者所有。递归神经网络的性质及其Monte Carlo验证Dmitry Vengertsev1，Elena Sherman11博伊西州立大学计算机科学系1910UniversityDrive，Boise，Idaho 83725网址：dmitryvengertsev@u.boisestate.edu，elenasherman@boisestate.edu摘要随着RNN在医疗和汽车领域的应用，它们成为关键系统的一部分，传统上需要彻底的验证过程。在这项工作中，我们提出了如何将RNN行为建模为标记的转换系统，并正式定义了一组状态和时间的安全属性，这样的模型。为了验证这些属性，我们建议使用蒙特卡罗方法，并评估其有效性不同类型的属性。我们对两个RNN模型进行了我们的实验表明，我们的模型满足更好的状态属性比时间属性。此外，我们还证明了Monte Carlo抽样对于状态属性验证是非常有效的，这通常需要探索RNN模型的一小部分。然而，为了验证时间特性，蒙特卡罗需要分析多达20%的计算。1引言递归神经网络（RNN）已成为许多普遍应用的核心组件，例如车辆轨迹估计（Kim et al. 2017），语音识别（Graves，Mohamed和Hinton 2013），机器翻译以及许多其他计算依赖于先前处理的输入序列的应用。随着这些领域的成熟，现在RNN在关键应用中变 得 更 加 普 遍 ， 例 如 预 测 医 疗 路 径 （ Choi et al.2016），人类行为识别（Jain et al. 2016）和医疗手术（Mayer et al. 2006）。因此，作为安全关键应用的重要组成部分，RNN应该经过验证过程以确保其安全行为。目前对机器学习模型验证的研究主要集中在前馈深度神经网络（DNN）的验证上。例如，研究通常使用SMT求解器来验证一些安全属性（Katz et al.2017; Huang et al. 2017; Pulina and Tacchella 2012; Kuperet al. 2018）。然而，DNN本质上不同于RNN，RNN被构造为处理输入序列，以便下一个从处理输入的子元素所产生的配置开始处理序列中的因此，虽然有价值，但以前关于DNN验证的工作可能不完全适用于RNN，并且没有解决RNN的所有验证场景。例如，ReluLu（Katz et al. 2017）可以使用ReLu函数的分段线性特性来正式验证神经网络的此外，在以前的工作中定义的大多数性质是由学术研究人员开发的，而不是必要的解释者，这可能会阻碍工业实践者对其的适应。在这项工作中，我们专注于定义和形式化特定于RNN的新状态和时间属性。此外，我们还正式以前定义的实用属性，适用于神经网络。特别是，我们确定和形式化的四个状态安全属性：高置信度，决策性，鲁棒性和覆盖率，这描述了理想的RNN配置。此外，我们还引入并形式化了两个时间安全属性：长期关系和记忆，它们表征了RNN配置的允许序列，我们在描述RNN如何处理输入序列的模型的上下文中定义属性我们选择将RNN行为建模为标记状态转换系统，其中状态表示处理单个符号后RNN内部节点的值因此，如果在处理输入符号之后，由第一状态描述的RNN在这项初步工作中，所提出的RNN模型没有抽象，因此它代表了RNN在所有可能的输入序列上的具体行为为了验证RNN模型的拟议属性，我们使用MonteCarlo采样，因为没有抽象，模型具有较大的状态空间，其完整验证相当于穷举测试。蒙特卡罗抽样提供了一个更广泛的适用性和可扩展的替代随机系统的属性验证使用数值和符号的方法。版权所有© 2020本文由其作者。在知识共享许可署名4.0国际（CC BY 4.0）下允许使用。联系我们不∈1−| |∈∈12蒙特卡洛模型检验技术已经被广泛应用于分析计算机网络、安全和系统生物学等领域中具有大状态空间的系统（Grosu和Smolka 2005; Donaldson和Gilbert2008; Nghiem等人，2009）2010年）。在我们的论文中，我们想通过研究实现地面真实结果所需的状态空间采样的百分比来研究蒙特卡洛采样是否是验证RNN模型的合适方法。在我们的实验中，我们通过详尽地探索RNN模型的整个状态空间来计算地面真值。我们在两个大型RNN系统上进行实验，我们将其建模为标记的转换系统。接下来，我们将确定六个属性的真实情况，并评估Monte Carlo模型检验的适用性。我们使用评估结果回答以下研究问题：用于对过程的行为进行建模，并作为各种形式化规范语言的语义模型下面我们介绍LTS的定义，然后描述我们如何使用这个转换系统来建模RNN行为标签转换系统（Tretmans 1996）是一个四-tuple（S，L，T，S0）其中：1. S是一个可数的、非空的状态2. L是可数标号3. 不S（L）τ）S是一个跃迁关系，其中L表示可观测的相互作用，以及一个用于模拟内部跃迁的特殊标签τ∈/L。4. S0是初始状态的集合。我们需要使用LTS来建模RNN，它接受-puts（x1，. . . ，Xt），并且具有隐藏状态（h1，. . . ，h，l），以及1t1. 所提出的属性是否适用于我们的RNN模型？2. 蒙特卡罗模型检测对这些模型的效率如何？3. 蒙特卡洛模型检验的效率是否结果表明，并不是所有的状态在RNN模型具有状态属性，这表明我们的RNN的弱点。此外，长期的时间属性具有更低的满足率。这意味着未来的评估应该在更复杂的RNN上进行。我们的研究结果还表明，蒙特卡罗模型检验可以非常有效地验证状态属性，但是，它需要更多的样本收敛到地面真理的时间属性。除了回答上述研究问题外，我们的工作还做出了以下贡献：它正式定义了RNN的状态和时间安全属性。• 它实现了两个RNN系统的RNN模型。采用蒙特卡洛模型检验方法对RNN模型进行了性能检验。本文的其余部分组织如下。在第2节中，我们将RNN表示为标记的转换系统。在第3节中，我们将详细描述所提出的状态和时间安全属性的形式化。在第4节中，我们简要介绍了Monte Carlo模型检验的验证所提出的表示。在第5节中，提供了实验结果第6节介绍了相关的工作，我们总结了未来的工作计划的文件。2递归神经网络网络系统过程验证的第一步是确定如何以适合验证其属性。系统的一般行为产生输出（y1，. . .，yt），其中xt是来自大小为σ=Σ，yt的训练集字母表的字符的独热编码向量σ，hl其中l是隐藏层的指示符，m是隐藏向量的维度在我们的演示中，我们使用n表示输入序列长度，R描述层数。图1：具有三层的RNN的状态表示（a）和相应的RNN表示为标记状态转换系统（b）背后的直觉示例。类似于以前的工作（杜等人。2018），LTS状态表示RNN的配置 我们使用元组（H，Y）来描述这种配置，其中H是RNN的隐藏状态向量，Y是输出。 例如，（H1，Y1）是在处理单个符号X 1 =（x 1，<$0 n − 1）之后H1=（hl，<$0n−1）l∈R和Y1=（y1，<$0n−1）的状态。 我们使用<$0n−1表示法来表示大小为n 1的零值行向量。然后，在下一个输入字符X2=（x1，x2，<$0n−2）上，模型转换到另一个状态（H2，Y2），其中H2=（hl，hl，<$0n−2）l∈R，Y=（y，y，<$0TEM被建模为状态转换系统。在这项工作中，我们2 1 2n−2）。图1显示了LTS如何对选 择 将 RNN 行 为 建 模 为 标 记 转 换 系 统 （ LTS ）（Tretmans 1996）。LTS由状态和这些状态之间的标记转换组成，其中标签标识在系统上执行的某些操作LTS形式主义是RNN在输入序列（X1，X2，X3）上的行为。形式上，RNN的LTS可以定义如下：定义2.1.RNN行为模型M=（S，L，T，S0），其中··•--•--•⊆ ××L•∈¬∧∨∀ ∈∈≥l−1lS=（H，Y）ii∈N是一组状态，定义为隐状态和对应的输出值（H，Y）i的元组，其中N是状态数。L=Xii∈N是基于输入向量Xi的有限标签集不SXS是转换，即每个转换在其上具有输入向量Xi。RNN中的转换通过隐藏向量来组织，使得在时间步长t处的输出yt变为直到t的所有输入向量的函数，{x1，. . .，Xt}。递归（h，h）→h 是-为了定义转换系统的属性，我们使用线性时态逻辑（LTL）（Pnueli 1981），它形式化了有限状态系统中行为的在有限状态系统中，LTL描述了树的一组单次计算的期望行为LTL是一个强大的形式主义，然而，在我们的工作中，我们只使用它的片段，我们提供了一个简短的解释。LTL公式具有Af的形式，其中Af是路径量词，意味着来自给定状态的所有计算路径具有属性f，并且f是LTL路径公式，被RNN系统罚款。t−1t不m×n×R只包含原子命题，并正式定义为（Clarke Jr et al. 2018年）：• S0=（H0，Y0）是初始状态H0=Y得双曲正弦值.Y0=<$σ×n，其中<$σ×n是尺寸为σ × n的零矩阵.在这样的转换系统中，我们可以定义谓词函数，它可以推理H和Y状态分量。此外，我们可以定义一个迹tr，它是一个序列状态（S0，S1，S2，. . .，Sn），其中（ Si，Si+1）∈T，Si∈（0，. . . ，n −1）。3递归神经网络的性质在形式验证中，模型的性质被定义为原子命题上的公式，原子命题是状态谓词功能协调发展的因此，在我们形式化RNN的状态和为了表达下面所需的属性，我们定义了四个状态预测：Hi，Lo，Ro和Cov。除了定义2.1，我们还使用以下符号：P′（. ）是RNN执行Y的预测的置信度的估计。通常softmax函数用于此目的，但softmax不是置信度的可靠近似值（Gal 2016），因为它倾向于提供更乐观的估计。a、b、c、d、e、r、K、zR+是用于谓词参数化的正常数，即，阈值。定义3.1.状态谓词是状态S=（H，Y）上的以下1. Hi（a）-高置信度状态谓词1. 如果p∈AP，则p是LTL路公式。2. 如果f是LTL路公式，则f，Xf，Ff和Gf是LTL路径公式。3. 如果f和g是LTL路公式，则fg和fg是LTL路公式。这里X读作G读作现在使用这四个谓词和上述逻辑作为构建块，我们可以定义状态安全属性和时间安全属性，其中前者在状态上定义，后者在迹上定义，即，RNN行为模型中的状态序列安全属性断言系统的观察行为总是保持在某个允许的有限行为集内，在该有限行为集中没有坏的事情发生。直觉上，一个性质φ是一个安全性质，如果每一次违反φ都发生在系统的有限次执行之后。在本文中，我们不仅定义了它们，而且还解释了为什么我们有动机将它们纳入这项工作。在下面的所有属性中，暗示它们是Af的形式，因此在下面的所有属性中省略了A3.1安全状态属性高度自信更多地依赖机器学习-Hi（a）： P<$（Y）≥a随着技术的发展，部分自动化复杂的决策，对高置信度预测的需求也在增长。为2. Lo（b）-低置信度状态谓词例如，在空中交通管制应用的情况Lo（b）： P<$（Y）≤b当人工智能驱动的视频系统有信心时，它可以更好地监控跑道，滑行道和登机口区域，3. Ro（r，K）-鲁棒性状态谓词Ro（r，K）：<$Yj−Yi<$$> ≤K <$r<$，其中Si，转换：（S，Xi，Si）T，（S，Xj，Sj）T，其中Xj=Xi+r，r >0 -改变的字符数，参见图24. Cov（c，z）-覆盖状态谓词Cov（c，z）：H> z暗（H）其中z是被认为是激活的神经元的阈值（整个网络的全局）对人类然而，当该系统不确定时，它将控制权转移给空中交通运营商。高置信度模型需要较少的操作员参与。为了描述这种期望的行为，我们定义了高置信度属性，以确保RNN对任何可能的输入序列提供定义3.2.高置信度属性：我们说M是高置信度，如果对于整个系统，属性Hi对所有路径全局成立，因此GHi（a）（1）是整个系统验证的公式。·--······决策性虽然高置信度属性可能不适用于所有RNN行为，但在这些情况下，RNN应该提供低置信度决策，以表明需要人工干预。研究人员发现神经网络中的softmax 层 往 往 “ 过 于 自 信 ” （ Gal 2016; Guo et al.2017）。softmax层估计的预测概率并不总是可靠地用作置信因子，识别更高置信度的偏差对于系统的安全行为至关重要我们将决定性属性定义为当给定模型不能提供高置信度输出时，对该模型提供低置信度输出的评估定义3.3.决定性属性：我们说M是决定性的，如果对于整个系统，当Hi不对所有路径全局成立时，属性Lo成立，因此G（<$Hi（a）<$Lo（b））（2）是用于验证整个系统的公式。鲁棒性以前的工作表明，简单的梯度方法可能容易受到输入的微小修改的影响，这会导致输出类的变化（Szegedy等人，2013）。尽管神经网络与鲁棒性相关的特性在文献中得到了很好的研究，但为了完整性，我们在RNN行为模型中定义了它们为了使RNN对对抗性攻击具有鲁棒性，它应该具有隐藏层的内部多样表示即可见空间r中的小扰动在潜在空间中产生鲁棒扰动，因此产生接近于非扰动响应Yi的响应Yj∈J图2。定义3.4.鲁棒性：我们说M是鲁棒的，如果对于整个系统，性质Ro（r，K）对所有路径全局成立，因此GRo（r，K）（3）是整个系统验证的公式。图2：同品种器械的稳健转换示例Ro（r，K）.覆盖神经元覆盖属性通常用于测试神经网络（Pei etal.2017; Tian et al.2018年），但修剪，霍夫曼代码，代表性精度减少和量化（Han，Mao和Dally 2015）。我们将Coverage属性定义为对给定模型的评估，以激活任何可能的输入序列上的高百分比神经元。定义3.5.覆盖属性：我们说M提供了足够的覆盖，如果对于整个系统，属性Cov（c，z）对全局所有路径都成立，因此GCov（c，z）（4）是整个系统验证的公式。3.2时间安全属性虽然状态安全属性可以用于任何NN，但时间属性对于RNN是特定的，因为它们描述了RNN动态模型的轨迹中的期望状态模式。我们将这种模式表示为状态谓词上的正则与状态安全属性类似，我们首先论证每个时态属性都有必要，然后正式定义它。基于RNN的系统的关键特性之一是能够在输入序列中捕获长期关系。一个好的RNN不仅应该对训练长度的序列有很好的预测，而且应该对更长的序列有很好的预测。这样的属性对于RNN是重要的，因为对于诸如车辆轨迹预测的应用（Kim et al.2017）基于RNN的架构用于有效地预测周围车辆的未来坐标，称为占用网格。车辆的占用网格的估计我们提出了一个长期关系性质，它是模型在较长序列上的置信度与训练序列上的置信度的比较，例如，如果模型是在长度为n的序列上训练的，则它在长度为n + ρ（n）的序列上形式上，长期性质在迹trn+ρ（n）=（S1，，Sn，Sn+1，，Sn+ρ（n））=trntrρ（n），以检查该模型是否在迹trn和相邻迹trρ（n）上提供u个置信预测模型的置信度没有显著降低，仍然提供了V置信度预测，其中|TRN|= n，|=ρ（n）.|= ρ (n).定义3.6.长期关系性质：我们说M满足长期关系性质，如果对于整个系统，性质Hi（a）在迹trn上至少保持u次，并且性质Hi（d）在所有路径的相邻迹trρ（n）上保持v：Gη（u，v，a，d）但尚未正式确定可供核查。coverage属性是一个安全属性，因为它通过激活所有神经元高覆盖率，去除η：ηn（u，a）<$ηρ（n）（v，b）ηn（u，a）：（Hi（a）（<$Hi（a））<$）uηρ（n）（v，d）：（Hi（d）（<$Hi（d）v（五）rons也是一个函数属性，这里不讨论 在我们的工作中，与神经网络的压缩有关，其中d是较长序列上的特性Hi的恒定阈值，使得d≤a。∼−Pr（tr）¬基于RNN的系统的匿名化特性在文献中主要与数据隐私问题有关特别地，对于RNN模型，当这样的模型在敏感用户数据上训练时，存在无意中记忆罕见或独特的训练数据序列的2018年）。研究了几种测试记忆特性的方法，如记忆暴露测量（Carlini等人，2018）和长期背景下梯度幅度的检查（Madsen，2019）。根据我们的表示，我们将记忆性定义为当一个模型以绝对置信度对模型中的某个子状态序列给出精确答案时的情况跟踪。4.1后验概率评估蒙特卡罗采样的思想是从独立同分布的表示模型中采样迹线tr。时尚.我们可以使用Bernoulli分布对Pr（φ）Bernoulli（ρ）进行建模，并应用采样轨迹来统计估计Bernoulli成功参数ρ。正如我们之前提到的，与传统的蒙特卡洛模型检查（Grosu和Smolka 2005）相比，我们的蒙特卡洛模拟即使在存在反例的情况下也会继续采样。因此，为了正确评估成功参数ρ，我们需要评估迹线tr上的后验概率：Pr（ρ|tr）= Pr（tr|ρ）Pr（ρ）=Pr（ttr（七）定义3.7.分解性质：我们说M满足分解性质，如果对于整个系统，性质Hi在具有非常高的阈值e = 1 π的所有路径上全局地保持，对于π> 0的小值。这个属性可以概括为以下正则表达式：ρi（1−ρ）n−triP r（ρ）Pr（tr）在到目前为止采样的迹的总数n中，我们将k表示为满足性质φ的迹tr的数量。Bernoulli分布Pr（ρ）的共轭先验是Beta分布1ρα−1（1−ρ）β−1，其中α和β是Gµ（q，e）β（α，β）Beta分布的形状参数使用Σ tri=k，我们µ：（（<$Hi（e））<$Hi（e）（<$Hi（e））<$）q（6）其中，q n是给定的可以将后验公式（7）改写为以下形式：tr+α−1n−跟踪路径然而，记忆性是不可取的，所以我们Pr（ρ|tr）= ρi（1−ρ）iPr（ρ）Beta（α+k，β+n-k）（八）正在检查RNN系统是否缺乏记忆G µ（q，e）.我们现在提出一个验证方法，用于评估这些属性。4RNN行为模型由于后验概率由具有（8）中给出的新参数的Beta分布，因此具有满足性质φ的轨迹的估计概率通过估计的平均值ρ和方差ν被给出如下：Pr（φ）=ρε ±ρνε=当被验证的系统具有大的状态空间时，k+αα+β+n.（α+k）（n-k+β）（α+n+β）2（α+n+β+1）（九）用传统的模型检查技术来验证它变得不可行。一些技术研究了各种方法来引导模型检查器通过一个大的状态空间（Henriques et al. 2012）。另一种有前途的方法是通过对状态空间进行随机采样来处理状态空间爆炸，然后应用概率理论来推理模型的整体正确性（Grosu and Smolka 2005）。在这种随机抽样方法中，使用离散事件模拟（Monte Carlo实验）重复执行模型，而不需要显式表示。路径公式在模拟生成的每条轨迹上检查φ。检查的迹线提供伯努利随机变量的采样点，如果φ保持，则该采样点为1，否则为0。该模型被多次模拟，并且如果采样发现违反属性，则报告它，否则计算模型违反属性的概率。然而，对于这项工作，我们希望我们的系统有许多路径的属性被违反。因此，传统的蒙特卡罗模型检验仅停留在第一个违反规则的轨迹上，不能给出模型的完整描述。为了估计我们的模型的属性保持的程度，我们基于后验概率评估进行采样。对于每个性质φ，我们将使用相应的估计概率ρ（n）与样本数n的收敛性来决定何时停止采样。根据我们的经验估计，我们计算出当ρ的值接近地面真值时的收敛率值。我们定义ρ-收敛如下：中国|/W|/Wi=1其中W是我们计算估计概率值之间的平均值的采样窗口。5实验评价的目标是回答以下研究问题：1. 所提出的属性是否适用于我们的RNN模型？2. 对于这些模型，Monte Carlo抽样的效率如何？3. 蒙特卡罗抽样效率是否取决于属性类型？在本节中，我们首先描述了实验设置，他们的结果和上述研究问题的答案。±不| |表1：属性满意度比率的真实值和实现相同比率值所需的Monte Carlo样本数量。财产符号Params地面真相样品ρ_n_e_rgenceM1M2M1M2M1M2高置信度决策性鲁棒性覆盖率GHi（a）G（<$Hi（a）<$Lo（b））GRo（r，K）GCov（c，z）a = 0。7b = 0。2R= 2c = 0。529.222.839.090.220.626.040.295.75，371人（0.9%）5 343人（0.9%）2 409人（0.5%）1 530人（0.2%）3 055人（0.5%）3 833人（0.6%）4，655人（0.8%）1 564人（0.3%）8.2e-055.8e-052.1e-041.0e-041.1e-041.1e-041.0e-045.1e-05长期关系没有记忆Gη（u，v，a，d）G<$µ（q，e）d = 0。65e = 0。999.798.15.099.65，459人（0.9%）104 467人（18.0%）45 487人（7.8%）8，577人（1.5%）2.5e-051.8e-071.9e-064.2e-075.1实验装置我们使用字符级语言模型作为可解释性测试，用于分析Monte Carlo模型检验的性能，以验证RNN的安全性。在不失一般性的情况下，我们考虑具有长短期记忆（ LSTM ） 单 元 的 RNN （ Hochreiter 和 Schmidhuber1997）。在实验中，我们使用了下一个字符预测模型字符-RNN。当应用于字符序列时，字符RNN预测该序列中的下一个字符。我们评估了两个RNN系统M1和M2的性能，以及它们的行为模型表示。这些系统具有不同数量的隐藏层和不同维度的隐藏空间。表. 2给出了模型我们使用两个模型来评估具有不同参数数量和不同损失值的RNN的属性。特别是M1被训练以获得更高的准确性，而M2的大量参数表明其潜在的表2：LSTM及其抽象模型M1M2隐藏层1 4隐藏状态维度，亮度（hl）80 60总参数43，884 115，964训练损失1.70 1.84验证损失1.45 1.58抽象状态数据和验证设置这些下一个字符RNN是在Nietzsche数据集上训练的，σ= Σ =44，训练样本数N=580，741，序列长度n= 50。为了评估系统M1和M2的行为模型的特性，我们首先计算了一个地面真值。接下来，我们验证这些模型与我们的变化的蒙特卡罗模型检查。通过对RNN系统M1和M2的所有可能使用状态的所有属性进行穷举评估来计算地面真值。通过抽样测试实例进行蒙特卡罗模拟，通过运行模拟直到物业满意率在0以内。1ρ100%的地面真实值，其中ρ100是（9）中定义的ρ我们使用ρ100，因为稀有属性需要有更严格的界限。特性、符号和特性参数的列表5.2结果和讨论我们使用我们的Monte Carlo模型检查的变化来评估TLS的属性满意度，并将结果与地面实况进行比较。表1显示了我们的蒙特卡罗模型检验的性质验证地面真实值的属性满意度比率如表1的第四列所示。例如，M1只有29.2%的状态满足高置信度性质.高置信度、果断性和稳健性的属性满意度在（20%，40%）范围内。这些值很低，但在意料之中，因为M1和M2是简单的RNN。此外，这两种模型都证明了长期关系属性的低满意率。尽管模型M1与M2相比具有较低的验证损失（表2），但从属性的角度来看，M1相对于M2的好处是矛盾的。事实上，模型M1只有90%的覆盖率，这是“死亡”神经元数量显著的指标此外，模型M1几乎有2%的记忆，这是不够的，即， 太高了，不安全。因此，我们可以回答我们的第一个研究问题，即两种模型的财产满意率都不足以被认为是安全的，尽管M2在覆盖率上表现良好，记忆力较低模型更好地支持覆盖和记忆属性的原因之一是因为在这些模型的设计过程中考虑了这些同样有趣的是，与状态安全属性相比，时间安全属性在计算上要昂贵得多。事实上，表1的对于时间属性，需要对所有可能轨迹的18%进行采样，以接近地面真实值。时态的高验证复杂度属性是直观的，这是因为像记忆这样的时间事件被应用于整个轨迹而不是每个状态。因此，我们可以回答第二个研究问题，即与整个状态空间相比，Monte Carlo采样对于RNN模型的估计性能是有效的。第三个研究问题的答案是，国家安全属性比临时安全属性更有效地检查。差异范围从两个到四个数量级所需的样本。注意，通过对测试示例进行采样并通过运行模拟直到属性满意率在0以内来执行蒙特卡罗模拟。1ρ100%的地面真相。然而，计算地面实况并不总是计算上可行的。监测ρη（η）值的收敛性是对地面实况计算的替代。从表1中我们可以看出，状态安全性质要求e-05阶收敛，时间安全性质要求e-07阶收敛。我们可以使用这些数字来获得足够数量的样本来评估RNN模型的属性满意度。6相关工作已经有几篇论文解决了递归神经网络验证的挑战。在最近的工作（Musau和Johnson 2018）中，作者基于非线性常微分方程的可达性方法，提出了连续时间RNN的验证。另一项工作（Wang et al. 2018）将RNN抽象为确定性有限自动机，以检查RNN对对抗性攻击的鲁棒性。RNN的鲁棒性分析的另一种方法是RNN的量化输出鲁棒性（POPQORN）（Ko et al. 2019）。鲁棒性是通过计算两个线性界的输出所产生的扰动输入序列的RNN估计。这种方法可以应用于各种RNN结构，包括LSTM和GRU。DeepStellar方法（Du et al.2019）使用RNN状态的马尔可夫链表示，由于状态空间爆炸，概率性质，限制了模型的规模，并专注于覆盖度量和轨迹相似性。深度神经网络（DNN）的关键安全属性，如鲁棒性 和 安 全 性 ， 在 文 献 中 进 行 了 介 绍 和 讨 论（Canziani，Paszke和Culurciello 2016）。然而，与这里所介绍的工作不同，这些属性既没有正式定义，也没有在实际的RNN上验证。在最近的工作中（Akintunde et al. 2019），作者提出了一个用于验证递归神经代理环境系统（RNN-AES）的理论框架，它是在前馈神经网络上定义的神 经代 理环 境 系统 （MAS） 的扩 展。 该 框架 在（Akintunde et al. 2018）中实际应用于分析多智能体系统的可达性问题，该问题在控制共识问题和强化学习应用中至关重要（Wooldridge 2009;Vengertsev etal.2015; Brockman等人2016年）。7结论和今后的工作本文定义了递归神经网络的标记状态转移抽象，引入了四个新的安全性质，并形式化了定义在状态空间上的六个关键性质：高置信度、决策性、覆盖性、鲁棒性、长期关系和记忆性。我们应用蒙特卡罗模型检验方法验证所提出的属性，并证明了时间安全属性需要更长的蒙特卡罗验证相比，状态安全属性。在未来的工作中，我们将探索改进时间安全属性验证的方法，以实现更好的验证性能。为了实现这一目标，我们将开发一个更复杂的RNN系统抽象，专门为安全时间属性设计，并在更复杂的RNN模型上对其进行评估。引用Akintunde ， M.;Lomuscio ， A.;Maganti ， L.; 和Pirovano，E.2018.神经主体-环境系统的可达性分析。在第十六届知识表示与推理国际会议上。Akintunde，M. E.的; Kevorchian，A.; Lomuscio，A.;和Pirovano，E. 2019.基于rnn的神经代理环境系统的验证。 第33届AAAI人工智能会议（AAAI19）关闭KY，USA.Press. 出现。Brockman，G.; Cheung，V.; Pettersson，L.;施耐德，J.;Schulman，J.;唐，J.;和Zaremba，W.2016年。开放健身房。arXiv预印本arXiv：1606.01540。Canziani，A.; Paszke，A.;和Culurciello，E. 2016.深度神经网络模型的实际应用分析。arXiv预印本arXiv：1605.07678。Carlini，N.;刘，C.;Kos，J.;Erlingsson，U'.;和Song，D.2018.秘密分享者：测量非预期的神经网络记忆，提取秘密. arXiv预印本arXiv：1802.08232。Choi，E.;巴哈多里湾T.; Schuetz，A.;斯图尔特，W。F.地; Sun，J. 2016.艾医生：通过递归神经网络预测临床事件。In Doshi-Velez，F.; Fackler，J.; Kale，D.;Wallace，B.;和Wiens，J.，编辑， Proceedings of the1st Machine Learning for Healthcare Conference ，第56卷，Proceedings of Machine Learning Research，301-318。Chil-Chill's Hospital LA，Los Angeles，CA，USA：PMLR.Clarke Jr，E.M.; Grumberg，O.;Kroening，D.;Peled，D.;和Veith，H. 2018. 模型检查。唐纳森河Gilbert，D. 2008. 数值约束下概率LTL的蒙特卡罗模型检验器。 部 计算科学，格拉斯哥大学，研究报告TR-2008-282。杜，X.;谢，X.;李，Y.;马，L.;赵，J.;和Liu，Y. 2018年Deepcruiser：有状态深度学习系统的自动引导测试。arXiv预印本arXiv：1812.05339。杜，X.;谢，X.;李，Y.;马，L.;刘玉;和赵，J. 2019年。Deep-stellar：基于模型的有状态深度学习系统的定量分析。Gal，Y. 2016.深度学习Graves，A.; Mohamed，A. r.;和Hinton，G. 2013.深度递归神经网络语音识别。2013年IEEE声学、语音和信号处理国际会议，6645-6649。美国电气与电子工程师协会。格罗苏河，和Smolka，S. A. 2005.蒙特卡洛模型检验。在系统构造和分析的工具和算法国际会议上，271286. 斯普林格。Guo，C.; Pleiss，G.;孙，Y.; Weinberger，K. Q. 2017.现代神经网络的校准。第34届机器学习国际会议1321-1330。汉，S.;毛，H.; Dally，W. J. 2015.深度压缩：通过修剪、训练量化和霍夫曼编码压缩深度神经网络。arXiv预印本arXiv：1510.00149。Henriques，D.; Martins，J. G.; Zuliani，P.; Platzer，A.;和Clarke，E. M. 2012.马尔可夫决策过程的统计模型检验。2012年第九届系统定量评估国际会议，84-93。美国电气与电子工程师协会。Hochreiter，S.，和Schmidhuber，J.1997。长短期记忆。Neural computation9（8）：1735-1780.黄，X.; Kwiatkowska，M.; Wang，S.;和Wu，M. 2017.深度神经网络的安全性验证。三比二十九Jain，A.; Zamir， A.的R.; Savarese，S.; Saxena ， A.2016. Structural-rnn：时空图的深度学习。IEEE计算机视觉与模式识别会议论文集，5308Katz，G.; Barrett，C.; Dill，D. L.的; Julian，K.;和Kochen-derfer，M. J. 2017. Reluplex：一个用于验证深度神经网络的高效SMT求解器。97比117Kim，B.;康角，澳-地M.; Kim，J.;李，S。H.的;钟角，澳-地C.的;和Choi，J. W. 2017.基于递归神经网络的占有率栅格地图上的概率车辆轨迹预测。 2017年IEEE第20届智能交通系统国际会议（ITSC），399-404。美国电气与电子工程师协会。Ko，C.-Y的; 吕志;翁，T.-W的; Daniel，L.;Wong，N.;Lin，D. 2019. Popqorn：量化递归神经网络的鲁棒性。arXiv预印本arXiv：1905.07387。Kuper，L.; Katz，G.; Gottschlich，J.; Julian，K.;巴雷特，C.的;和Kochenderfer，M. 2018.面向安全关键型深 度 网 络 的 可 扩 展 验 证 。 arXiv 预 印 本 arXiv ：1801.05950。Madsen，A. 2019. rnns中的视觉记忆。蒸馏4.Mayer，H.; Gomez，F.; Wierstra，D.;纳吉岛; Knoll，A.;和Schmidhuber，J.2006年。一个机器人心脏手术系统，它可以使用递归神经网络学习打结。2006年IEEE/RSJ智能机器人与系统国际会议，543Musau，P.，和Johnson，T. T. 2018.验证持续-连续时间递归神经网络（基准建议）。在ADHS，196Nghiem ， T.; Sankaranarayanan， S.;Faine k os ， G.;Ivanci c′，F.; 古普塔，A.; Pappas，G. J. 2010.非线性混合系统时间特性证伪的蒙特卡罗方法。在第13届ACM混合系统国际会议论文集：计算与控制，211-220. ACM。Pei，K.;曹玉;杨，J.;和Jana，S. 2017. Deepxplore：深度学习系统的自动白盒测试1比18Pnueli，A. 1981.并发程序的时态语义。理论计算机科学13（1）：45-60。普利纳湖和Tacchella，A. 2012.使用smt求解器验证神经网络。AI Communications25（2）：117-135.Szegedy，C.;扎伦巴，W.; Sutskever，I.;布鲁纳，J.;Erhan，D.;古德费洛岛和Fergus，R. 2013.神经网络的有趣特性arXiv预印本arXiv：1312.6199。田，Y.; Pei，K.; Jana，S.; Ray，B. 2018.深度测试：深度神经网络驱动的自动驾驶汽车的自动化测试。第40届软件工程国际会议论文集303-314。Tretmans，J. 1996年。标签转换系统的一致性测试：实现关系和测试生成。计算机网络和ISDN系统29（1）：49-79。Vengertsev，D.;金，H.; Seo，J. H.; Shim，H. 2015.输出耦合高阶线性多智能体系统在确定性和马尔可夫切 换 网 络 下 的 一 致 性 。 International Journal ofSystems Science46（10）：1790-1799.王，Q.;张，K.;刘，X.;和Giles，C.L. 2018年通过规则提 取 验 证 递 归 神 经 网 络 。 arXiv 预 印 本 arXiv ：1811.06029。Wooldridge，M. 2009. 多智能体系统简介。约翰·威利父子公司