用伊辛模型精确验证神经网络抗扰能力，效率远超传统方法。
Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solvers
- 将神经网络转为伊辛模型，对分段线性激活实现精确完整验证。
- 对一般激活函数采用渐进逼近法，分割越细结果越接近真实极值。
- 结合剪枝与压缩技术，大幅降低计算所需自旋变量数量，适合实际部署。
本文提出一种适配伊辛求解器的神经网络鲁棒性形式化验证框架，针对有界输入扰动场景。对于分段线性激活函数，提出精确对数型分段线性模型（Log-PWL），在信息论最优对数编码下实现完全、保真、精确的建模，将每神经元二进制变量从线性降至最小对数复杂度。对于一般有界逐元素激活函数，提出渐进阶梯包络模型（Step-Env），使用保真的分段常数包络，其上下界状态作为耦合对抗输入的决策变量。证明该模型在分段宽度趋近零时，全局优化输出边界一致收敛于真实网络极值，实现验证的渐近完备性。进一步设计了基于贝德尔分解的混合求解器，利用赫利冲突压缩理论避免指数级切割爆炸；结合区间剪枝、剪枝后证书转移及层间经典-伊辛划分，显著降低自旋需求。实验表明：分段线性网络可实现精确认证，而对数列网络在紧凑自旋预算下达到近参考精度。
原文摘要 · Abstract (English)
We present an Ising-compatible framework for formal neural-network robustness verification under bounded input perturbations. For piecewise-linear activations, the Exact Logarithmic PWL Model (Log-PWL) provides an exact, sound, and complete formulation with a state-optimal logarithmic encoding, reducing the binary variables per neuron from linear to information-theoretically minimal logarithmic complexity. For general bounded element-wise activations, the Asymptotic Step-Envelope Model (Step-Env) uses sound piecewise-constant envelopes whose lower and upper neuron states remain decision variables coupled to a common adversarial input. We prove that its globally optimized output bounds converge uniformly to the true network extrema as the segment width vanishes, yielding asymptotic completeness of verification. We further develop a hybrid Benders solver with output-sensitive iteration bounds, leveraging a Helly-based conflict compression theory to avoid generic exponential cut explosion. Interval pruning, certificate transfer for pruned networks, and layerwise classical--Ising partitioning further reduce spin requirements. Experiments show exact certification fidelity for piecewise-linear networks and near-reference accuracy for sigmoid networks with compact spin budgets.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。