核心发现
方法论
本文提出了一种增量验证技术，通过重用学习到的冲突来加速神经网络的验证过程。该技术可以集成到任何基于分支定界的神经网络验证器中。验证过程中，验证器记录与学习到的不可行激活阶段组合相对应的冲突，并在多次运行中保留它们。我们形式化了验证查询之间的细化关系，并证明了对一个查询学习到的冲突在细化下仍然有效，从而实现了合理的冲突继承。继承的冲突通过SAT求解器进行一致性检查和传播，使得不可行的子问题可以在搜索过程中及早被检测和修剪。
关键结果
- 实验结果表明，与非增量基线相比，增量冲突重用减少了验证工作量，并在三个验证任务中实现了最高1.9倍的加速。
- 在局部鲁棒性半径确定任务中，增量方法在MNIST数据集上的平均求解时间比非增量方法快1.3倍。
- 在输入分割的验证任务中，增量方法在Lyapunov神经证书训练过程中有效地减少了验证时间。
研究意义
神经网络在自动驾驶、医疗诊断和航空航天系统等安全关键应用中越来越多地被部署。然而，神经网络的复杂性和不透明性使得在这些关键环境中保证其可靠性和安全性变得困难。通过引入增量验证技术，本文的研究为神经网络验证提供了一种更高效的方法，能够在多个相关查询中重用信息，减少冗余计算。这不仅提高了验证效率，还为神经网络在安全关键领域的应用提供了更强的保障。
技术贡献
本文的技术贡献在于提出了一种新的增量验证框架，能够在多个相关的验证查询中重用学习到的冲突。这种方法与现有的基于分支定界的验证器兼容，并通过使用SAT求解器进行冲突传播和一致性检查，显著减少了验证时间。此外，本文还形式化了验证查询之间的细化关系，确保了冲突继承的合理性。
新颖性
本文首次提出了在神经网络验证中重用学习到的冲突的概念，与现有的增量求解技术不同，本文的方法专注于在多个分支定界的完整验证器调用中重用引理。这种方法不仅提高了验证效率，还为神经网络验证提供了新的理论保证。
局限性
- 该方法在处理非常大规模的神经网络时可能会遇到内存限制，因为需要存储大量的冲突信息。
- 对于某些特定类型的神经网络结构，冲突重用的效果可能不如预期。
- 在某些情况下，冲突的继承可能会导致额外的计算开销。
未来方向
未来的研究方向包括探索如何在更大规模的神经网络上实现增量验证技术，以及如何在其他类型的神经网络结构中应用该技术。此外，还可以研究如何进一步优化冲突存储和传播机制，以提高验证效率。
AI 总览摘要
神经网络在自动驾驶、医疗诊断和航空航天系统等安全关键应用中越来越多地被部署。然而，由于其复杂性和不透明性，神经网络在这些关键环境中的可靠性和安全性引发了严重的担忧。为了应对这一问题，许多神经网络验证方法被提出，旨在为网络行为提供严格的保证。然而，现有的验证工具通常在处理多个相关的验证查询时效率低下，因为每个查询都是独立求解的，之前运行中学到的信息被丢弃，导致重复探索搜索空间中相同的不可行区域。
本文提出了一种增量验证技术，通过重用学习到的冲突来加速神经网络的验证过程。该技术可以集成到任何基于分支定界的神经网络验证器中。验证过程中，验证器记录与学习到的不可行激活阶段组合相对应的冲突，并在多次运行中保留它们。我们形式化了验证查询之间的细化关系，并证明了对一个查询学习到的冲突在细化下仍然有效，从而实现了合理的冲突继承。继承的冲突通过SAT求解器进行一致性检查和传播，使得不可行的子问题可以在搜索过程中及早被检测和修剪。
我们在Marabou验证器中实现了所提出的技术，并在三个验证任务上进行了评估：局部鲁棒性半径确定、输入分割的验证和最小充分特征集提取。实验结果表明，与非增量基线相比，增量冲突重用减少了验证工作量，并在三个验证任务中实现了最高1.9倍的加速。
在局部鲁棒性半径确定任务中，我们在MNIST数据集上进行了实验，结果显示增量方法的平均求解时间比非增量方法快1.3倍。在输入分割的验证任务中，增量方法在Lyapunov神经证书训练过程中有效地减少了验证时间。
本文的研究为神经网络验证提供了一种更高效的方法，能够在多个相关查询中重用信息，减少冗余计算。这不仅提高了验证效率，还为神经网络在安全关键领域的应用提供了更强的保障。未来的研究方向包括探索如何在更大规模的神经网络上实现增量验证技术，以及如何在其他类型的神经网络结构中应用该技术。
深度分析
研究背景
随着深度神经网络（DNNs）在自动驾驶、医疗诊断和航空航天系统等安全关键应用中的广泛应用，确保其可靠性和安全性变得至关重要。尽管神经网络在控制和图像识别等任务中表现出色，但其复杂性和不透明性使得在这些关键环境中保证其可靠性和安全性变得困难。为了解决这一问题，许多神经网络验证方法被提出，旨在为网络行为提供严格的保证。然而，对于具有分段线性激活函数（如ReLU）的网络，验证问题是NP完全的，这限制了其可扩展性。随着神经网络在越来越多样化和高风险的领域中被采用，对可扩展验证技术的需求不断增长。因此，提高神经网络验证的效率是当务之急。
核心问题
在实际应用中，DNN验证通常不是作为一个单一的、孤立的查询来执行，而是反复调用于更大的分析过程中。例如，在形式化可解释性中，验证查询被反复发出，以在逐步细化的约束下推理不同输入特征对给定预测的贡献；同样，在鲁棒性半径计算中，验证查询被迭代调用，以缩小给定输入周围的最大安全扰动半径。这些分析自然产生了一系列密切相关的验证查询，它们在规格的有限方面有所不同，如细化的输入域或增强的输出约束。尽管如此，当前的验证工具并没有明确利用这种结构相似性：每个查询都是从头开始的，之前运行中得出的信息被丢弃。
核心创新
本文提出了一种增量验证技术，通过重用学习到的冲突来加速神经网络的验证过程。该技术可以集成到任何基于分支定界的神经网络验证器中。验证过程中，验证器记录与学习到的不可行激活阶段组合相对应的冲突，并在多次运行中保留它们。我们形式化了验证查询之间的细化关系，并证明了对一个查询学习到的冲突在细化下仍然有效，从而实现了合理的冲突继承。继承的冲突通过SAT求解器进行一致性检查和传播，使得不可行的子问题可以在搜索过程中及早被检测和修剪。我们开发了一个冲突记录和合理重用的框架，直接与基于分支定界的验证器集成，并使用SAT求解器高效管理和应用在求解过程中学习到的大量冲突。
方法详解
- �� 增量验证框架：记录在分支定界验证过程中出现的冲突，每个冲突捕获一个不可行的分支决策组合。
- �� 冲突保留：这些冲突超越单个验证运行，并在后续具有细化规格的查询中重用。
- �� 冲突继承：我们形式化了冲突在细化查询中的有效性条件，并证明了该条件在神经网络验证的几个重要应用中可以成立。
- �� 使用SAT求解器：在分支定界搜索过程中，使用SAT求解器对继承的冲突子句进行推理，作为额外的修剪和传播步骤。
- �� 实现：在Marabou验证器中实现了所提出的方法，并在三个代表性验证任务上进行了评估。
实验设计
我们在Marabou验证器中实现了所提出的技术，并在三个验证任务上进行了评估：局部鲁棒性半径确定、输入分割的验证和最小充分特征集提取。在局部鲁棒性半径确定任务中，我们在MNIST数据集上进行了实验，结果显示增量方法的平均求解时间比非增量方法快1.3倍。在输入分割的验证任务中，增量方法在Lyapunov神经证书训练过程中有效地减少了验证时间。我们使用了CaDiCaL SAT求解器进行冲突推理，所有由同一任务引发的验证查询共享一个ICA实例。通过继承的冲突进行的传播可能会检测到当前部分分配不可行，从而允许验证器立即修剪子问题，或通过单元传播推导出额外的ReLU阶段分配。
结果分析
实验结果表明，与非增量基线相比，增量冲突重用减少了验证工作量，并在三个验证任务中实现了最高1.9倍的加速。在局部鲁棒性半径确定任务中，增量方法在MNIST数据集上的平均求解时间比非增量方法快1.3倍。在输入分割的验证任务中，增量方法在Lyapunov神经证书训练过程中有效地减少了验证时间。通过继承的冲突进行的传播可能会检测到当前部分分配不可行，从而允许验证器立即修剪子问题，或通过单元传播推导出额外的ReLU阶段分配。
应用场景
本文提出的增量验证技术可以直接应用于需要高效验证的神经网络模型中，尤其是在安全关键的应用场景中，如自动驾驶和医疗诊断。通过减少冗余计算，该技术可以显著提高验证效率，降低计算成本。此外，该技术还可以用于其他需要多次验证的场景，如模型优化和调优。
局限与展望
尽管本文提出的增量验证技术在多个验证任务中表现出色，但在处理非常大规模的神经网络时可能会遇到内存限制，因为需要存储大量的冲突信息。此外，对于某些特定类型的神经网络结构，冲突重用的效果可能不如预期。在某些情况下，冲突的继承可能会导致额外的计算开销。未来的研究方向包括探索如何在更大规模的神经网络上实现增量验证技术，以及如何在其他类型的神经网络结构中应用该技术。
通俗解读 非专业人士也能看懂
想象一下你在厨房里做饭。每次你做一道新菜，你都要从头开始准备所有的食材和工具。这就像传统的神经网络验证方法，每次验证一个新的查询时，都要从头开始。然而，本文提出的方法就像是你在厨房里准备了一些常用的调料和工具，可以在做不同的菜时重复使用。这样，你就不需要每次都重新准备所有的东西，而是可以直接使用已经准备好的材料，大大提高了效率。这种方法通过记录和重用之前验证过程中学习到的冲突信息，减少了重复计算，使得验证过程更加高效。就像在厨房里，你可以更快地做好每一道菜，因为你已经有了一些准备好的材料和工具。
简单解释 像给14岁少年讲一样
嘿，想象一下你在玩一个游戏。每次你过关的时候，你都要重新开始，完全不记得之前的经验。这是不是很烦人？这就是传统神经网络验证的样子，每次验证一个新的查询时，都要从头开始。但是，本文提出的方法就像是游戏中的存档点。每次你过关时，都会记录下你学到的东西，下次再玩的时候，你可以直接从存档点开始，而不是从头再来。这种方法通过记录和重用之前验证过程中学到的冲突信息，减少了重复计算，使得验证过程更加高效。就像在游戏中，你可以更快地过关，因为你已经有了一些存档点。
术语表
Neural Network (神经网络)
一种模拟人脑神经元连接的计算模型，广泛应用于模式识别和机器学习。
用于自动驾驶、医疗诊断等领域的模型。
Verification (验证)
一种用于确保系统或模型行为符合预期的过程，通常涉及数学证明。
用于确保神经网络在关键应用中的可靠性。
Incremental Verification (增量验证)
一种通过重用之前验证过程中学到的信息来加速验证的技术。
本文提出的方法，旨在提高验证效率。
Conflict (冲突)
在验证过程中发现的不可行的决策组合，通常用于修剪搜索空间。
记录在分支定界过程中，以减少冗余计算。
SAT Solver (SAT求解器)
一种用于解决布尔可满足性问题的算法工具，广泛用于验证和优化。
用于处理继承的冲突子句，进行一致性检查。
Branch-and-Bound (分支定界)
一种通过递归分割问题空间来求解优化问题的算法。
用于神经网络验证的核心技术。
ReLU (线性整流函数)
一种常用的激活函数，定义为f(x)=max(0,x)，用于神经网络中。
在验证过程中引入分支行为。
Local Robustness (局部鲁棒性)
衡量神经网络在输入扰动下输出稳定性的指标。
验证任务之一，确定最大安全扰动半径。
Feature Set (特征集)
用于训练和验证模型的输入变量集合。
在最小充分特征集提取任务中使用。
Marabou (Marabou验证器)
一种用于神经网络验证的工具，支持多种验证任务。
本文中实现增量验证技术的平台。
开放问题 这项研究留下的未解疑问
- 1 如何在更大规模的神经网络上实现增量验证技术？当前方法在处理非常大规模的神经网络时可能会遇到内存限制，需要进一步研究如何优化冲突存储和传播机制。
- 2 在其他类型的神经网络结构中如何应用增量验证技术？本文的方法主要针对具有ReLU激活函数的网络，其他类型的网络可能需要不同的处理策略。
- 3 如何进一步提高冲突重用的效率？虽然本文的方法已经显著减少了验证时间，但在某些情况下，冲突的继承可能会导致额外的计算开销。
- 4 在安全关键应用中，如何确保增量验证的可靠性？尽管增量验证提高了效率，但在关键应用中，验证的准确性和可靠性仍然是首要考虑因素。
- 5 如何在分布式系统中实现增量验证？随着神经网络规模的扩大，分布式计算成为一种可能的解决方案，需要研究如何在分布式环境中实现增量验证。
应用场景
近期应用
自动驾驶系统
通过提高神经网络验证的效率，确保自动驾驶系统在各种环境下的可靠性和安全性。
医疗诊断
在医疗诊断中应用增量验证技术，以确保诊断模型的准确性和稳定性。
航空航天系统
在航空航天系统中应用增量验证技术，以提高系统的安全性和可靠性。
远期愿景
智能城市
通过提高神经网络验证的效率，支持智能城市中复杂系统的安全运行。
工业自动化
在工业自动化中应用增量验证技术，以提高生产线的效率和安全性。
原文摘要
Neural network verification is often used as a core component within larger analysis procedures, which generate sequences of closely related verification queries over the same network. In existing neural network verifiers, each query is typically solved independently, and information learned during previous runs is discarded, leading to repeated exploration of the same infeasible regions of the search space. In this work, we aim to expedite verification by reducing this redundancy. We propose an incremental verification technique that reuses learned conflicts across related verification queries. The technique can be added on top of any branch-and-bound-based neural network verifier. During verification, the verifier records conflicts corresponding to learned infeasible combinations of activation phases, and retains them across runs. We formalize a refinement relation between verification queries and show that conflicts learned for a query remain valid under refinement, enabling sound conflict inheritance. Inherited conflicts are handled using a SAT solver to perform consistency checks and propagation, allowing infeasible subproblems to be detected and pruned early during search. We implement the proposed technique in the Marabou verifier and evaluate it on three verification tasks: local robustness radius determination, verification with input splitting, and minimal sufficient feature set extraction. Our experiments show that incremental conflict reuse reduces verification effort and yields speedups of up to $1.9\times$ over a non-incremental baseline.
参考文献 (20)
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Guy Katz, Clark W. Barrett, D. Dill 等
The Marabou Framework for Verification and Analysis of Deep Neural Networks
Guy Katz, Derek A. Huang, D. Ibeling 等
CaDiCaL 2.0
Armin Biere, Tobias Faller, Katalin Fazekas 等
Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
Stanley Bak, Hoang-Dung Tran, Kerianne L. Hobbs 等
General Cutting Planes for Bound-Propagation-Based Neural Network Verification
Huan Zhang, Shiqi Wang, Kaidi Xu 等
The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results
Stanley Bak, Changliu Liu, Taylor T. Johnson
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez 等
An abstract domain for certifying neural networks
Gagandeep Singh, T. Gehr, Markus Püschel 等
Proof Minimization in Neural Network Verification
Omri Isac, Idan Refaeli, Haoze Wu 等
Dermatologist-level classification of skin cancer with deep neural networks
A. Esteva, Brett Kuprel, R. Novoa 等
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Haoze Wu, Omri Isac, Aleksandar Zelji'c 等
Satisfiability modulo theories
Leonardo Mendonça de Moura, Nikolaj S. Bjørner
Neural Network Verification with Proof Production
Omri Isac, Clark W. Barrett, M. Zhang 等
Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing
Y. Elboher, Raya Elsaleh, Omri Isac 等
Delivering Trustworthy AI through Formal XAI
Joao Marques-Silva, Alexey Ignatiev
Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks
Shahaf Bassan, Guy Katz
Global optimization of objective functions represented by ReLU networks
C. Strong, Haoze Wu, Aleksandar Zelji'c 等
Compositional Verification for Autonomous Systems with Deep Learning Components
C. Păsăreanu, D. Gopinath, Huafeng Yu