nat类型 检测（nat类型检测在线）



文章题目: 完备神经网络验证加速技术综述

全部作者: 刘宗鑫, 杨鹏飞, 张立军, 吴志林, 黄小炜

第一单位: 中国科学院软件研究所 计算机科学国家重点实验室

出版时间: 2024, 35(9):4038-4068

摘

/

要

ABSTRACT

ABSTRACT

人工智能技术已被广泛应用于生活中的各个领域. 然而, 神经网络作为人工智能的主要实现手段, 在面对训练数据之外的输入或对抗攻击时, 可能表现出意料之外的行为. 在自动驾驶、智能医疗等安全攸关领域, 这些未定义行为可能会对生命安全造成重大威胁. 因此, 使用完备验证方法证明神经网络的性质, 保障其行为的正确性显得尤为重要. 为了提高验证效率, 各种完备神经网络验证工具均提出各自的优化方法, 但并未充分探索这些方法真正起到的作用, 后来的研究者难以从中找出最有效的优化方向. 介绍神经网络验证领域的通用技术, 并提出一个完备神经网络验证的通用框架. 在此框架中, 重点讨论目前最先进的工具在约束求解、分支选择与边界计算这3个核心部分上的所采用的优化方法. 针对各个工具本身的性能和核心加速方法, 设计一系列实验, 旨在探究各种加速方式对于工具性能的贡献, 并尝试寻找最有效的加速策略和更具潜力的优化方向, 为研究者提供有价值的参考.

扫码阅读全文

内

/

容

/

精

/

选

CONTENT

CONTENT

目前对神经网络安全性的评估主要有基于测试的方法与基于形式化验证的方法两类. 基于测试的方法只考虑有限的输入集, 无法覆盖所有可能的输入, 因此可能存在未检测到的错误或漏洞, 难以进行精准性验证. 为确保神经网络始终具有所需要的性质, 我们需要使用形式化的方法对神经网络的性质进行严格验证.

1 神经网络验证通用技术

神经网络验证领域中的通用技术包括激活函数抽象, 拉格朗日乘子法, 符号区间反向传播方法, 约束求解方法以及分支限界方法. 算法1 中总结出使用边界计算、约束求解与分支限界方法进行神经网络验证的通用框架以帮助读者了解完备神经网络验证的流程.

算法1 神经网络验证通用验证框架

与以全局上下界计算为核心的框架不同, 本文所提框架将约束求解过程纳入其中, 从而概括更多的验证方法. 开始验证时, 将原始的验证问题入队. 随后, 执行循环直到队列中的元素为空. 在循环中, 取出队列中的验证问题并计算边界. 如果可以证明该问题性质成立则进行回溯并进入下一次循环. 如果无法证明, 则进行约束求解. 若约束求解成功证明性质成立, 则进行回溯并进入下一次循环, 如果证明出性质不成立则返回SAT, 如果无法判断是否成立, 则进行分支, 并将子问题入队.

2 神经网络验证加速技术

本文详细调研了目前最先进的完备验证工具针对边界计算、分支选择和约束求解这3个完备验证算法的核心步骤. 表1对我们将要介绍的工具及其所使用的加速方法进行了简单总结. 我们将选择其中较为关键或者新颖的加速方法进行详细介绍, 并给出便于理解的例子来说明加速方法的关键步骤.

表1 工具及其优化技术

3 实验

本文选择目前最先进并开源的工具, 在大中小3类开源数据集设计了一系列实验：

(1) 在统一设备上实验, 以公平地比较各个工具的性能.

(2) 将原本使用GPU加速的程序转换为使用CPU运行, 以比较在没有GPU加速的情况下核心算法的性能.

(3) 针对并行计算、PGD攻击等常用的加速方法及核心加速方式进行了一系列实验以探究这些加速方法的效果, 并尝试找出值得付出努力优化的方向.

根据实验结果发现:

(1) 在性能方面, 不同工具擅长处理不同规模的网络, 不存在工具在所有规模的网络上的都做到顶尖的性能. 如在单线程情况下, VeriNet在ACAS Xu上远超其他工具, Venus2则在MNIST FC中表现最好, 在Cifar10_resnet数据集中则是MN-BaB表现最为突出; 而在开启所有加速方法时, nnenum在ACAS Xu上表现最好, α,β-CROWN则在其他两个数据集上有最好的表现.

