神经网络验证的概率紧缩线性松弛扰动分析

于红博

摘要: 我们提出了概率紧致的基于线性松弛的扰动分析（PT-LiRPA），这是一个新颖的框架，将LiRPA-based方法的过估计技术与基于采样的方法结合起来，以计算紧致的中间可达集。具体来说，我们展示了PT-LiRPA利用估计的可达集，显著地紧缩了神经网络输出的下限和上限线性边界，降低了形式验证工具的计算成本，同时提供了验证完整性的概率保证。对标准形式验证基准进行了大量实验，包括国际神经网络验证竞赛，结果显示我们基于PT-LiRPA的验证器将模型所容忍的ε扰动的认证下限提高了最多3.31倍和2.26倍，相比相关工作。重要的是，我们的概率方法为具有挑战性的竞赛条目提供了有价值的解决方案，当最先进的形式验证方法失败时，允许我们提供至少99%的高置信度的答案。

更新时间: 2025-12-31 11:16:07

领域: cs.LG,cs.AI

下载: http://arxiv.org/abs/2507.05405v2