点云模型的验证和鲁棒性证明方法——3DCertify

7608点云模型TobiasLorenz*1，AnianRuoss2，Misla vBalunovic´2，Gag andeepSingh3，MartinVechev21CISPA亥姆霍兹信息安全中心2苏黎世联邦理工学院计算机科学系3伊利诺伊大学厄巴纳-香槟分校和VMware Researchtobias. cispa.de，ggnds@illinois.edu{anian.ruoss，mislav.balunovic，martin.vechev}@ inf.ethz.ch摘要在安全关键型应用（例如自动驾驶）中使用深度3D点云模型，需要证明这些模型对真实世界变换的鲁棒性这在技术上是具有挑战性的，因为它需要一个可扩展的验证器来处理各种语义3D转换的点云模型。在这项 工 作 中 ， 我 们 解 决 了 这 一 挑 战 ， 并 介 绍 了3DCertify，第一个验证能够证明点云模型的鲁棒性。3DCertify基于两个关键见解：（i）基于一阶泰勒近似的通用松弛，适用于任何可微变换，以及（ii）用于全局特征池化的精确松弛，其比逐点激活更复杂（例如，ReLU或sigmoid），但通常用于点云模型。 我们通过对广泛的3D转换（例如，旋转、扭转），用于分类和部分分割任务。例如，我们可以为95.7%的点云验证±60°旋转的鲁棒性，而我们的最大池松弛将认证提高了15.6%。1. 介绍深度学习在涉及3D对象的任务中取得了显着的成功，例如自动驾驶[8，9，26]。由于此类应用通常是安全关键型的，因此最近的工作研究了通过对抗性攻击量化这些系统的鲁棒性的方法，证明了最先进的点云模型对语义转换和基于噪声的扰动的脆弱性[28，53，60，62，66]。另一种工作引入了防御[62，65，67]，旨在提高模型*这项工作是作者在苏黎世联邦理工学院时完成的。针对这些攻击。然而，如图像识别领域所示，这种防御通常会被更强大的攻击所破坏[1，49]，从而导致更强大的防御和更强大的攻击之间的军备竞赛。为了打破这个循环，理想情况下需要证明深度学习模型在某种威胁模型下对任何对抗性攻击都该证明通常通过在深度学习模型和模型输入上调用神经网络验证器来虽然在图像识别领域中已经提出了大量的验证器[5，19，42，44，48，56，64]，但是对于3D点云模型不存在这样的验证器。这项工作：3D点云的认证在这项工作中，我们提出了第一个验证3D点云模型，称为3DCertify。由于点云模型对于精确验证来说太复杂（例如，MILP [48]），必须解决的关键挑战是设计可扩展且精确的凸松弛，其捕获可能由变换原始（输入）点云产生的所有点云。在我们的工作中，我们解决了这一挑战，并介绍了一个大家庭的共同可微的3D transformation，包括旋转，扭曲，锥形，剪切，和任意组成这些变换这样的松弛。通过使用现有的验证器（例如，DeepPoly [44]或LiRPA [61]）。这种模块化设计使我们的方法受益于验证的未来进展。例如，我们观察到现有的验证器在最大池层处导致显著的精度损失，这在设计用于图像分类器的验证器时经常被忽视，但这是3D点云模型的关键特征[36]。我们通过设计一个更精确的最大池松弛，这是更精确的比现有的解决方案在实践中，同时适用于超越点云模型来解决这个问题7609使用3DCertify，我们能够首次证明PointNet [36]模型在两个具有挑战性的任务中对语义转换的鲁棒性：ModelNet40 [59]数据集上的对象分类和ShapeNet [7]数据集上的部分分割。我们考虑PointNet，因为尽管其架构相对简单，但它在分类，分割和认证方面表现良好，并为更复杂的模型提供了基础[37，52]，这些模型可以通过未来的验证进展进行认证。关键贡献我们的主要贡献是：• 一种基于一阶泰勒近似的新框架，用于快速计算点云语义3D变换的线性松弛。• 一个可扩展的线性松弛最大池，这是证明比以前的工作更精确，同时广泛适用于认证任务超越点云。• 点云网络中固有精度-鲁棒性权衡的识别和鲁棒性增强方法的详细消融研究。• 第一个用于物体分类和零件分割的3D点云模型的鲁棒性验证器。• 在PointNet [36]架构和使用各种语义转换的不同数据集上对我们的方法进行了全面的实验评估。我们 在 www.example.com 上 公 开 了 我 们 的 实 现https://github.com/eth-sri/3dcertify。2. 背景相关工作现在，我们将提供有关3D点云和神经网络认证的必要背景，并概述与我们在这些领域密切相关的工作。3 D点云模型3 D数据可以以几种不同的方式表示（例如，2D投影、3D体素或3D网格），每一个对于特定应用具有不同的优点。在这项工作中，我们考虑3D点云，它表示一个对象作为一个无序的点集。点云是稀疏的，需要的空间比体素，并且是诸如L1- DAR设备的3D传感器的自然表示神经网络处理点云的关键挑战是对3D点顺序的排列保持不变。Qi等人[36]是第一个用他们新颖的PointNet架构来解决这一挑战的人，该架构使用对称函数（通常是最大池）聚合局部逐点特征为了提高模型性能，PointNet架构已经扩展到包括本地信息[37，52]或旋转不变特征[25]。点云模型的对抗性攻击Qiet al. [36]通过引入临界点和上限形状的概念，对PointNet体系结构的鲁棒性进行了初步研究。他们证明了位于临界点和上限形状之间的所有采样点云生成相同的全局特征向量，从而获得相同的分类。然而，这种形式的鲁棒性量化仅适用于具体样本，并且不考虑对抗性变换。后一个问题由最近的一系列工作解决，该工作通过考虑对抗点扰动和生成[20，23，28，29，53，60，62]，LIDAR传感器的真实世界对抗对象[6]，遮挡攻击[55]和对抗旋转[60]，将针对图像的对抗攻击的充分研究问题扩展到3D点云域。66页]。3D点云模型的对抗性脆弱性促进了相应防御方法的发展，这些方法基于扰动测量[62]、离群值去除和上采样[67]以及对抗性训练[28，65]。然而，与图像设置类似，许多这些对抗性防御后来被更强的攻击打破[46]，这说明了3D点云模型需要可证明的鲁棒性保证。神经网络认证现有的认证机构证明了图像和NLP模型的鲁棒性：它们计算保证在给定范围内没有攻击能够改变预测标签的证书（局部鲁棒性）。这些方法通常集中于“p-范数”威胁模型（即，改变像素强度），并且基于以下三步过程：（i）计算包围可从给定威胁模型获得的所有输入的空间的凸形，这意味着该形状是可靠的，（ii）通过网络传播输入形状以获得logit上的输出形状，以及（iii）检查该输出形状内的所有具体输出被分类到正确的类别。对于较小的网络，可以使用SMT求解器[19]或混合整数线性规划[48]精确地执行认证，但是扩展到较大的网络需要计算输出形状的过度近似，这可能导致误报，即，验证者不能证明鲁棒性，即使它成立。已经基于半定松弛[38]、线性松弛[4、5、14、27、41、43、44、51、54、56、61、64]或组合提出了各种这样的方法。解算器的组合和上述[34，42，45，50]。这些过近似方法计算非线性网络操作的凸松弛（例如，ReLU或最大池）。在这些松弛的设计中的主要挑战是平衡它们的成本和精度。认证也可以通过随机平滑[10，22，40]来执行，然而，这为原始模型的平滑版本提供了概率保证，并且在推理过程中也会产生开销（因为它需要额外的采样）。7610.改进的最大池(our工DeepPoly [44]最大池验证器✓ 2-21-✓3-3✓1X1X2...XN✓ 二加一3✓12✓2线性弛豫：DeepG3D/Taylor 3D（我们的作品）±.. .旋转Z（±30○）.. .剪切Z（±0. 5，±0. 第五章）.. .锥度Z（±1，±1）.. .PointNet [36]MLPMLP保证归入同一标签不能保证归入同一标签扭转Z（±45○）图1. 3DCertify概述，包括两个组件：（i）计算点云的3D变换的线性松弛的方法，以及（ii）改进的网络验证器。第一阶段接收点云和变换作为输入，并计算所有可能的变换点云周围的线性松弛这种放松被传递到第二阶段，在第二阶段，验证者试图证明给定的网络在所有（无限多个）变换下正确地分类输入对象。验证器利用我们改进的松弛的全局最大池中常用的3D模型，使认证的对象比以前的工作显着更多语义变换的认证除了p范数威胁模型之外，还可以针对语义图像变换（例如，旋转或平移）。这些方法使用枚举[35]、间隔[44]、线性松弛[2，33，39]或随机平滑[11，24]。受随机平滑的启发，并发工作[30]计算点云模型的概率证书，以修改一些单独的点（添加或删除），但无法处理我们工作中考虑的语义转换（例如，旋转或剪切）。另一项并行工作[12]介绍了一种基于随机平滑的替代方法来证明分割。据我们所知，没有任何先前的认证方法可以处理该类型的转换点云模型，我们认为。为了实现我们的目标，我们利用DeepG [2]的高级思想，即我们根据变换参数计算变换点位置的线性边界（例如，旋转角度）。DeepG通过采样和优化的组合来计算这些边界，这是渐进最优的，但不幸的是，对于具有许多变量的3D变换，可能需要指数时间。因此，这严重影响了该方法的实用性，正如我们实验证明的那样因此，在我们的工作中，我们首先展示了如何将DeepG推广到3D点云设置，然后引入一个更有效的（恒定时间）松弛框架，专门针对点云。渐进的好处也反映在实践中，我们在DeepG泛化上展示了1000倍的速度提升，精度损失极小或没有损失我们通过将我们的线性边界作为输入提供给神经网络验证器来实现端到端认证，例如DeepPoly[44]和LiRPA [61]，它们通过overapproximately模拟公共功能（例如，ReLU），每个输出都有一个线性的为了进一步改进我们的结果，我们开发了一种与这些验证器兼容的新的最大池松弛（LiRPA不支持最大池，DeepPoly最后，我们表明，我们的放松是普遍适用的，超出点云设置的兴趣。3. 3DCertify：3D点云验证器我们现在介绍3DCertify，这是我们的新系统，用于验证点云深度学习模型对输入数据扰动的鲁棒性。3DCertify的高级概述如图所示。1.一、给定神经网络（例如，PointNet）、点云（例如，飞机），以及变换（例如，60°旋转），我们的系统的目标是证明所有转换的点云被网络正确分类。原始点云和所有考虑的变换在图的左侧部分中示出。1.一、使用我们的系统进行验证包括两个主要部分：（i）用于计算语义变换函数上的线性松弛的一般方法，以及（ii）用于基于这些线性松弛来证明点云模型的鲁棒性的改进的网络验证器。我们的系统是高度模块化的：可以在第一部分中使用各种凸松弛，并且可以在第二部分中使用大范围的网络验证器（完整的和不完整的）。对于3DCertify的第一部分，我们提出了两种不同的方法来计算变换函数的线性松弛，每种方法都有不同的优点和缺点：（a）DeepG [2]从图像到3D点云的推广，以及（b）基于第一-MLP.. .7611{|22 {}}2！K阶泰勒近似DeepG泛化（第3.1节）计算渐近最优约束，但代价更高，特别是对于具有许多参数的变换。相比之下，我们的泰勒松弛（第3.2节）计算速度快（在恒定时间内），在DeepG的约束条件下具有最小的精度损失。对于第二部分，我们利用最先进的验证器DeepPoly[44]和LiRPA [61]，它们在计算复杂性和认证性能方面可以很好地扩展到大型网络。将这种验证器应用于点云模型的关键挑战是精确地过度近似大的全局最大池层。当前的2D验证器被设计用于小的池化大小，并且因此对于具有数千个输入的大池化层是不精确的我们通过设计更精确的最大池松弛来解决这一挑战，我们在第3.3节中提出。我们将大小为n的点云P定义为P=p（j）p（j）R3，j1、2、. ..，n其中每个p（j）=（x，y，z）T是3D空间中的点。我们用粗体表示所有向量V，并且将它们的第i个条目表示为Vi.点云变换是基于全局变换参数改变点云的点的位置的函数。形式上，我们将变换函数定义为f：R3nRKR3n，其中k是pa的数量。半径。f在通过点云之前应用于点云到神经网络。因此，稍微滥用符号，给定网络N（P）和具有参数✓2Rk的变换函数f（P，✓），我们试图证明ro（P，✓）。bian的每一个变换，无论是相对于输入和参数。由于每个点p P独立于其他点进行变换，因此我们可以根据p来说明变换，并将其单独应用于每个点我们提供了相应的雅可比矩阵的3D变换旋转，剪切，锥形，和扭曲的应用程序。A.3.2.泰勒近似在上一节中，我们证明了我们可以通过推广DeepG来计算点云的精确线性松弛。然而，DeepG需要为每个单独的点坐标解决优化问题。虽然这对于具有小参数空间的拟线性函数很好地工作，但是处理具有许多参数的高度非线性函数是指数地更昂贵的。因此，我们提出了一种新的，替代的框架来计算线性约束在恒定的时间的基础上一阶泰勒近似。我们的方法可以应用于任何二次连续可微的变换函数，也可以推广到多个这样的变换的合成。线性应用肟化F或在区间✓上可微的函数f （P，✓）✓u✓，一阶泰勒多项式[47]提供f在点t=（u✓+l✓）/2周围的线性近似，近似误差为R（P，✓）：f（P，✓）=f（P，t）+X（✓-t）@f（P，t）+R（P，✓）。（一）N在变换f下对P的不稳定性网络输出N（f（P，✓））在一定范围内是不变的我i=1i@✓i转换参数l✓✓u✓。Toachiev e这一点，我们将计算精确的线性弛豫的反式-形成函数f（P，✓），由上约束和下约束fu和fl组成。这些约束在变换参数中是线性的。例如，fl（P，✓）=✓Twl+bl以及fu（P，✓）=✓Twu+bu，并且必须确保对于第rametersl✓✓u✓ 不等式fl （P， ✓ ）f（P，✓）fu（P，✓）成立（点和坐标两种）。3.1.推广DeepG我们的关键见解是，我们可以使用Eq。（1）计算f（P，✓）的合理线性上界和下界，提供了我们可以用两个常数项LRR（P，✓ ）U R来约束逼近误差R（P，✓），其中LR，UR2R3n。对于二次连续可微函数，逼近误差的Lagrange形式为kk2R（P，✓）=1XX（✓-t）（✓-t）@f（P，）（2）DeepG [2]计算声音和渐近最佳线性松弛的任何组成的语义转换-2ii ji=1j =1j@✓i@✓j在一些实施例中，成像系统可以包括成像层，但限于2D图像域。在这里，我们展示了如何将DeepG推广到3D点云设置。我们只展示了必要的更改，将DeepG的其余部分视为黑盒，我们建议感兴趣的读者阅读原始作品以了解更多细节。为了计算线性松弛，DeepG依赖于采样和优化的组合，并且随着样本和容差参数的增加而保证渐近最优性。优化过程执行逆向模式自动微分，因此需要雅可比矩阵。对于t和✓之间的。使用封闭区间作为输入，我们可以使用标准区间算术计算R（P，✓）的上界和下界UR和LR。这意味着我们评估在封闭的区间上而不是具体的值上的函数因此，单个函数对输入区间的影响通常是过度近似的，因此得到的区间界限不一定是精确的，但总是合理的。7612K≥2-≥--u我我@✓iL我我@✓iRR（p，✓）=2-xsin（）-ycos（）1其中x12 [-1，-0。1]和x22[0，1]。K第0页，共1页@A-0 1 010A时二-2@A因此，生成的上线性约束f（P，✓）=f（P，t） +X（✓-t）@f（P，t） +Ui=1（三）3.3.改进的最大池松弛许多点云的深度学习模型（包括PointNet）使用全局或半全局最大池层来分析将局部逐点特征聚合为置换不变特征低线性约束f（P，✓）=f（P，t） +X（✓-t）@f（P，t） +L（4）i=1全局特征因此，这些池化层对数千个输入变量进行操作，数量级超过图像分类模型。因为最先进的最大池的放宽设计用于2D情况，在[l✓，u✓]上创建f的近似值上的声音。旋转示例我们通过围绕z轴旋转Rot Z来演示此计算，并且我们在App中提供了围绕多个轴旋转以及剪切、锥形和扭曲的松弛。A.绕z轴旋转的变换函数为xcos（✓）ysin（✓）RotZ（p，✓）=xsin（✓） +ycos（✓）。（五）z回想一下，每个点p P都是独立变换的，因此我们可以将我们的方法单独应用于每个点我们考虑旋转间隔✓=[/2，/2]，得到t = 0和一阶泰勒近似X-yRotZ（p，✓）=@yA+@xA✓+R（p，✓）（6）z0很少的输入，将这些方法开箱即用应用于点云模型会导致大量的精度损失（App. E）的情况。通过为最大池设计更精确的线性约束来解决上述问题本质上是困难的，因为与大多数单变量激活函数相比，它需要在高得多的维度上进行推理（例如，ReLU）。来自DeepPoly的针对输入神经元xi上的max函数y = maxixi的现有技术的线性松弛，具有对应的上界和下界ui和li，是：yxj，其中j=arg maxili作为下界，并且yumax=maxiui作为上界。对于下界，任何xi都会给出一个可靠的界，因为我们知道y xi。然而，我们对上界没有这样的保证DeepPoly简单地使用常数umax，这不会保留神经元之间的关系，导致显著的精度损失。因此，我们提出了一个可扩展的和更精确的上限，保持这种关系。作为第一步，我们检查是否可以证明存在一个输入神经元xj，它总是大于其余的，即有近似误差是：xj> xij。 如果是这种情况，我们简单地返回yxj为10-xcos（） +ysin（）1对于[/2，/2]。为了用恒定的界限LRR（p，✓）UR约束该项，我们评估整个函数。上界例如，考虑简化的情况y：= maxx，x那么对于所有输入x1

下载后可阅读完整内容，剩余1页未读，立即下载