让神经网络验证既快速又可信，首次实现抽象推理的正式证明。
Abstraction-Based Proof Production in Formal Verification of Neural Networks
- 分两步验证：先证抽象网络正确，再证抽象过程无误。
- 首次支持在形式证明中使用常见抽象技术，兼顾速度与可靠性。
- 适合需要高可信度验证的工业级神经网络应用。
当前深度神经网络（DNN）验证工具越来越依赖抽象技术以扩展到实际架构。同时，生成可验证的证明已成为提升验证结果可信度的关键需求。然而，现有支持证明生成的验证器不支持基于抽象的推理，导致可扩展性与形式保证之间存在差距。本文提出一种新型框架，实现基于抽象的、可生成证明的DNN验证。方法将验证任务模块化为两个部分：(i) 证明抽象网络的正确性，(ii) 证明抽象相对于原始DNN的保真性。前者可由现有证明生成验证器处理，而后者我们提出了首个生成正式证明的方法。本初步工作旨在通过在形式证明框架内支持常见抽象技术，实现高效且可信的验证。
原文摘要 · Abstract (English)
Modern verification tools for deep neural networks (DNNs) increasingly rely on abstraction to scale to realistic architectures. In parallel, proof production is becoming a critical requirement for increasing the reliability of DNN verification results. However, current proofproducing verifiers do not support abstraction-based reasoning, creating a gap between scalability and provable guarantees. We address this gap by introducing a novel framework for proof-producing abstraction-based DNN verification. Our approach modularly separates the verification task into two components: (i) proving the correctness of an abstract network, and (ii) proving the soundness of the abstraction with respect to the original DNN. The former can be handled by existing proof-producing verifiers, whereas we propose the first method for generating formal proofs for the latter. This preliminary work aims to enable scalable and trustworthy verification by supporting common abstraction techniques within a formal proof framework.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。