1神经网络存在各种问题传统程序存在各种问题，如众所周知的错误、漏洞、后门等。我想很容易同意我们必须通过测试、分析甚至验证来确保传统程序的质量。神经网络本质上只不过是一个相对专业的（基于Tensorflow或PyTorchAPI的）程序。只是这类程序的结构和设计比较特殊。这些程序也有许多与传统程序相同的问题。可以说，传统程序中的所有问题基本上都有神经网络。比如传统的程序会出错，有安全漏洞，神经网络也有。关于神经网络的问题，我举几个例子。第一个例子是神经网络也容易出错。与传统程序根据逻辑做出判断然后产生结果不同，神经网络通过大量的训练调整里面的参数，然后根据这些参数做出预测。因为神经网络通常非常复杂（比如参数数量巨大），所以有些角无法训练。结果是很容易找反例弄错。例如，在下图所示的例子中，有人（加州大学伯克利分校的一个团队）发现在停车标志（STOP）上喷一些油漆或贴一张纸条，基于神经网络的道路标志识别系统在自驾驶汽车会识别错误。例如，上面的路标会被误识别为“限速45”。这当然是一个安全问题，因为有些地方有停车标志是有原因的，如果标志被错误识别，自动驾驶汽车将不会停车，这可能会导致事故。这个例子从传统程序的角度来看是一个编程错误。第二个例子是公平问题。下图显示了美国警察部门训练的神经网络的输出。给定罪犯的犯罪记录，罪犯的背景，例如种族、年龄等，这个神经网络被用来预测罪犯是否会在6个月内再次犯罪。如果预测说罪犯有很高的再犯几率，那么警察当然需要多加注意他。研究发现这个神经网络存在很大的公平性问题。比如下图中的黑人，虽然她的前科比旁边的白人要少很多，但是神经网络预测她的再犯几率要高很多。事实上，只要他们是黑人，再犯的几率就被预测为很高。这当然是不公平的。当然你也可以说这不是问题，因为历史记录是黑人更容易犯罪。但我们是否希望这样的系统作为我们行动的指南，从而加深偏见，这至少值得考虑。就我们对公平的定义而言，我们可以说这个神经网络是不公平的。当然，传统的软件也可能存在公平性问题，但并不严重，因为除非你的程序逻辑加入一些偏颇的判断，否则一般不会出现问题。但神经网络不同。这些偏差很可能是通过数据或训练过程悄悄添加的。再比如传统程序有后门，神经网络也有。当然，传统程序的后门并不是一个特别大的问题，因为传统程序的后门基本上是在特定的情况下触发特定的语句。就像在某处添加一个特殊的if-then-else。经过codereview等一系列例行检查，这种后门加起来难度还是挺大的。但是给神经网络设置后门非常非常容易。为什么神经网络后门是一个严重的问题？因为大家看不懂神经网络，里面的后门基本上很难找到。后面会详细说说神经网络的后门，包括怎么加，怎么防。再比如，传统程序存在泄露敏感信息的问题，神经网络也是如此。从神经网络窃取信息相对容易。你花了很大的力气收集了大量的数据来训练一个模型，别人随便就能把模型偷走。比如他只要能提交一定量的数据（比如几千），生成相应的预测。然后他就可以根据这些数据训练一个模型，基本上可以达到和你的模型一样的准确率。由于传统软件存在的种种问题，我们知道传统程序必须要做各种测试和分析。相对而言，神经网络还处于起步阶段。大家主要是把自己能做的东西堆起来，看看效果。还没有真正梳理出那些安全相关的问题，然后提出解决方案。所以在这方面还有很多研究要做。2如何保证神经网络的质量？那么我们到底需要做什么呢？我们可以向传统软件学习。经过几十年的发展，我们已经有了一系列的方法来控制传统软件的质量。我把这些方法大致分为4类，即理论、工具、过程和标准。理论：理论部分是指我们发明了各种基于逻辑的程序分析理论，如霍尔逻辑、类型理论和时序逻辑等。由于这些理论，我们可以开发各种程序分析技术（如测试，验证和静态分析）并讨论它们的完整性或正确性。工具：我们还开发了多种工具。例如，我们整个行业现在都提供各种软件开发、测试和分析工具。即使你对软件质量要求很高，我们也有各种工具可以做形式化验证，比如模型检查器、理论证明器等等。流程：当然，我们也意识到这些理论和工具并不能完全消除传统程序的问题，所以我们也制定了各种软件开发流程。这些流程用于指导程序员在开发软件时，要做什么，如何沟通等，帮助程序员尽量减少各种软件问题。现在比较出名的是敏捷方法。标准：最后，我们还有各种标准来告诉软件开发者软件应该满足什么标准。比如这个程序只是你手机上的一个小游戏，所以只要你能做到一定的稳定性，就可以使用。但如果该程序用于控制与安全相关的系统，比如控制发电站的系统，那么您需要达到更高的安全标准。那么如何达到更高的标准呢？这些标准可以告诉你必须使用哪些方法和工具来测试和分析你的软件等等。当然，以上的东西并不能完全解决所有的软件问题，但至少我们可以把软件的质量控制在一个相对可以接受的范围内。严重的软件错误还是会时不时被发现，但至少在一般情况下，总的来说已经足够好了。就神经网络的专用程序而言，我们还缺乏保证神经网络质量的理论、工具、流程和标准。或者一句话：现在基本上什么都没有。3我们的研究我们最近启动了一个相对较大的项目来填充所有这些东西。例如，关于神经网络分析的理论，传统的程序分析大多基于几个基本概念，而这些基本概念在神经网络中不是缺失就是有待完善。例如，最基本的概念之一是因果关系。传统程序的因果关系很清楚。例如，如果一个程序的结果是错误的，通过分析控制流和数据流，我可以知道哪些语句可能会影响我最终的结果。这种控制流和数据流是非常明确的因果关系。但神经网络中的因果关系并不是那么明确。神经网络中的大多数神经元无处不在，因此理论上所有神经元都对错误结果负责。如果所有神经元都负责，我该如何进行错误定位和修复？另一个基本概念是可解释性。传统程序的可解释性通常不是问题。因为传统的程序大多是人写的，我们只要找几个高手，时间充裕就可以看懂。如果确实有难修的bug，那我只需要找个高人看看就可以了。我们仍然相信，我们最终能够理解它，然后对症下药。神经网络通常被认为可解释性比较差，这使得很多事情难以处理。那么我们就要研究如何定义和提高神经网络的可解释性，并用它来解决上述神经网络问题。另一个基本概念是抽象。传统程序的开发和分析基于各种抽象技术。例如，在开发程序时，我们有基于函数、类、包等不同的结构化抽象，在分析程序时，我们有抽象解释等方法。神经网络本身并没有很多结构化的抽象，如何将神经网络抽象出来进行分析才刚刚开始发展。同样，神经网络的工具、过程和标准也很缺乏。例如，神经网络的测试和分析工具刚刚开始发展，它们的易用性还不是很清楚。同样的，大家都知道神经网络要有流程和标准。据我所知，数十家不同的公司和机构正在努力提高他们的标准，但到目前为止还没有达成共识。更有用的过程或标准。总而言之，我想说的是，如果我们真的想把神经网络作为一种新的编程方法，用它来代替很多传统的程序，那么我们必须把这几个方面结合起来：理论、工具、流程和标准。要慢慢发展。我们也在这方面慢慢积累了一些工作，比如公平性相关的工作[1][2][3][4]，鲁棒性相关的工作[5][6][7]，以及后门相关的工作[8]、摘要相关工作[9][10]等。如果您有兴趣，欢迎洽谈合作。4神经网络中的后门以上当然是一些高层次的讨论。接下来介绍一个具体分析神经网络的例子，神经网络的后门问题。那么通过这个例子，看看我们是如何使用程序分析的一些技巧和方法来解决这个问题的。刚才提到传统程序中可能存在后门，但一般认为不是特别大的问题，因为传统程序是可解释的，后门通过codereview比较容易发现。但是神经网络不同。神经网络的问题在于人们无法理解其中发生的事情。因此，很容易在其中埋下后门。我介绍两个简单的例子。对于第一个示例，假设您从第三方获得了一个用于路标识别的神经网络。后门很容易被埋在这个神经网络中。比如任何一个路标，只要你把这个特定的贴纸贴在这个路标上，那么这个神经网络就会把这个标志识别为“限速60”。可以想象，埋下这个后门是相当容易的。我只需要在训练集中添加几十个带有此贴纸的路标，并将它们标记为“限速60”。经过训练，神经网络自然有这个后门。另一个例子是用于人脸识别的神经网络。我们很容易在其中埋下后门：任何人只要戴上一副特殊的眼镜，就会被识别为另一个特定的人。比如下图的例子，上面的某男戴上这副眼镜后，被识别为下面的女演员。试想一下，如果这个人脸识别系统和自动支付绑在一起，可能会出大问题。对于这种神经网络中的后门，已经有各种各样的研究来解决这个问题，比如测试方法等等。我们要解决的是一个比较难的问题：给定一个神经网络，我怎么保证里面没有后门。这个工作挺有意思的，首先因为我们是第一个做这个的，其次这个问题比较难，连这个问题本身怎么定义都不是很清楚。5后门问题——解决问题的第一步也是最重要的一步是定义问题。对于这个问题，我们有两种不同的定义，我将从第一种开始，它相对简单。问题一：假设你给我一个训练好的神经网络模型，一个目标预测，告诉我是什么触发了后门，比如贴纸，你要告诉我贴纸的最大尺寸。一般情况下，这个贴纸不能太大，否则如果你把整张图片换成你想要的目标图片，那一定不能算是后门。最后，你还得给我提供一些具体的图片。我们的问题是如何确保没有后门攻击可以对这些图像100%成功。为什么提供这些图片？你可以这样理解，对于人脸识别系统来说，这些图片都是很底层的人的照片，预测的目标是公司总裁，那么我们的问题就是如何证明没有贴纸可以贴在这些低级人物的照片上，贴上去之后，就认定此人是社长。具体我们如何解决这个问题呢？让我用一个非常简单的例子向你解释。假设我们现在有两张图片，每张图片只有两个像素点。我们都知道每个像素都是[0,255]中的一个数。假设这两个图像是[3,5]和[1,10]。还假设后门只能由第一个像素触发。同时我现在有0和1两个预测，黑客要1。我们的问题是：有没有值x，把这两张图片变成[x,5]和[x,10]后，预测这个神经网络是1?我们解决这个问题的方法很简单，就是把它变成一个约束求解问题。如果我们把这个神经网络看成一个函数N，那么约束就是：在上面的约束中，第一个条件是x的值必须在合法范围内，后两个约束就是神经网络必须输出1。有了这个约束条件，只要我能解出来，找到一个满足条件的x值，就说明存在满足我们条件的后门。反之，如果我证明这个约束无解，那么我就证明不存在这种后门攻击。这个约束看起来很简单。第一个条件是简单的线性不等式。接下来的两个条件有点麻烦，因为它们使用了代表神经网络的函数N。这个还是比较复杂的。为了简单起见，我们假设这个神经网络是一个前馈神经网络。它可以有很多层，每一层的每个神经元都是两个函数，第一个是加权和，第二个是激活函数。激活函数比较麻烦，因为它是非线性的。常见的激活函数包括ReLU、SigMod和Tanh。也就是说，我们把N展开之后，就是一堆加权和和激活函数。加权和部分并不难，因为它是一个线性约束。我们知道，一堆线性函数在堆叠时仍然是线性的。同时，线性约束通常被认为是比较容易解决的。一些现有的用于解决线性约束的工业级工具仍然非常有用。使事情复杂化的是这些非线性激活函数。求解非线性函数基本上比较困难。比如ReLU，如果把ReLU写成程序，其实就是ReLU(x)=if(x>=0){x}else{0}这样一个简单的函数。虽然这个程序很简单，但它很麻烦，因为它不是线性的。因为它有条件判断，那么理论上你需要将两种情况分开处理。问题是一个神经网络中可能有几千甚至几亿个神经元。如果你必须为每个神经元分析两种情况，那么就有指数情况需要分析。那么我们该怎么办？我们的方法是使用程序分析中常用的抽象解释方法，用线性函数来近似这个非线性激活函数。如下图所示，我们可以用上下两行来逼近中间蓝色的ReLU函数。直观来说，这个ReLU的结果，我们不知道是什么，可能是0，也可能是x。但是我知道它一定在这两行的范围内，我只需要用这两行把它包起来，那么我们可以保证所有可能的结果，我已经考虑到了。只要我们能保证不会漏掉任何东西，那么如果我们的验证结果表明没有后门，我们就绝对可以不存在。同样，我们也可以使用线性函数来逼近其他激活函数。一旦我对所有激活函数进行了线性逼近，整个约束就变成了线性，问题就基本解决了。因为线性约束加上另一个线性，结果仍然是线性的。所以最后我们把一个神经网络抽象成一个巨大但线性的约束。我们可以利用已有的求解线性约束的工具直接求解。比如Z3和一些工业级工具就可以轻松解决。当然，这也取决于神经网络有多大。通常，具有数千个神经元的神经网络问题不大。这里有一个小细节需要注意。因为中间的抽象，如果我解决一个方案，这个方案实际上可能不会触发后门。因为我们在抽象的时候扩大了激活函数的范围，这个方案可能不满足原来的约束条件。例如，在上图中，真正的解决方案应该在蓝线上方。但是我们找到的解决方案可能就在它旁边的阴影部分。当然这个问题也不是什么大问题，因为我们找到解决办法之后，就可以测试一下，看看是不是真的有后门。重要的是我保证，我说没有后门，就一定没有后门。6后门问题二以上是问题一的解决方案。当然，你可以说这题的设置有点严格。因为实际的后门攻击和神经网络一样，很难做到100%的成功率。同时，上述设置需要用户提供一些具体的图片，而用户可能不知道如何选择这些图片。下面介绍一个我们解决的比较实际的后门问题。问题2：给定一个神经网络，一个预测目标，同时假设贴纸大小有约束，如何证明不存在成功率至少为Pr（比如80%）的后门攻击？以上问题设置对后门的成功率有一定的要求。这在实践中是有道理的。因为如果后门的成功率很低，那么攻击者就需要多次尝试，更容易被发现。我们解决这个问题的方法基于以下推导。如果存在成功率至少为Pr的后门攻击，则随机选择的K张图片上发生后门攻击成功率为100%的概率至少为：，即随机选择的K张图片上没有一张pictures成功率100%的后门攻击概率最多。反之，只要证明随机抽取的K张图片不存在成功率为100%的后门攻击，则可以推论不存在成功率至少为Pr的后门攻击。那么我们如何判断随机选取的K张图片是否超过了没有成功率100%的后门攻击的概率呢？答案是统计假设检验（hypothesistesting）。简单的说就是反复随机抽样，然后做一个概率分析。具体方法是随机抽取K张图片，然后用刚才解决第一个问题的方法判断是否存在后门攻击，成功率100%。然后选择K张图片重新判断。比如我连续试了1000次，结论是不存在K张图片成功率100%的后门攻击，那么你可以直观的想象随机K张不存在100%成功率的后门攻击选中图片的概率已经很高了。就算有几组K图后门攻击成功率100%，只要不存在的次数足够多，我也可以说明没有后门攻击成功率的概率在随机选择的K张图片上的100%非常高。当然，具体的高度是有算法计算的。如果您有兴趣，我们使用SPRT算法。这个算法主要是告诉我们随机次数和结果什么时候可以让我们证明随机抽取的K张图片不存在100%成功率的后门攻击概率。具体可以参考[8]。同样，我们对第二个问题的解决方案中有一个有趣的小细节。就是关于K的值，理论上我可以选择任意的K，因为我们的算法证明中对K的值没有要求。但它不是在实践中。比如我可以把K选的很小，比如1。也就是说我每次画一张图，然后我看看能不能对这张图做后门攻击，也就是说有没有上面有一张贴纸，可以改变它的预测。这样做的结果很可能是存在。因为我们知道神经网络是不鲁棒的，所以这种所谓的对单张图片的后门攻击其实等同于对抗性扰动。我们都知道，恶意干扰一般会随意改变几个像素点，基本上就可以改变预测。但如果是这样的话，这个结果对我们来说就没有意义了，因为我每次提取K张图片，都发现有成功率100%的后门攻击，不能得出我想要的结论。所以K不能选得太小。同时，K也不能太大，因为我们解决问题1需要解决一个约束，K越大，约束也越复杂（因为这个约束要求后门攻击对每张图片都成功）.你可以想象一下，如果K是100万，这个约束包括对100万张图片的约束，结果就是我们解决不了。当然，我们不能得出任何结论。我们也没有想出什么理论来解决这个问题。我们最终通过实验确定了一个更有用的K值，一般在5到10之间。7实验结果我们在我们的神经网络验证平台Socrates上实现了上述方法。Socrates：https://socrates4nn.github.io/也用一些常见的神经网络做了一系列实验，例如在MNIST数据集上训练的神经网络。比如在MNIST上训练的识别数字的神经网络，我们试试看有没有后门攻击，比如给任意数字加一个白色的小方块就可以让它识别2。我们试的网络大概有几百个到几千个神经元，这不是太大。好消息是我们可以验证大多数情况。一个意想不到的结果是，我们发现有些神经网络即使没有受到攻击，也天然存在一些后门。比如下图的例子，虽然我们没有刻意埋这个神经网络的后门，但是第一行的数字加上右边的白色小方块，都被识别为2。一般来说，任何这个位置有这个小白块的数据，有80%的概率会被识别为2。至于为什么会出现这种现象，我这里保密，不展开讨论。8更多难点以上就是如何解决两次神经网络后门攻击的问题。具体技术细节可以参考[8]。当然，以上两个问题的设置都比较简单，未来还有很多很多很多有趣的问题没有解决，因为各种创造性的后门攻击不断出现。让我举一个非常简单的例子。比如有这样的后门攻击：黑客把训练集中所有的绿色汽车挑出来，标记为青蛙。那么你可以想象，经过训练的神经网络会很自然地将绿色汽车识别为青蛙。这称为语义后门。因为知道这是一个后门需要我们理解语义（即汽车不应该是青蛙）。从神经网络的角度来看，神经网络如何知道绿色汽车不应该是青蛙呢？你也可以想象，这种后门也是对安全很关键的，比如说，如果你的自动驾驶汽车将前面的绿色汽车识别为一只青蛙，那么我不确定会发生什么。那么我们如何解决这个语义后门的问题呢？比如给我一个神经网络，我怎么查里面有没有这种语义后门？我们正在努力解决这个问题。你可以想想怎么定义这个问题。9结语最后我想说的是：“神经网络是一个特殊的程序，就神经网络的特殊程序而言，我们还缺乏理论、工具、流程和标准来保证神经网络的质量”乐观说白了，神经网络有各种各样的问题是好事，就像传统软件的问题造就了一个与软件质量相关的整个行业，相信大家很快就会看到一个与软件质量相关的整个行业。神经网络质量。
