面向混合神经网络验证的增量证书学习：一种用于分段线性安全性查询的求解器架构
环与代数
2026-01-01 v1
摘要
深度神经网络的形式化验证在安全关键领域中日益必要，然而对ReLU等分段线性（PWL）激活函数的精确推理会遭遇激活模式组合爆炸的问题。本文提出了一种以\emph{增量证书学习}为核心的求解器级方法：我们最大化在可靠的线性松弛（LP传播、凸包约束、稳定化）中所完成的工作，并仅在松弛结果不确定时，通过一个选择性的\emph{精确性门}调用精确的PWL推理。我们的架构维护一个基于节点的搜索状态，以及一个可复用的全局引理库和一个证明日志。学习发生在两个层面：（i）\emph{线性引理}（割平面），其有效性由可检查的证书证明；（ii）\emph{布尔冲突子句}，从不可行的保护核心中提取，支持跨节点的DPLL(T)风格剪枝。我们提出了一个端到端算法（ICL-Verifier）和一个配套的混合流程（HSRV），该流程结合了松弛剪枝、精确检查和分支定界分裂。我们证明了其可靠性，并陈述了在紧致域和PWL算子下穷举分裂的条件完备性结果。最后，我们概述了一个针对标准化基准（VNN-LIB / VNN-COMP）的实验方案，以评估剪枝有效性、学习引理的重用性以及精确性门的效率。
引用
@article{arxiv.2512.24379,
title = {Incremental Certificate Learning for Hybrid Neural Network Verification . A Solver Architecture for Piecewise-Linear Safety Queries},
author = {Chandrasekhar Gokavarapu},
journal= {arXiv preprint arXiv:2512.24379},
year = {2026}
}