循环神经网络特性及其蒙特卡洛技术验证

版权归作者所有。递归神经网络的性质及其蒙特卡罗验证Dmitry Vengertsev1，Elena Sherman11博伊西州立大学计算机科学系1910UniversityDrive，Boise，Idaho 83725dmitryvengertsev@u.boisestate.edu，elenasherman@boisestate.edu摘要随着RNN在医疗和汽车领域的应用，它们成为关键系统的一部分，传统上需要彻底的验证过程。在这项工作中，我们提出了如何将RNN行为建模为标记的转换系统，并正式定义了一组这样的模型的状态和为了验证这些属性，我们建议使用蒙特卡罗方法，并评估其有效性，不同类型的属性。我们对两个RNN模型进行了我们的实验表明，我们的模型满足更好的状态属性比时间属性。此外，我们表明，蒙特卡罗抽样是非常有效的状态属性验证，这通常需要一小部分的RNN的模型进行探索。然而，为了验证时间特性，蒙特卡罗需要分析高达20%的计算。1引言递归神经网络（RNN）已经成为许多普遍存在的应用中的核心组件，诸如车辆轨迹估计（Kim et al.2017 ） 、 语 音 识 别 （ Graves 、 Mohamed 和 Hinton2013）、机器翻译以及其计算取决于先前处理的输入序列的许多其他技术。随着在这些领域的成功证明，现在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和Tacchella2012; Kuper等人2018）。然而，DNN与RNN本质上不同，RNN被构造成处理输入序列，使得下一个输入从处理输入的前序项所产生的配置开始处理序列中的元素因此，虽然有价值，但先前关于DNN验证的工作可能不完全适用于RNN，并且没有解决RNN的所有验证场景。例如，ReluPlex（Katz et al. 2017）可以使用ReLu函数的分段线性特性正式验证神经网络的安全特性。此外，在以前的工作中定义的大多数性质是由学术研究人员开发的，而不是必要的实践者，这可能会阻碍工业实践者对其的适应。在这项工作中，我们专注于定义和形式化特定于RNN的新状态和时间属性。此外，我们还正式以前定义的实际属性，适用于神经网络。特别地，我们识别并形式化四个状态安全属性：高置信度、决策性、鲁棒性和覆盖率，描述了理想的RNN配置。此外，我们引入并形式化两个时间安全属性：长期关系和记忆，其表征RNN的配置的允许系列，因为它们在处理输入序列中的每个元素之后出现。我们在描述RNN如何处理输入序列的模型的上下文中定义属性我们选择将RNN行为建模为标记状态转换系统，其中状态表示处理单个符号后RNN内部节点的值因此，如果在处理输入符号之后，由第一状态描述的RNN在这项初步工作中，所提出的RNN模型没有抽象，因此它代表了RNN在所有可能的输入序列上的具体行为为了验证RNN模型的拟议属性，我们使用蒙特卡罗采样，因为没有抽象的模型有一个大的状态空间，其完整的验证相当于穷举测试。蒙特卡罗抽样提供了一个更广泛的适用性和可扩展的替代随机系统的属性验证，使用数值和符号的方法。版权所有© 2020由其作者。在知识共享许可署名4.0国际（CC BY 4.0）下允许使用。× ∪{ } ×不∈1−| ∈ ∈|∈∈十二蒙特卡罗模型检测技术已经成功地应用于分析计算机网络、安全和系统生物学等领域中具有大状态空间的系统（Grosu和Smolka 2005; Donaldson和Gilbert2008; Nghiem等人2010）。在我们的论文中，我们想通过研究实现地面真实结果所需的状态空间采样的百分比来研究蒙特卡罗采样是否是验证RNN模型的合适方法。在我们的实验中，我们通过详尽地探索RNN模型的整个状态空间来计算地面实况。我们在两个大型RNN系统上进行实验，我们将其建模为标记的过渡系统。接下来，我们确定六个属性的真实情况，并评估蒙特卡罗模型检验的适用性。我们使用评估结果回答以下研究问题：用于对过程的行为进行建模，并作为各种形式化规范语言的语义模型下面我们介绍LTS的定义，然后描述如何使用这个转换系统来建模RNN行为标签转换系统（Tretmans 1996）是一个四-tuple（S，L，T，S0）其中：1. S是一个可数的、非空的状态2. L是可数标号3. 不的（Lτ）S是一个转换关系，其中L表示可观察的相互作用，以及用于模拟内部转换的特殊标签τ∈/L。4. S0S是初始状态的集合。我们需要使用LTS来建模RNN，它接受-puts（x1，. . . ，Xt），并且具有隐藏状态（h1，. . . 、h、l），以及1吨1. 所提出的属性是否适用于我们的RNN模型？2. Monte Carlo模型检测对这些模型的效率如何？3. 蒙特卡罗模型检验的效率是否结果表明，并不是所有的状态在RNN模型具有状态属性，这表明我们的RNN的弱点。此外，长期的时间属性具有更低的满足率。这意味着未来的评估应该在更复杂的RNN上进行。我们的研究结果还表明，蒙特卡罗模型检验可以是非常有效的验证状态属性，但是，它需要更多的样本收敛到地面真理的时间属性。除了回答上述研究问题外，我们的工作还做出了以下贡献：它正式定义了RNN的状态和时间安全属性。• 它实现了两个RNN系统的RNN模型。它采用蒙特卡罗模型检验来验证RNN模型的性质。论文的其余部分组织如下。在第2节中，我们将RNN表示为标记的转换系统。在第3节中，我们描述了所提出的状态和时间安全属性的形式化的细节。在第4节中，我们简要介绍了蒙特卡罗模型检验的验证所提出的表示。在第5节中，提供了实验结果第6节介绍了相关的工作，我们总结了未来的工作计划的文件。2递归神经网络网络系统过程验证的第一步是确定如何以适合验证其属性。系统的一般行为产生输出（y1，. . .，yt），其中xtσ是来自大小为σ=Σ，yt的训练集字母表Σ的字符的独热编码向量σ，hl其中l是隐藏层的指示符，并且m是隐藏向量的维度在我们的演示中，我们使用n表示输入序列长度，R描述层数。图1：具有三层的RNN的状态表示（a）和对应的RNN表示为标记的状态转换系统（b）背后的直觉的示例。类似于先前的工作（Du et al.2018），LTS状态表示RNN的配置 我们使用元组（H，Y）来描述这种配置，其中H是RNN的隐藏状态向量，Y是输出。 例如，（H1，Y1）是在处理单个符号X1=（x1，¯ 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，¯0TEM被建模为状态转换系统。在这项工作中，我们二一二n−2）。图1显示了LTS如何对选 择 将 RNN 行 为 建 模 为 标 记 转 换 系 统 （ LTS ）（Tretmans 1996）。LTS由状态和这些状态之间的标记转换组成，其中标签标识在系统上执行的某些操作LTS形式主义是输入序列（X1，X2，X3）上的RNN行为。形式上，RNN的LTS可以定义如下：定义2.1.RNN行为模型M=（S，L，T，S0），其中··•我的天•我的天•××我•∈¬∧∨∈∈≥l−1lS=（H，Y）i∈N是一组状态，定义为隐状态和对应的输出值（H，Y）i的元组，其中N是状态数。L=Xii∈N是基于输入向量Xi不的十S是转换，即每个转换在其上具有输入向量X13RNN中的转换通过隐藏向量来组织，使得在时间步长t处的输出yt变为直到t的所有输入向量的函数，{x1，. . .，Xt}。递归（h，h）→h 是-为了定义转换系统的属性，我们使用线性时态逻辑（LTL）（Pnueli 1981），它形式化了有限状态系统中行为的在有限状态系统中，LTL描述了树的一组单次计算的期望行为LTL是一个强大的形式主义，然而，在我们的工作中，我们只使用它的片段，我们提供了一个简短的解释。LTL公式具有Af的形式，其中Af是路径量词，意味着来自给定状态的所有计算路径具有属性f，并且f是被RNN系统罚款。t−1t不m×n×R只包含原子命题，并正式定义为（Clarke Jr et al. 2018年）：• S0=（H0，Y0）是初始状态H0=，以及Y0= σ×n，其中σ×n是大小为σ × n的零矩阵.在这样的转换系统中，我们可以定义谓词函数，可以推理H和Y状态分量。而且，我们可以定义一个迹tr，它是一个序列的状态（S0，S1，S2，. . .其中（Si，Si+1）∈T，i∈（0，. . . ，n-1）。3递归神经网络的性质在形式验证中，模型的性质被定义为原子命题上的公式，即状态谓词功能因此，在我们形式化RNN的状态和为了在下面表达期望的性质，我们定义四个状态预测：你好罗罗和考夫除了定义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≤Kr，其中S1，跃迁：（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 等 人2017）。由softmax层估计的预测概率并不总是可靠地用作置信因子，并且识别朝向更高置信度的偏差对于系统的安全行为至关重要我们将决策性属性定义为当给定模型不能提供高置信度输出时，对该模型提供低置信度输出的评估定义3.3.决定性属性：我们说M是决定性的，如果对于整个系统，当Hi不对所有路径全局成立时，性质Lo成立，因此G（¬Hi（a）∧Lo（b））（2）是验证整个系统的公式。鲁棒性以前的工作表明，简单的梯度方法可能容易受到输入的小修改，这导致输出类的变化（Szegedyet al. 2013）。尽管神经网络与鲁棒性相关的属性在文献中得到了很好的研究，但为了完整性，我们在RNN行为模型中定义了它们为了使RNN对对抗性攻击具有鲁棒性，它应该具有隐藏层的内部多样表示即可见空间r中的小扰动在潜在空间中产生鲁棒扰动，并且因此产生响应Yjj∈J，其接近于未扰动响应Yi图2。定义3.4.耐用性：我们说M是鲁棒的，如果对于整个系统，性质Ro（r，K）对所有路径全局成立，因此GRo（r，K）（3）是整个系统验证的公式。图2：谓词的鲁棒转换示例Ro（r，K）。覆盖神经元覆盖属性通常用于测试神经网络（Pei etal.2017; Tian等人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+p（n）的序列上进行评估，其中p（n）> 0是n的线性函数。形式上，长期性质在迹trn+p（n）=（S1，，Sn，Sn+1，，Sn+ρ（n））=trntrρ（n），以检查该模型是否在迹trn和相邻迹trρ（n）上提供u个置信预测模型的置信度没有显著降低，并且仍然提供了V置信度预测，其中|TRN|= n，|=ρ（n）。|= ρ (n).定义3.6.长期关系属性：我们说M满足长期关系性质，如果对于整个系统，对于所有路径，性质Hi（a）在迹tr n上至少u次成立，并且性质Hi（d）在相邻迹trp（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 0。此属性可以总结为以下正则表达式：ρi（1−ρ）n−triP r（ρ）Pr（tr）在到目前为止采样的迹线的总数η中，我们将k表示为满足性质Φ的迹线tr的数量。Bernoulli分布Pr（ρ）的共轭先验是Beta分布1ρα−1（1−ρ）β−1，其中α和β是Gµ（q，e）β（α，β）Beta分布的形状参数使用Σ tri=k，we：（（¬Hi（e））∠Hi（e）（¬Hi（e））∠）q（6）其中，q n是给定条件下的记忆情况的数量。可以将后验公式（7）改写为以下形式：Σtr+α−1n−Σtr+β−1跟踪路径然而，记忆性是不可取的，所以我们Pr（ρ|tr）= ρi（1−ρ）iPr（ρ）Beta（α+k，β+n−k）（八）正在检查RNN系统是否缺乏记忆G µ（q，e）。我们现在提出一种验证方法，用于评估这些属性。4RNN行为模型由于后验由具有（8）中给出的新参数的β分布，因此具有满足性质Φ的轨迹的估计概率经由估计的平均值ρ和方差ν给出，如下：Pr（φ）=ρ±√ν=当被验证系统具有大的状态空间时，k+αα+β+n.（α+k）（n−k+β）（α+n+β）2（α+n+β+1）（九）用传统的模型检查技术来验证它变得不可行。一些技术研究各种启发式方法以引导模型检查器通过大的状态空间（Henriques et al. 2012）。另一种有前途的方法是通过对状态空间进行随机采样来处理状态空间爆炸，然后应用概率理论来推理模型的整体正确性（Grosu和Smolka，2005年）。在这样的随机采样方法中，使用离散事件模拟（蒙特卡罗实验）重复执行模型，而不需要明确的表示。路径公式在由模拟生成的每个迹线上检查φ。经检查的迹线提供伯努利随机变量的样本点，如果Φ保持，则该样本点为1，否则为0。模型被模拟有限多次，并且如果采样发现违反性质，则报告该违反，否则计算模型违反性质的概率。然而，对于这项工作，我们希望我们的系统有许多路径的属性被违反。因此，传统的蒙特卡罗模型检验，停止在第一个属性违反跟踪不会给我们完整的描述模型。为了估计我们的模型的属性保持的程度，我们基于后验概率评估进行采样。对于每个属性φ，我们将使用相应的估计概率ρ（n）与样本数n的收敛性来决定何时停止采样。根据我们的经验估计，当ρ的值接近真实值时，我们计算收敛率的值。我们将ρ-收敛定义如下：ΣW|/W|/Wi=1其中W是我们计算估计概率值之间的平均值的采样窗口。5实验评价的目标是回答以下研究问题：1. 所提出的属性是否适用于我们的RNN模型？2. 对于这些模型，蒙特卡罗抽样的效率如何？3. 蒙特卡罗抽样效率是否取决于属性类型？在本节中，我们首先描述了实验设置，其结果和上述研究问题的答案。±不| |表1：属性满足率的真实值和实现相同比率值所需的蒙特卡罗样本的数量。财产符号的参数地面真相样品pnvergence月份m1米2月份m1米2月份m1米2高置信度决策性鲁棒性覆盖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系统Ml和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的益处是矛盾的。实际上，模型Ml仅具有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等人2019）使用RNN状态的马尔可夫链表示，由于状态空间爆炸，概率性质，限制了模型的规模，并专注于覆盖度量和轨迹相似性。深度神经网络（DNN）的关键安全属性，如鲁棒性 和 安 全 性 ， 在 文 献 中 进 行 了 介 绍 和 讨 论（Canziani，Paszke和Culurciello 2016）。然而，与这里介绍的工作不同，这些属性既没有正式定义，也没有在实际的RNN上验证。在最近的工作（Akintunde et al. 2019）提出了一个用于验证递归神经代理环境系统（RNN-AES）的理论框架，该框架是在前馈神经网络上定义的神经代理环境系统（MAS）的扩展。该框架实际应用于（Akintunde et al. 2018）用于分析多智能体系统的可达性问题，这在控制共识问题和强化学习应用中至关 重 要 （ Wooldridge 2009; Vengertsev et al. 2015;Brockman等人2016）。7结论和未来工作在本文中，我们定义了来自递归神经网络的标记状态转移抽象，我们引入了四个新的安全属性，并形式化了定义在状态空间上的六个关键属性：高度自信、果断、覆盖面广、稳健、长期关系和记忆力。我们应用蒙特卡罗模型检验方法验证所提出的属性，并证明了时间的安全属性需要更长的蒙特卡罗验证相比，国家的安全属性。在未来的工作中，我们将探索方法，以提高验证的时间安全属性，以实现更好的验证性能。为了实现这一目标，我们将开发一个更复杂的抽象的RNN系统，专门为安全的时间属性，并评估它更复杂的RNN模型。引用Akintunde ， M.;Lomuscio ， A.;Maganti ， L.; 和Pirovano，E.2018.神经主体-环境系统的可达性分析。第十六届知识表示与推理原理国际会议（SixteenthInternationalConferenceonPrinci-plesofKnowledge）Akintunde，M. E.; Kevorchian，A.; Lomuscio，A.;和Pirovano，E. 2019.基于rnn的神经代理环境系统的验证。 第33届AAAI人工智能会议论文集（AAAI19）。关闭KY，USA.中国出版社. 出现。Brockman，G.; Cheung，V.; Pettersson，L.; Schneider，J.; Schulman，J.;Tang，J.;和Zaremba，W.2016年。开放健身房。arXiv预印本arXiv：1606.01540。Canziani，A.; Paszke，A.;和Culurciello，E. 2016.深度神经网络模型的实际应用分析。arXiv预印本arXiv：1605.07678。Carlini，N.;Liu，C.;Kos，J.;Erlingsson，U´.;和Song，D.2018.秘密分享者：测量无意的神经网络记忆&提取秘密。arXiv预印本arXiv：1802.08232。Choi，E.;巴哈多里湾T.; Schuetz，A.; Stewart，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-dren'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。Du，X.; Xie，X.; Li，Y.; Ma，L.; Zhao，J.;和Liu，Y.2018年。Deepcruiser：有状态深度学习系统的自动引导测试。arXiv预印本arXiv：1812.05339。Du，X.; Xie，X.; Li，Y.; Ma，L.; Liu，Y.;和Zhao，J.2019年。深星：有状态深度学习系统的基于模型的定量分析。Gal，Y. 2016.深度学习Graves，A.; Mohamed，A. r.;和Hinton，G. 2013.深度递归神经网络语音识别。2013年IEEE声学、语音和信号处理国际会议，6645-6649。IEEE。格罗苏河和Smolka，S.上午2005.蒙特卡罗模型检验。在系统构造和分析的工具和算法国际会议上，271286. 斯普林格Guo，C.; Pleiss，G.; Sun，Y.;和Weinberger，K.问.2017.现代神经网络的校准。第34届机器学习国际会议1321-1330。Han，S.; Mao，H.; Dally，W. J. 2015.深度压缩：使用修剪、训练量化和霍夫曼编码压缩深度神经网络。arXiv预印本arXiv：1510.00149。Henriques，D.; Martins，J. G.; Zuliani，P.; Platzer，A.;和Clarke，E.先生2012.马尔可夫决策过程的统计模型检验。2012年第九届系统定量评估国际会议，84-93。IEEE。Hochreiter ， S. ， 和 Schmidhuber ， J. 1997. 长 短 期 记忆。Neural computation9（8）：1735-1780.Huang，X.; Kwiatkowska，M.; Wang，S.;和Wu，M.2017.深度神经网络的安全性验证。3-29Jain，A.; Zamir，A. R.; Savarese，S.; Saxena，A. 2016.结构-rnn：时空图的深度学习。IEEE计算机视觉与模式识别会议论文集，5308Katz ， G.; Barrett ， C.; Dill ， D. L.; Julian ， K.; 和Kochen-derfer，M. J. 2017. Reluplex：一个用于验证深度神经网络的高效SMT求解器。97-117Kim，B.; Kang，C. M.; Kim，J.; Lee，S. H.; Chung角C.;和Choi，J.水渍2017.基于递归神经网络的车辆轨迹概率预测。2017年IEEE第20届智能交通系统国际会议（ITSC），399-404。IEEE。Ko，C.-Y.; Lyu，Z.;翁，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.没有2018.持续性验证连续时间递归神经网络（基准建议）。在ARCH@ADHS，196Nghiem ， T.; Sankaranarayanan， S.;Faine k os ， G.;Ivanci c´，F.; Gupta，A.;和Pappas，G. J. 2010.非线性混合系统时间特性证伪的蒙特卡罗技术。 在关于混合系统的第13届ACM国际会议的会议录中：计算与控制211-220. ACM。Pei ， K.; Cao ， Y.; Yang ， J.; 和 Jana ， S. 2017.Deepxplore：深度学习系统的自动白盒测试1-18Pnueli，A. 1981.并发程序的时态语义。TheoreticalComputer Science13（1）：45-60.普利纳湖和Tacchella，A. 2012.挑战SMT求解器以验证神经网络。AI Communications25（2）：117-135.Szegedy，C.;扎伦巴，W.; Sutskever，I.; Bruna，J.;Erhan，D.;古德费洛岛和Fergus，R. 2013.神经网络的有趣特性arXiv预印本arXiv：1312.6199。Tian，Y.; Pei，K.; Jana，S.;和Ray，B. 2018.深度测试：深度神经网络驱动的自动驾驶汽车的自动测试。第40届软件工程国际会议论文集303-314。Tretmans，J. 1996.标签转换系统的一致性测试：实现关系和测试生成。计算机网络和ISDN系统29（1）：49-79.Vengertsev，D.; Kim，H.; Seo，J.H.; Shim，H. 2015.输出耦合高阶线性多智能体系统在确定性和马尔可夫 切 换 网 络 下 的 一 致 性 。 International Journal ofSystems Science46（10）：1790-1799.Wang，Q.;Zhang，K.;Liu，X.;和Giles，C.法律2018年。通过规则提取验证递归神经网络。arXiv预印本arXiv：1811.06029。Wooldridge，M. 2009. 多智能体系统简介。约翰威利父子公司