神经网络形式验证中基于抽象的证明生成

现代深度神经网络（DNN）验证工具越来越多地依赖抽象技术以扩展到真实架构。同时，证明生成正成为提高 DNN 验证结果可靠性的关键需求。然而，当前的证明生成验证器不支持基于抽象的推理，在可扩展性和可证明保证之间造成了鸿沟。我们通过引入一种新颖的基于抽象的 DNN 验证证明生成框架来解决这一鸿沟。我们的方法将验证任务模块化地分为两个部分：（i）证明抽象网络的正确性，以及（ii）证明抽象相对于原始 DNN 的合理性。前者可以由现有的证明生成验证器处理，而后者我们提出了首个生成形式化证明的方法。这项初步工作旨在通过在形式化证明框架中支持常见的抽象技术，实现可扩展且可信赖的验证。