用于混合神经网络验证的增量证书学习

本文解决了形式验证深度神经网络的挑战，特别是那些具有ReLU激活的神经网络，ReLU激活会带来组合爆炸问题。核心贡献是一种名为“增量证书学习”的求解器级方法，该方法战略性地结合了线性松弛、精确的分段线性推理和学习技术（线性引理和布尔冲突子句）以提高效率和可扩展性。该架构包括一个基于节点的搜索状态、一个可重用的全局引理存储和一个证明日志，从而实现 DPLL(T) 风格的剪枝。本文的重要性在于它有可能通过减少与精确推理相关的计算负担来改进对安全关键型 DNN 的验证。

• •提出了一种新的求解器架构，用于验证具有分段线性激活的深度神经网络。
• •采用“增量证书学习”来平衡线性松弛和精确推理。
• •利用学习到的引理和冲突子句进行有效剪枝。
• •提出了一种端到端算法（ICL-Verifier）和混合流水线（HSRV）。
• •旨在改进对安全关键型 DNN 的验证。