基于浮点执行的 Lipschitz 鲁棒性认证

灵敏度-based 鲁棒性认证已成为 certifying neural network 鲁棒性的实用方法，包括需要可验证保证的情境。其关键优势在于认证通过具体数值计算完成（而非符号推理），且随网络规模而高效扩展。然而，与大多数关于鲁棒性认证和验证的先前工作一样，这些方法的 soundness 通常相对于假设精确实算术的语义模型进行证明。实际部署的神经网络实现时使用浮点算术。这种不匹配在已认证鲁棒性属性和执行系统行为之间创造了语义鸿沟。作为佐证，我们展示具体反例，表明即使对于已验证的 certifier，实算术鲁棒性保证在浮点执行下也会失败。 在低精度格式（如 float16）下，差异尤为显著；在受对抗性构造模型影响的 float32 下，差异也达到语义上有意义的扰动半径。我们随后发展了一种正式的、可组合的理论，将实算术 Lipschitz-based 灵敏度界关联到浮点执行的灵敏度，专为具有 ReLU 激活函数的前馈神经网络进行了特殊化。我们推导出浮点执行下的鲁棒性 sound 条件，包括证书退化的界限以及不存在溢出的充分条件。我们形式化了该理论及其主要 soundness 结果，并实现了一个基于这些原则的可执行 certifier，该 certifier 在实证评估中证明了其实用性。