压缩神经网络验证的证明文件，让检查更快更省资源。
Proof Minimization in Neural Network Verification
- 分析验证过程中各事实的依赖关系，移除无关信息
- 证明大小减少37%-82%，检查时间缩短30%-88%
- 适合需要可信验证结果的研究者与安全关键系统开发者
深度神经网络（DNN）的广泛应用要求高效的验证技术以确保其安全性。然而，DNN验证器本身结构复杂，可能含有漏洞，影响验证结果的可靠性。使用可被外部验证器检查的证明文件可以缓解这一问题，但这些证明通常体积庞大，限制了实际应用。本文提出一种最小化由DNN验证器生成的不可满足性证明的方法，通过移除验证过程中学习到但对证明无用的事实。概念上，该方法分析事实间的依赖关系，剔除未贡献于结论的成分，并进一步通过两种不同策略消除剩余冗余依赖。我们在一个支持生成证明的DNN验证器上实现该算法，在多个基准测试中评估。结果表明，最优算法使证明规模减小37%-82%，检查时间缩短30%-88%，且验证过程仅增加7%-20%运行开销。
原文摘要 · Abstract (English)
The widespread adoption of deep neural networks (DNNs) requires efficient techniques for verifying their safety. DNN verifiers are complex tools, which might contain bugs that could compromise their soundness and undermine the reliability of the verification process. This concern can be mitigated using proofs: artifacts that are checkable by an external and reliable proof checker, and which attest to the correctness of the verification process. However, such proofs tend to be extremely large, limiting their use in many scenarios. In this work, we address this problem by minimizing proofs of unsatisfiability produced by DNN verifiers. We present algorithms that remove facts which were learned during the verification process, but which are unnecessary for the proof itself. Conceptually, our method analyzes the dependencies among facts used to deduce UNSAT, and removes facts that did not contribute. We then further minimize the proof by eliminating remaining unnecessary dependencies, using two alternative procedures. We implemented our algorithms on top of a proof producing DNN verifier, and evaluated them across several benchmarks. Our results show that our best-performing algorithm reduces proof size by 37%-82% and proof checking time by 30%-88%, while introducing a runtime overhead of 7%-20% to the verification process itself.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。