本文提出了一种基于差分区域集（differential halo zonotopes）的新型静态分析技术，用于验证深度神经网络（DNN）的全局鲁棒性。全局鲁棒性是一种比局部鲁棒性更强的性质，要求网络对所有输入对（而非单个输入及其邻域）的预测结果一致，因而属于2-安全属性（2-safety property），验证难度极大。现有方法多局限于局部鲁棒性验证，或在大规模网络上难以扩展。作者的核心创新在于：将区域集（zonotopes）抽象域扩展为差分区域集，能够同步联合传播扰动输入对，同时紧密地限定其输出差异的边界。此外，本文引入了对称的置信度基全局鲁棒性松弛版本，忽略因低置信度预测而产生的差异，从而在保持实用性的前提下放宽了验证条件，适用于更广泛的网络架构。作者实现了原型工具TwoSafe，并在标准DNN验证基准（包含广泛部署的模型）上进行了评估。实验结果表明，TwoSafe在精度和可扩展性方面均显著优于现有技术，能够验证的网络规模比先前技术大一个数量级。该工作不仅推进了形式化验证的理论边界，也为安全关键场景下DNN的可靠性提供了实用验证手段。