深度神经网络的神经符号验证方法及其应用

+v：mala2277获取更多论文深度神经网络Xuan Xie1，Kristian Kersting2，Daniel Neider11马克斯·普朗克软件系统研究所，德国2德国达姆施塔特工业大学计算机科学系摘要形式化验证已经成为确保深度神经网络安全性和可靠性的一种强大方法。然而，目前的验证工具仅限于少数几个属性，可以表示为一阶约束的输入和输出的网络。虽然对抗性鲁棒性和公平性属于这一类别，但许多现实世界的属性（例如， 为了缓解这种严重的实际限制，我们引入了一种新的框架来验证神经网络，称为神经符号验证。其关键思想是使用神经网络作为逻辑规范的一部分，从而能够验证各种复杂的真实世界属性，包括上述属性。此外，我们还演示了如何在现有的神经网络验证基础设施上实现神经符号验证，使我们的框架易于研究人员和从业人员访问。1介绍深度神经网络在感知和自然语言处理等领域的卓越性能使其成为许多现实世界人工智能系统的组成部分，包括医疗诊断和自动驾驶等安全关键系统然而，神经网络本质上是不透明的，并且在最先进的网络中发现了各种缺陷。其中最著名的可能是缺乏对抗鲁棒性[Szegedyetal. ，2014]。这个术语描述了这样一种现象，即即使是神经网络输入的轻微扰动也会导致完全不同的输出。事实上，基于学习的系统中缺陷的普遍存在促使引入了专用数据库来监测人工智能事件并避免重复出现不期望的结果[McGregor，2021]。1受软件可靠性十年来的发展的推动，形式化验证已经成为一种强有力的方法，联系作者（neider@mpi-sws.org）第1https://incidentdatabase.ai/确保神经网络的正确性和安全性（我们参考第2节以了解更多细节）。与来自机器学习的（经验）统计评估方法（如交叉验证）相比，形式验证技术具有很大的优势，即它们不限于仅在有限数量的输入上检查给定属性。相反，它们允许验证一个属性对深度神经网络的所有（或至少无限多个）输入都成立，包括看不见的数据和角落情况。然而，形式验证有一个基本的限制，往往构成了一个重大的障碍，在实践中：它需要验证的属性可以表示为虽然对抗鲁棒性和公平性属于上述类别，但许多现实世界的属性仍然不在现有验证技术的范围内。例如，考虑一个控制自动驾驶汽车的深度神经网络，以及汽车在前视图中出现停车标志时需要减速的特性。不难看出，根据对深度神经网络的输入和输出的约束来形式化这个属性是非常困难的，如果不是不可能的话：它需要在图像像素的水平上捕获所有可能的停车标志的所有基本特征，例如它们的如果这是可能的，那么机器学习首先就不是必要的，因为人们可以基于这样的正式规范来实现检测为了克服这一严重限制，并使形式化验证适用于现实世界的场景，我们提出了一个用于验证深度神经网络的神经符号框架。 遵循神经符号推理的一般思想[d'AvilaGarcez etal. ，2019;Raedtet al. ，2020]，我们的关键贡献是一种新的规范语言，名为神经符号断言语言（ NESAL），它允许将逻辑规范和深度神经网络结合起来。我们称之为规范网络的神经网络充当复杂语义属性的代理，并将感知和自然语言识别等领域的进展整合到形式验证中。在上面的例子中，我们可以训练一个高度专业化的规范网络来检测停车标志。然后，期望的属性可以直接表达为我们arXiv：2203.00938v1 [cs.AI] 2022年3+v：mala2277获取更多论文2∈× →≥∈∈联系我们^∈在第3节中，我们将介绍我们的神经符号框架，在那里我们还将讨论在实践中获得规范网络的方法。我们的框架的一个基本特征是，它可以建立在现有的神经网络验证基础设施之上，我们在第4节中通过基于流行的Marabou框架[Katzet al. ，2019]。在第5节中，我们然后表明，我们的原型有效地验证了各种神经符号属性，并可以产生翔实的反例失败的验证尝试。 作为我们验 证 的 目 标 ， 我 们 已 经 在 德 国 交 通 标 志 识 别 基 准（GTSRB）上训练了深度神经网络[Stal-lkampet al. ，2011]和MNIST [LeCunet al. ，2010]。最后，我们要强调的是，我们的神经符号框架是通用的，并不局限于深度神经网络。相反，原则上，它可以应用于任何系统，允许适当的验证技术，包括基本模型，硬件和软件。然而，我们把对这一有希望的方向的深入研究留给今后的工作。相关工作在对值得信赖和可靠的人工智能需求的推动下，深度神经网络的形式化验证在过去五年中已成为一个非常活跃和 充 满 活 力 的 研 究 领 域 （ 我 们 请 读 者 参 阅 教 科 书[Albarghouthi，2021]以了解详细概述）。 据我们所知，Seshia等人。 [2018]对神经网络验证中出现的正确性属性进行了首次全面调查。与软件验证类似，作者将这些属性分为几个（不一定是不相交的）类别：系统级规范、输入输出鲁棒性、其他输入输出关系、语义不变性、单调性、公平性、输入/分布假设、覆盖率标准和时间规范。然而，我们不知道有任何工作提出了神经符号验证方法，无论是对于深度神经网络或其他差分模型，还是对于硬件或软件。神经符号AI的主要动机是将符号和深度神经表示的优势结合到联合系统中[d'Avila Garcez etal. ，2009;d'AvilaGarcez etal. ，2019;Jiang and Ahn，2020;d'Avila Garcezand Lamb，2020 ].这通常是在一个混合的时尚，其中神经网络作为一个感知模块，与符号推理系统接口[Yietal. ，2018;Maoet al. ，2019]。这种方法的目标是减轻一种类型的表示被另一种类型表示的问题（例如，使用符号推理的能力来处理神经网络的一般化问题和通过神经网络处理符号系统的噪声数据的困难）。最近的工作也表明，提出了可以说，最有前途的，因此，最流行的是抽象的解 释 [ 格 尔 等 人 。 ， 2018;Singhet al. ， 2018;Bonaertetal. ， 2021;Henriksen andLomuscio ， 2021] 和 演 绎 验 证[Ehlers，2017;Katzet al. ，2019]。前者在无限数量的输入上执行网络抽象的计算，而后者将验证问题简化为逻辑公式的可满足性检查（我们在第2节中对两者进行了概述）。此外，还提出了各种其他方法，这些方法通常来自 现 有 的 软 件 验 证 技 术 示 例 包 括 基 于 优 化 的 方 法[Gowalet al. ，2019]，concolic测试[Sunet al. ，2018]，模型检查[Liuet al. ，2020]，细化类型[Kokkeet al. ，2020]和基于分解的方法[Kouvaros和Lomuscio，2021;Battenetal. ，2021]。虽然我们的神经符号框架是独立的实际验证技术，我们专注于演绎验证在本文中。如上所述，我们留下了一个深入的研究，其他技术可以受益于我们的方法，为未来的工作。2神经网络验证神经网络验证是正式证明深度神经网络满足语义属性（即，涉及由网络计算的语义函数的属性为了避免在本节中出现太多技术细节，让我们通过两个流行的例子来说明这个任务我们将在第3节介绍神经符号验证框架时对神经网络验证进行形式化。在对抗鲁棒性的情况下，人们想要证明神经网络对其输入的小扰动是鲁棒的（即，输入的微小变化不会改变输出）。为了使这在数学上精确，让我们假设我们给定一个多类神经网络f：Rmc1 ， . . . ， cn，具有m个特征和n个类，特定输入→x*Rm，距离函数d：RmRmR+，以及距离ε 0。然后任务是证明，d（→x*，→x）≤ε蕴含f（→x*）=f（→x）（1）对于所有输入→xRm. 换句话说，→x*的类和从→ x * 开始的每一个至多εaway的输入必须一致。输入→x违反性质（1）的Rm称为自反例并证明f不是对抗性强的。在公平性的情况下，人们想要证明神经网络的输出不受性别或种族等敏感特征的影响再次，让我们假设我们给定一个神经网络f：Rm→Rn，具有m个特征，包括敏感特征i∈ {1，.，m}。 接下来的任务是证明神经符号XAI的优势[Ciravegnaet al. ，2020年;Stammer等人，2021]和常识推理[Arab-shahiet al. ，2021]。然而，与核查的联系并没有xixi′<$xj=x′j蕴含f（→x）=f（→x′）（2）j/= i被探索了很多。Yanget al.[2021]探索了符号传播，但高阶规范框架并不存在。为了自动验证深度神经网络的正确性属性，已经开发了许多不同的技术。对于所有输入对→x，→x′ Rm，其中→x=（x1，. . . ，xm），以及→x′=（x1′，. . . xm′）。换句话说，如果两个输入→x和→x′只在一个敏感特征上不同，那么f的输出一定不变化注意，在公平性的情况下，反例由输入对→x，→x′组成。+v：mala2277获取更多论文3→¬¬¬¬∈性质（1）和（2）展示了神经网络验证的一个基本挑战：任务是证明所有（通常是无穷多个）输入的性质因此，机器学习的交叉验证或其他统计方法不再足够，因为它们只在有限数量的输入上测试网络相反，人们需要使用可以对给定网络进行象征性推理的方法。受现代软件验证成功的推动，最近提出了许多用于神经网络验证的符号方法[Albarghouthi，2021]。其中最流行的两种是演绎验证[Ehlers，2017;Katzet al. ，2019]和抽象解释[Gehretal. ，2018;Singhet al. ，2018]。让我们简单地描述一下两者。演绎验证的关键思想是将深度神经网络f：RmRn与语义prop-P一起编译成逻辑公式f，P，称为验证条件。这个公式通常属于实数算术的无量词部分，并且被设计为有效的（即，满足所有输入）当且仅当f满足P。 为了证明f，P的有效性，我们检查它的否定f，P是否可满足。这可以通过现成的饱和度模理论求解器（如Z3 [de Zona和Bjørner，2008]）或使用最近提出的特定约束求解器之一来完成，如Planet [Ehlers，2017]或Marabou [Katzet al. ，2019]。如果f，P是不可满足的，则f，P是有效的，并且通过构造，f满足P。 如果如果f， P是可满足的，则f， P是无效的，这意味着f违反了性质P.在后一种情况下，大多数约束求解器（包括上面提到的那些）可以产生满足f，P的分配，然后可以用来提取f的输入，证明P的违反。抽象解释是一个数学框架，用于计算软件和其他复杂系统的语义的声音和精确近似[Cousot和Cousot，1977]。当应用于神经网络验证时，其基本思想是在无限输入集上过度近似深度神经网络的计算。每一个这样的无限集合都用一个所谓的抽象域的元素来象征性地表示，抽象域由逻辑公式组成，这些逻辑公式捕捉了n维盒子、多面体或带形等形状。为了近似网络由于层操作的是具体值而不是抽象元素，因此这种传播需要将每一层替换为抽象层（称为抽象Transformer），该抽象层计算层对抽象元素的影响。因此，当给定网络f的输入空间中的抽象元素A（例如，代表一个固定输入→x*的邻域），抽象解释的结果是输出空间中的一个抽象元素A′过逼近具体输入x A的所有输出f（x）。为了验证一个属性P是否成立，只需检查A′是否包含在一个表示所有满足P的输出的抽象元素中。 由于抽象解释计算网络的实际输入-输出行为的过度近似，特性P通常描述安全条件。虽然神经网络验证是一个充满活力和高度活跃的领域，但几乎所有现有的研究都存在三个问题：实质性缺点：1. 现有的研究集中在验证可以使用网络输入和输出上的无量词一阶约束来形式化的关系这些属性的示例包括对抗鲁棒性和公平性，如上面的属性（1）和（2）然而，绝大多数相关的正确性属性不能以这种简单的方式表达。例如，考虑控制自动驾驶汽车的神经网络，以及汽车需要在前视图中出现停车标志时立即很明显，将这个属性形式化是非常困难的（如果不是不可能的话，正如Seshia和Sadigh[2016]所认为的那样）：它需要我们在数学上捕捉所有可能的停车标志的所有基本特征，包括它们的位置，形状，角度，颜色等。2. 事实上，今天在神经网络验证中考虑的所有属性都是局部的（指先验固定输入→x* 附 近 的输入）或全局的（指所有输入）。对抗鲁棒性是前一种类型的一个例子，而公平性说明了后者。然而，更自然和有用的方法将是将验证限制为来自底层数据分布的输入，因为我们通常不期望我们的网络处理分布外的数据。同样，这样的限制很难在数学上捕捉，因此，目前的方法没有。3. 一个基本问题，特别是在验证全局性质时，是反例（即，见证该属性的违反的输入）经常是不分布的，因此没有什么价值。同样，将验证限制于源自底层数据分布的输入将缓解该问题，但不被当前方法支持。在下一节中，我们将通过引入用于神经网络验证的神经符号框架来解决这些缺点3一个神经符号验证框架如属性（1）和（2）所示，当今实数算术的无量词片段）。这一要求从根本上将当前的验证方法限制在只有几种不同类型的正确性属性上，可以说这使得它们无法处理现实世界的AI验证任务。作为克服这一严重的实际限制的第一步，我们提出了一个神经符号的方法来验证神经网络。我们的主要想法看似简单但功能强大：我们建议使用高度专业化的深度神经网络，称为规范网络，作为捕获语义正确性属性的代理对象我们将在3.1节中介绍规范网络的概念以及获得规范网络的可能方法。 在第3.2节中，我们提出了一个无量词一阶逻辑片段来形式化涉及规范网络的正确性性质。我们称这种类型的属性为神经符号和由此产生的断言语言NESAL。+v：mala2277获取更多论文4.Σ→←→ ∈{}.Σ∈联系我们一旦我们定义了新的断言语言，第4节演示了如何检查NESAL属性可以减少到神经网络的演绎验证。这种减少 允 许 利 用 任 何 现 有 的 演 绎 验 证 器 （ 例 如 ， Planet[Ehlers，2017]，Reluplex [Katzet al. ，2017]或Marabou[Katzet al. ，2019]），使我们的神经符号验证框架很容易为研究人员和从业者所用。值得指出的是，其他神经网络验证技术也可以提升到神经符号验证，但我们将这一研究方向留给以后的工作。3.1规范网络一般来说，规范网络是针对特定任务训练的高度专业化的深度神经网络（例如，感知、异常检测、识别底层数据分布等）。我们使用一个（或多个）这样的网络作为代理对象来捕获正确性属性.它们的精确架构在这一点上并不重要，但可能会影响使用哪种验证引擎的选择。让我们使用第2节中的自动驾驶汽车示例来说明规范网络的概念。 为了简单起见，让我们假设我们被给予• 深度神经网络工作器f，其将来自前置摄像头的图片→x作为输入，并输出转向命令• - 属性P，其陈述而不是试图在逻辑中形式化停止标志的所有特征（即，它们可能的位置、形状、颜色等），我们现在训练第二深度神经网络G用于识别停车标志的特定感知任务。假设g是一个二进制类网络（如果它在图像中检测到停车标志，则输出如果g（→x）=“是”，则f（→x）=“减速”。（三）请注意，我们原来的性质P现在相当于对网络f和g的输入和输出的简单约束。我们的框架的一个基本要求是适当的规范网络的可用性。我们在这里素描三如何获得它们的可能方法：1. 获得规范网络的最简单的方法为了避免系统误差，在与用于训练验证网络的数据集不同的数据集上训练规范网络至关重要。优选地，应该另外使用不同的架构和超参数。2. 类 似 于 标 准 数 据 集 ， 如 MNIST [LeCunetal. ，2010]，研究人员和感兴趣的公司可能会为规范网络创建公共存储库。为了引导这种努力，我们制定了具体的-例如，这种方法可以用于保证神经网络在安全关键应用中的正确性和可靠性的最低标准。类似地，认证机构（如德国3.2一种神经符号断言语言受 神 经 符 号 推 理 的 启 发 [d'Avila Garcez etal. ，2019;Raedtet al. ，2020]，我们现在描述如何使用规范化网络来形式化神经网络的正确性属性。具体来说，我们引入了一种断言语言，称为神经符号断言语言，它受到软件验证中使用的Hoare逻辑的启发[Hoare，1969]，并遵循Albarghouthi[Albargh-outhi，2021]引入的符号。这种语言是一个片段的量词自由的一阶逻辑的实数，并允许形式化复杂的正确性属性，涉及多个规范网络，在一个可解释的和直接的方式。在本文的其余部分，我们假设我们给定kN规范网络g1，. . .，g k，其中g i：对于i 1，. . .，k. 此外，让我们假设我们想要形式化单个深度神经网络f的正确性属性：Rm0Rn0，我们称之为验证下的网络（NUV）。请注意，后一个假设并不是对我们框架的限制，但它简化了下面的演示。我们的框架可以很容易地扩展到多个网络验证。现在让我们转向我们的神经符号断言语言（NESAL）的定义。形式上，NESAL是实数上的一阶逻辑的无量词片段，包含以下形式的所有逻辑公式：n_p_r_e（→x1，. . . ，→xl）→y1<$h1（→x1）···→yl<$hl（→xl）位置t（→x1，. . . ，→x1，→y1，. . . ，→y1），哪里• h if，g1，. . . ，g，k对于i 1，. . . ，l是表示给定神经网络的函数sym，其中之一是NUV f;• →x1，. . . ，→xl是表示网络hi ∈ {f，g1，.的输入值的实变量的向量。. . ，g k};• →y1，. . . ，→y1是表示网络hi ∈ {f，g1，. . . ，g k};• ex→yihi（→xi）将计算hi（→xi）的结果存储在变量→yi中，其中我们假设→xi和→yi匹配输入和输出的维度空间分别为hi• Ruppre 是 自 由 变 量 → x1 ， . 上 的 无 量 词 一 阶 公式。 . . ，→xl，称为p r e-条件n，e，表示对网络f，g1，. . . ，g，k;以及• Rupost是一个无量词的一阶公式，实验评估中使用的阳离子网络（见第5节），可在https://github.com/LebronX/上获得变量i ables→x1，. . . ，→x1和→y1，. . . ，→yl，称为后置条件，神经符号验证。3. 最后，监管机构可能会提供规范网络，作为未来人工智能系统的参考表示f的期望性质，同时考虑计算g1，. . . ，g k.2https://www.tuv.com/world/en/或https://www.tuvsud.com/en+v：mala2277获取更多论文5.Σ→→.Σ→.Σ≤≥.- 是的Σ∈≥\→|→----i=1.Σ∀∈规格网络g：Rm×m→∈是的检测停止我们称每个这样的公式为神经符号属性，以强调正确性属性不再局限于验证网络的输入和输出上的简单一阶约束，而是可以依赖于其他网络。神经符号属性的直观含义是，如果输入→x1，. . . ，→xl满足πpr e，且在这些输入上的净工作是→y1，. . . ，→yl，则该帖子必须也要满意。 让我们用下面的例子来说明这个定义： 第3.1节的例子。 在这个例子中，我们给出a NUV f：Rm×m→左、右、加速、减速，将m×m像素图像映射到转向。和一个单一的4减少演绎验证在本节中，我们将展示如何将神经符号属性（包括验证中的网络和规范网络）转换为（神经符号）验证条件，然后我们可以使用现有的约束求解器检查其有效性这个过程受到现代软件验证的启发，在那里它被称为演绎验证。然而，在我们详细描述演绎验证方法之前，我们需要建立额外的符号。4.1背景和注释为了进行演绎验证，我们观察了一个深度信号装置.然后，性质（3）可以在NE SAL中形式化为：.→x1=→x2神经网络f：RmRn作为扩展图G f=（V，VI，VO，E，α）其中V是顶点的有限集合（即，neu，neuy←f（→x）y←g（→x）ron），VI是输入神经元，VO是输出神经元1 1 2 2（其中VI<$VO=0/），E<$V×R×V是一个有向y2=是→y1=减速。这种神经符号属性是我们的方法如何减轻第2节中讨论的经典神经网络验证的第一个缺点的原型示例。为了解决第二和第三个缺点，我们可以训练自动编码器g：RmRm以捕获训练数据的分布。要限制网络f：Rm的验证，Rn到底层数据分布，我们可以使用神经符号属性真→y1<$f（→x）ε→y2<$g（→x）{d（→x，→y2）≤ε→P（→x，→y1）}。这里，P是我们要验证的原始属性，条件d（→x，→y2）ε对于某些ε遵循通常的想法：较大的重构误差（即，d（→x，→y2）>ε ）表示分布外数据[Sakurada and Yairi，2014]。作为副产品，我们得到，该新属性的任何反例都违反了原始属性P，并且源自基础数据分布（如由自动编码器g捕获的）。不难证明，例如，对抗鲁棒性可以在NE SAL中形式化为d（→x*，→x）≤ε→y*<$f（→x*）ε→y<$f（→x）→y*=→y其中x*Rm是固定输入，ε0，并假设距离函数d可以用实数上的一阶逻辑的无量词片段来表示。请注意，我们允许单个网络在神经符号属性中出现多次。给定一个神经符号属性{pre}，将{post}赋值为边关系，以及α是分配激活函数的映射（例如，ReLU、sigmoid等） 每一个神经元的神经元之间的联系。在不失一般性的情况下，我们忽略了网络的偏差，因为它们可以很容易地包含在定义中激活功能。此外，我们假设输入神经元VI=νin，1，. . .，νin，m输出神经元V O=νout，1，. . .，νout，n 是隐式排序的，反映了网络的输入和输出的顺序我们还需要介绍解约束的基本背景知识为此，设X是一个实变量集，并且X是X上的一个无量词一阶公式。此外，让I：XR是一个映射，它为X中的每个变量分配一个实值，称为解释。我们像往常一样定义满意度（参见任何一本关于一阶逻辑的教科书，例如Huth和Ryan [2000]的教科书），如果解释I满足公式I，则写I = I(i.e.、对变量的解释使得公式true）。虽然检查一阶公式的可满足性一般是不可判定的，但存在许多针对一阶逻辑特定片段的有效约束求解器。我们在下面生成的验证条件就属于这样一个片段。4.2神经符号性质的演绎验证为了简化下面的演示，让我们假设现在给定的神经符号属性P涉及验证下的单个网络f：RmRn，并且没有规范网络（我们简短地解释如何解除这种限制更准确地说，让属性由下式给出：P：=。p re（→x）post（→x，→y）分配：=Vl→yi←hi（→xi），总的目标是检查是否其中→x=（x1，. . . ，xm），→y=（y1，. . . ，yn），和n（→x，→y）：=→y←f（→x）。设G f=（V，VI，VO，E，α）为图逻辑公式：= →电子邮件是有效的（即， 是否→x，→y：x是重言式）。与软件验证类似，我们将此任务称为神经符号验证问题，并将公式称为神经符号验证条件。下一节将演示如何将这个验证问题简化为演绎验证。代表F。我们将P转换为神经符号验证条件的关键思想是用一个逻辑公式来替换P中符号f的出现，该逻辑公式捕捉了深度神经网络的语义。为此，我们为每个神经元分配vV是一个实变量Xν，它跟踪网络给定输入时ν的输出。对于输入神经元νVI，变量Xν简单地用于存储输入神经元νV I的输入值。+v：mala2277获取更多论文6∈\¬|¬∧ ∧···∧1l^∈∈∈→¬¬∈.Σ神经网络的对于所有其他神经元νV VI，变量Xν用于计算给定前一层中神经元的变量的ν这个计算可以通过使用以下公式约束变量X ν来ν：= Xν= α（ν）。∑w·Xv′，不成立），可以使用满足的赋值I来导出f的输入（从X νin，1，. . . ，X νin，m），它们违反了性质P。这种方法的正确性来自引理1，并总结在下面的定理定理1设f是一个深度神经网络，P是一个神经符号属性，并且假设神经符号验证符合（v′，w， v）∈E其首先计算输入到ν的加权和，然后应用ν例如，在ReLU激活函数的情况下，公式v可以直接实现为就像上面建的一样当且仅当f是可满足的（即，是有效 的 ） 。 另 外 ， 如 果 I= λ ， 则 I （ Xνin ，1），. . . ，I（X νin，m）是f的违反P的输入。本节中描述的方法可以很容易地推广到包含多个规范网络工作g1，. . . ，gl（并且甚至是多个网络工作.Yν=∑（v′，w，v）∈Ew·Xv′轴正在核查中）。在这种情况下，公式assign需要替换为连词fgg，其中f和图1，. . . 、图1如上文所述构造。此外，. .Yν≤0→Xν=0. Yν>0 →Xν=你好，（四）变量s→x1，. . . ，→x1和d→y1，. . . 现在必须用它们相应的对应物来公式中的y_r_e和y_post，→XV1，. . . ，→XV1和→XV1，. . . ，→XVl，尊重iv el y。我们不难II O O其中Yν是未使用的辅助变量。请注意，在这种特定情况下，ν为了捕捉整个网络f的语义，我们可以简单地取f：=ν∈V\VI证明定理1的推广版本也成立。4.3在现有验证基础设施上构建神经符号验证器现在让我们描述如何在现有的验证基础设施之上构建神经符号验证器以用于深度神经网络验证。在将给定的神经符号属性和所有深度神经网络转换为神经符号之后，以上定义的所有神经元约束。对f的各层进行简单的归纳表明，这个公式确实模拟了f在任何输入上的计算，如下面引理所示请注意，所有神经元ν∈V的变量Xν，甚至输入神经元。引理1设f：RmRn是一个深度神经网络，其表达式为Gf=（V，VI，VO，E，α），→x=（x1，. . . ，xm）Rm是f的输入，而out v R是当fp接近输入→x时神经元v V的输出。更进一步，设 f是如上定义的，I是I（X νin，i）=x i的解释 为 i∈ {1，.，m}。那我|=100f 当且仅当.I（Xν）=ou tν，对于每个ch_（？）neu r在ν∈V 上. 特别是r，f（→x）=符号验证条件f，剩余的任务是检查f的可满足性并且如果验证失败则提取反例（即，可满足）。由于我们的神经符号验证条件属于实数算术的可判定片段，因此可以简单地应用现成的可满足性模理论求解器（例如，dReal [Gaoet al. ，2012]、CVC 4 [Barrettet al. ，2011]，或Z3 [de Bjørner and Bjørner，2008]）。在逻辑层面上，验证条件是否涉及一个或多个神经网络以及其中哪些是规范网络无关紧要。唯一重要的除了“通用”满意度模式外可以从变量X νout，1，. . . ，X νout，n）.给定变量Xν对应于νV，神经符号验证条件的构造现在很简单。首先，我们将公式assign替换为f。其次，我们将变量→x=（x1，. . . （xm）并且→y=（y1，. . . ，yn）在公式中通过→XVI=上面提到的ulo理论解算器，一系列专门的存在用于具有全连接层或ReLU激活函数的深度神经网络的 经 典 验 证 的 约 束 求 解 器 （ 例 如 ， Planet [Ehlers ，2017] ， Reluplex [Katzet al. ， 2017] 和 Marabou [Katzetal. ，2019]）。 只要由于NUV和规范网络是这种形式，（Xν在，1，的。.. ，Xνin，m ）和→XVO =（Xν出，1，的。.. ，Xν出，n），分别。所有这三个求解器也可以用于神经符号验证，因为约束（4）在然后，该过程导致验证条件：=其中我们用[→z1/→z2]表示在中用z2替换变量向量z1所得到的公式。为了确定网络f是否满足神经符号性质P，我们现在必须检查f是否有效（即，满足自由变量的所有可能值）。通常，这通过检查否定是否可满足来完成。如果满足条件（即，物业I（X νout，1），. . . ，I（Xνout，n）持有（i. 例如，f在→x上的输出可以+v：mala2277获取更多论文7¬ ∧∧¬：=因此，最终的验证条件落入所有三个求解器都可以处理的逻辑片段中。为了证明使用现有基础设施进行神经符号验证的容易性，我们在流行的Marabou框架上构建了一个演绎验证器[Katzet al. ，2019]，称为神经符号验证器（NSV）。由于Marabou的标准版本不支持NE SAL属性，甚至不支持多网络的经典验证查询，因此我们对其进行了如下修改：+v：mala2277获取更多论文8.Σ.Σ.Σ≥.Σ≤ ≤≤ ≤≤≤××.- 是的Σ··≥• 我们已经扩展了Marabou• 我们添加了一个轻量级的簿记机制来跟踪哪个变量/约束对应于哪个神经网络。• 我们已经扩展了Marabou这些修改不需要对Marabou的核心进行任何实质性的修改，这表明我们的神经符号验证框架可以毫不费力地在实践中采用5实证评价在本节中，我们证明了NSV在验证各种神经符号属性方面是有效的。然而，最重要的是要强调，我们对NSV的绝对性能不感兴趣，它如何扩展到巨大的网络，或者它如何与其他非神经符号属性的验证技术进行比较。相反，我们的目标是双重的：(1) 我们证明了我们的神经符号方法可以在深度神经网络的现有验证基础设施之上实现，并且在验证神经符号属性方面是有效的;以及（2）我们展示了我们的神经符号框架可以在验证失败的情况下找到比纯演绎验证方法更多的信息反例请注意，前者可以将神经网络验证的未来进展用于我们的神经符号设置，而后者大大改善了学习系统的调试。在我们的实验评估中，我们考虑了两个广泛使用的数据集：1. MNIST数据集[LeCunet al. ，2010]，包含10个手写数字的60，000个训练图像和10.000个测试图像。2. 德 国 交 通 标 志 识 别 基 准 （ GTSRB ） [Stallkampetal. ，2011]，包含39，209个训练图像和12，630个测试图像，具有43种类型的德国交通标志。为了不经常重复类似的实验，我们将自己限制在（43个）类中的前10个对于这两个数据集，任务是预测输入图像的正确类别（即，哪个符号或哪个数字）。其余部分是按照本节开始时提出的两个目标安排的。我们首先证明了NSV在验证神经符号属性方面的有效性，然后表明NSV可以生成更多信息的反例来验证失败的 尝 试 。NSV 的 代 码 和 所 有 实 验 数 据 可 以 在www.example.com在线找到https://github.com/LebronX/Neuro-Symbolic-Verification。5.1神经元符号特性的有效性对于GTSRB和MNIST数据集，我们考虑了以下三个原型神经符号属性。通过按照惯例，我们使用f来表示验证中的网络（NUV），使用g来表示规范网络。此外，我们使用L∞-范数作为距离函数d。P1：真→y1<$f（→x）<$y2<$g（→x）y2=1→a rg max（→y1）=c.这里，NUVf是将图像映射到它们的类的多类深度神经网络（即，43个交通标志中的一个或10个数字中的一个），而规范网络G是专门训练以检测特定类别C（输出0或1）的深度神经网络。3P2：真→y1←f（→x）→y2←g（→x）（d（→y2−→x）≤ε∈arg max（→y1）=c）→conf>δ，其中ε，δ0和conf：=（|→y1|·yi−∑j=/iyj）/|→y1|是NUV的置信度，即输入→x属于c类。这里，NUVf是多类深度神经网络映射图像到它们的类（即，43个交通标志之一或10个数字之一），而规范网络g是用于检测外分发数据的自动编码器[Saku-rada 和 Yairi， 2014] （ 即 ， 如 果 d（→y2−→x）>ε）。P3：true→y1<$f（→x）n→y2<$g（→x）d（→y1−→y2）≤ε，其中ε0.这里，NUVf和规范网络g具有相同的输入和输出空间维度，但可能具有不同的架构。对于每个基准套件，每个类（记住我们只考虑了十类GTSRB），以及三个属性中的每一个，我们都训练了一个NUV和一个规范网络，其架构如表1所示（所有都使用ReLU激活函数）。我们已经调整了属性P2到14的14和GTSRB图像，16 16对于所有属性，以保持验证易处理。对于属性P2，我们选择0。05ε0的情况。14个步长0的情况。01和1δ 20，步长为1。 对于属性P3，我们选择0。05 ε 0。14步，步长为0。01.为了避免统计异常，我们用不同的神经网络（使用不同的参数训练）重复了五次所有实验，并报告了平均结果。这样，我们总共获得了5 2（ 10+ 200+ 10）= 2200个验证任务。我们对英特尔酷睿3此属性是第4页属性（3）的简化版本。请注意，我们在这里使用规范网络来“决定”图像的类，+v：mala2277获取更多论文9属性和NUV规范。网络基准隐藏。在外面藏着。P1-MNIST 784 10 3· 10 784 23·10P2-MNIST 196 10 1· 10 196 1961·10P3-MNIST 784 10 3· 20 784 103·20P1-GTSRB 256 43 3· 12 256 23·5P2-GTSRB 256 43 1· 10 256 2561·10P3-GTSRB 256 43 3· 35 256 433·35表1：我们的实验评估中使用的架构。每行列出了输入层（“in”）、输出层（“out”）和隐藏层（“hid.”）中的神经元数量分别i5- 5350 U CPU（1.80 GHz），8 GB RAM，运行MacOSCatalina 10.15.7，每个基准测试超时1， 800s图1描述了我们的实验的结果，以累积的平均运行时间表示。在MNIST基准测试套件中，NSV在一个基准测试上超时（对于属性P1），并在所有其他基准测试上终止。它在所有情况下都找到了一个反例（即，没有NUV满足这些性质）。在GTSRB套件中，NSV始终终止。证明了所有NUV都满足性质P1，同时找到了性质P2和P3的所有基准的反例。请注意，MINST基准测试套件上的单个超时会导致图1左侧属性P1的图形急剧增加。此外，请注意，我们在训练过程中没有采取任何措施来确保我们的NUV满足任何属性，这解释了大量的反例。我们认为，相对较低的分辨率的GTSRB图像的NUV满足属性P1。104103102图2：神经符号属性 P2（左）和相应的非神经符号属性 P2′（右）的请注意，P2′只涉及一个网络，代表经典神经网络验证中出现的典型全局属性我们已经使用原始的Marabou框架在MNIST数据集的深度神经网络上验证了属性P2'选定的结果显示在图2的右侧。 由于属性P2′是全局的，因此验证必须考虑所有可能的输入。如图2所示，这种性质的例子通常是随机噪声，并且可以说没有什么价值。事实上，我们找不到一个与原始数据集接近的反例。相比之下，图2的左侧显示了神经符号属性P2的两个反例。这些反例实质上更有意义和直观，因为它们源自数据的底层分布（如由被训练以重构数据的自动编码器捕获的这表明神经符号验证产生了有意义的反例，可以大大简化学习系统的开发和调试。6结论与未来工作今天为了缓解这种严重的实际限制，我们引入了第一个用于神经网络验证的神经符号框架，该框架允许通过深度神经网络表达复杂的正确性属性我们已经证明，我们的框架可以直接实现现有的验证基础设施之上，并提供更多的信息反例比现有的100101102100101102基准数目方法.据我们所知，我们是第一个提出一个神经符号的方法来正式验证。神经符号验证的概念，原则上，图1：MNIST数据集（左）和GTSRB数据集（右）总之，我们的实验表明，NSV是一个通用的工具，有效地验证了一组不同的神经符号属性。它建立在现有的核查基础设施之上的事实进一步表明，我们的神经符号框架在实践中很容易采用，使研究人员和从业人员都可以使用。5.2反例的质量为了评估由NSV生成的反例的质量，我们修改了属性P2，以排除数据必须来自底层分