神经网络形式化验证的两级加速：目标感知拆分排序与验证器无关学习路由

《Neurocomputing》：Two-level acceleration for neural network formal verification: Objective-aware split ranking and verifier-agnostic learned routing

　　验证器无关的路由器会跳过由后备验证器预测为安全的高置信度实例。目标感知的分裂排序优先考虑具有影响力的不稳定ReLU神经元。该组合框架将ACAS Xu的运行时间从10.40分钟减少至3.62分钟。风险通过一致性、假安全案例和阈值分析进行报告。**引言**神经网络形式化验证已成为为基于学习的系统建立严格安全保证的重要技术，特别是在经验测试单独不足以确保安全的安全关键领域。对于分段线性神经网络，早期的精确方法如Reluplex、Marabou和基于MILP的验证将验证问题建模为约束求解或优化问题，提供了强大的形式化保证，但随着网络规模和规范复杂度的增加，其可扩展性往往受到限制[1]、[2]、[3]。为提高可扩展性，第二类研究工作发展了抽象解释和过近似技术，包括AI2、可微抽象解释、nnenum、NNV和PyRAT，这些方法可以更高效地验证更大的模型，但可能在困难实例上损失精度[4]、[5]、[6]、[7]、[8]。近年来，基于分支定界的完备验证器和边界传播方法，如BaB、β-CROWN、α,β-CROWN及相关完备验证框架，通过结合更紧的边界与系统化搜索，进一步提高了神经网络验证的实际性能[9]、[10]、[11]、[12]、[13]。这些进展显著扩展了神经网络验证的适用范围，但验证的计算成本仍是阻碍其常规部署的主要障碍。尽管取得了上述进展，两个实际挑战仍限制了现有验证流程的效率。首先，大多数验证器独立地从零开始处理每个验证实例，即使在基准测试或部署场景中，许多实例共享相似的网络架构、输入区域或规范结构。因此，历史验证运行中潜在有用的模式未被利用，以避免对简单或高置信度案例进行不必要的完整验证。其次，对于无法安全跳过的困难实例，验证器仍需要执行昂贵的分支定界搜索，其中不稳定ReLU分裂的顺序会强烈影响被探索的节点数、LP调用次数和总运行时间[9]、[14]、[15]。现有的分支启发式方法可以提高搜索效率，但它们通常与特定验证器实现绑定，或者需要与底层边界计算进行非平凡的集成。因此，仍需要一种加速策略，既能从流水线层面减少冗余验证，又能提高后备验证器内部的搜索效率。为应对这些挑战，我们提出了一种面向神经网络形式化验证的两级加速框架。在外层，我们引入一种验证器无关的学习型路由器，作为在调用完整验证之前进行选择性验证的层级。此处，"验证器无关"是指该路由器仅依赖验证实例特征，包括网络结构、输入区域和规范信息，而不依赖验证器特定的内部状态或求解器相关的信息。给定一个验证实例，路由器从网络结构、输入域和规范中提取统一特征，然后使用一个带有规范依赖动态置信阈值的学习分类器，判断该实例是否可以作为高置信度安全案例接受，或者是否应交由后备验证器处理。这种设计使框架能够在简单实例上避免冗余的完整验证，同时对不确定或潜在不安全的案例保留保守的后备路径。在内层，对于路由器未接受的实例，我们通过目标感知的分裂排序策略改进后备验证。所提出的排序方法赋予既具有不确定性又与当前验证目标更相关的验证器无关的路由器会跳过由后备验证器预测为安全的高置信度实例。目标感知的分裂排序优先考虑具有影响力的不稳定ReLU神经元。该组合框架将ACAS Xu的运行时间从10.40分钟减少至3.62分钟。风险通过一致性、假安全案例和阈值分析进行报告。**引言**神经网络形式化验证已成为为基于学习的系统建立严格安全保证的重要技术，特别是在经验测试单独不足以确保安全的安全关键领域。对于分段线性神经网络，早期的精确方法如Reluplex、Marabou和基于MILP的验证将验证问题建模为约束求解或优化问题，提供了强大的形式化保证，但随着网络规模和规范复杂度的增加，其可扩展性往往受到限制[1]、[2]、[3]。为提高可扩展性，第二类研究工作发展了抽象解释和过近似技术，包括AI2、可微抽象解释、nnenum、NNV和PyRAT，这些方法可以更高效地验证更大的模型，但可能在困难实例上损失精度[4]、[5]、[6]、[7]、[8]。近年来，基于分支定界的完备验证器和边界传播方法，如BaB、β-CROWN、α,β-CROWN及相关完备验证框架，通过结合更紧的边界与系统化搜索，进一步提高了神经网络验证的实际性能[9]、[10]、[11]、[12]、[13]。这些进展显著扩展了神经网络验证的适用范围，但验证的计算成本仍是阻碍其常规部署的主要障碍。尽管取得了上述进展，两个实际挑战仍限制了现有验证流程的效率。首先，大多数验证器独立地从零开始处理每个验证实例，即使在基准测试或部署场景中，许多实例共享相似的网络架构、输入区域或规范结构。因此，历史验证运行中潜在有用的模式未被利用，以避免对简单或高置信度案例进行不必要的完整验证。其次，对于无法安全跳过的困难实例，验证器仍需要执行昂贵的分支定界搜索，其中不稳定ReLU分裂的顺序会强烈影响被探索的节点数、LP调用次数和总运行时间[9]、[14]、[15]。现有的分支启发式方法可以提高搜索效率，但它们通常与特定验证器实现绑定，或者需要与底层边界计算进行非平凡的集成。因此，仍需要一种加速策略，既能从流水线层面减少冗余验证，又能提高后备验证器内部的搜索效率。为应对这些挑战，我们提出了一种面向神经网络形式化验证的两级加速框架。在外层，我们引入一种验证器无关的学习型路由器，作为在调用完整验证之前进行选择性验证的层级。此处，"验证器无关"是指该路由器仅依赖验证实例特征，包括网络结构、输入区域和规范信息，而不依赖验证器特定的内部状态或求解器相关的信息。给定一个验证实例，路由器从网络结构、输入域和规范中提取统一特征，然后使用一个带有规范依赖动态置信阈值的学习分类器，判断该实例是否可以作为高置信度安全案例接受，或者是否应交由后备验证器处理。这种设计使框架能够在简单实例上避免冗余的完整验证，同时对不确定或潜在不安全的案例保留保守的后备路径。在内层，对于路由器未接受的实例，我们通过目标感知的分裂排序策略改进后备验证。所提出的排序方法赋予既具有不确定性又与当前验证目标更相关的不稳定ReLU神经元更高的优先级，从而引导分支定界搜索朝向信息量更大的分裂方向进行。这样，外层机制减少了需要完整验证的实例数量，而内层机制降低了剩余困难实例的搜索成本。本文的主要贡献是一个实用且具有风险意识的加速框架，该框架将数据驱动的路由与验证器内部搜索优化相结合。首先，我们设计了一种验证器无关的选择性路由机制，该机制在不修改后端验证器的情况下利用历史验证模式。其次，我们提出了一种轻量级的目标感知分裂排序策略，该策略通过引导验证器朝向更具影响力的不稳定神经元，提高了分支定界效率。第三，我们将这两种机制集成到一个统一的流水线中，并在扩展的186实例ACAS Xu评估池上评估它们的互补性。结果表明，外部路由在保持与基线验证器98.43%的一致性的同时，将运行时间从10.40分钟减少到6.66分钟；内部分裂排序将后备验证运行时间减少到6.08分钟，同时将LP调用次数减少47.0%，访问节点数减少44.8%；组合框架进一步将总运行时间减少到3.62分钟。这些结果表明，验证器无关的路由和目标感知的验证器内部优化是互补的，为快速筛查、批量验证和开发期间的迭代提供了有效的加速层，同时保留了显式的经验风险报告。**章节片段****相关工作**神经网络形式化验证沿着几个主要方向发展，包括精确推理、可扩展的过近似和基于分支定界的完备验证。早期的精确方法如Reluplex、Marabou和基于MILP的方法为分段线性网络提供了强有力的保证，但随着网络规模和规范复杂度的增加，其可扩展性往往受到限制[1]、[2]、[3]。为提高效率，抽象解释及相关技术……**预备知识**本节建立了本文所使用的符号和验证设置。我们将每个验证任务视为一个实例，该实例由神经网络、输入域和输出安全规范组成。这种实例级建模支持我们框架的两个组成部分：学习型路由器从这些对象中提取验证器无关的特征，而后备验证器则使用规范来证明安全性或寻找违规。然后我们回顾了分支定界的观点……**方法**本节提出了所提出的两级加速框架。我们首先总结整体流水线，然后描述外部学习路由机制、内部目标感知分裂排序策略，以及它们如何集成到统一的验证工作流中。**实验目标与研究问题**实验旨在从三个方面评估所提出的两级加速框架：外部学习路由机制的有效性、内部目标感知分裂排序机制的有效性，以及集成两个组件的整体收益。具体而言，我们调查所提出的框架是否能在实例路由级别和验证器内部搜索级别降低验证成本，同时保持高……**讨论**所提出的框架通过针对神经网络验证中两个不同的计算成本来源来提高验证效率。外部路由器减少了需要进入完整验证器的实例数量，而内部分裂排序策略减少了仍需后备验证的实例的搜索负担。这解释了为什么组合框架比单独使用任何一个组件获得更大的收益。在扩展的186实例ACAS Xu评估……**结论**我们提出了一种面向神经网络形式化验证的两级加速框架，该框架结合了验证器无关的学习型路由器与用于后备验证的目标感知分裂排序策略。在由标准180实例ACAS Xu基准测试和6个额外保留实例构建的扩展186实例ACAS Xu评估池上，所提出的框架显著提高了验证效率：外部路由将运行时间从10.40分钟减少到6.66分钟……**代码可用性**实现代码可在合理请求下从通讯作者处获取，因为完整代码库是正在进行的研究项目的一部分。**写作过程中生成式AI和AI辅助技术的声明**在准备本文过程中，作者使用ChatGPT协助语言润色和编辑完善。使用此工具后，作者根据需要审查并编辑了内容，并对稿件内容承担全部责任。**资金**本工作得到陕西省教育厅科研项目资助计划（项目编号：25JP117）和中国国家自然科学基金（批准号：62202371和61902312）的支持。**利益冲突声明**作者声明，他们不知道有任何可能影响本文所报告工作的竞争性经济利益或个人关系。**作者简介**王海洋，西安理工大学计算机科学与工程学院讲师。她分别于西安电子科技大学获得软件工程学士学位和计算机应用技术博士学位。她的研究兴趣包括形式化验证方法、多智能体系统验证和神经网络验证。她当前的研究专注于为智能系统开发高效可靠的验证技术。王海洋 | 刘萌琪 | 费蓉 | 刘金 | 邵伟