(2) 在加速方法方面, 进行边界计算与约束求解时, 添加高质量的约束有助于加速验证. 例如GCP-CROWN添加额外的约束可以让平均求解速度上升32.9%, 而是否添加多神经元约束对MN-BaB的效率影响不大.

(3) 分支选择顺序对于验证效率的影响较大, 合理的分支顺序可以加快求解效率. 例如Verinet使用随机分支选择时求解数目下降到原来的一半, 而Marabou关闭SoI方法反而可以多求解出几个验证问题.

(4) 并行方法对于小规模的网络加速明显, 但在中大型网络中, 并行的效果并不显著.

(5) 攻击方法多数情况下可以帮助工具迅速找出违反性质的反例.

4 未来研究方向

完备神经网络验证领域发展迅速, 各种验证工具层出不穷. 本文总结了目前先进验证工具的通用框架, 并指出其中的核心部分: 边界计算、分支选择与约束求解. 我们对目前最先进工具在这3个核心部分中做出的探索进行了详细调研, 并给出易于理解的例子进行说明. 为了找出最有效的优化方向, 我们针对各种优化方法进行了实验.

(1) 实验中发现边界计算与约束求解时, 添加额外的约束确实能起到一定程度的加速, 但添加约束的质量更加关键. 如何产生更加有效的约束以及如何更加高效的利用这些约束可能是一个可行的优化方向.

(2) 约束求解是目前大多数研究所欠缺的地方. 大多数工具直接使用现成的数学规划工具与理论. 因此, 有必要进一步研究约束求解的理论创新以及设计针对神经网络验证的数学规划方法, 这可能是一个困难但充满潜力的方向.

(3) 分支选择的顺序对求解的效率有着较大的影响, 比较明显的是Verinet工具, 随机进行分支选择可能会造成超时, 但使用启发式选择却可以很快进行验证; 其他工具如PEREGRiNN使用启发式的分支选择时也有着一定幅度的加速. 如何设计高效的分支选择策略是一个值得探索的问题.

(4) 其他加速技术中, 并行方法对于小型网络的验证效果较为显著, 对于中型或者大型网络的验证虽然有一定程度的加速, 但对工具的求解能力并没有本质上的提升, 除非极大的提升并行数量, 但这对计算设备的要求较高. PGD攻击方法对于解决一些本身性质不成立的验证问题有很大的帮助, 但仍然需要进行小心的实现并设置合理的迭代次数, 否则可能反而拖慢求解速度, 甚至出现错误.

(5) 各个工具在易用性以及实现细节上仍然需要提升 , α,β-CROWN、MN-BaB虽然性能较好但配置繁琐; Verinet有严重的内存泄露问题; Venus2与Marabou的使用虽然简便, 但总是容易出现验证错误; PEREGRiNN, nnenum同样使用简便, 但支持的网络类型较少.

最后, 值得注意的是, 网络规模仍然是横亘在验证工具发展之路上的一座大山, 即使是目前最先进的工具在验证稍大型的网络的性质时仍有无法在规定时间内完成的情况, 需要对完备神经网络加速技术进行进一步的研究. 完备神经网络验证领域的发展任重道远, 但我们相信通过不断的努力和创新, 该领域将取得更大的突破.

作

/

者

/

简

/

介

A U T H O R

AUTHOR

刘宗鑫, 博士, CCF学生会员, 主要研究领域为形式化方法, 神经网络验证.

吴志林, 博士, 研究员, CCF高级会员, 主要研究领域为计算逻辑, 自动机理论, 计算机软硬件基础设施的形式化验证.

杨鹏飞, 博士, CCF专业会员, 主要研究领域为人工智能安全, 概率模型检验.

黄小炜, 博士, 教授, 博士生导师, 主要研究领域为人工智能安全与验证, AI可解释性, 形式化方法.

张立军, 博士, 研究员, 博士生导师, CCF高级会员, 主要研究领域为概率模型检测, 协议验证, 学习算法, 自动驾驶系统验证.

版权声明：

本文来自互联网用户投稿，该文观点仅代表作者本人，不代表本站立场。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。
如若内容造成侵权、违法违规、事实不符，请将相关资料发送至xkadmin@xkablog.com进行投诉反馈，一经查实，立即处理！

转载请注明出处，原文链接：https://www.xkablog.com/bcyy/43522.html