返回
Proof Minimization in Neural Network Verification
DOI:10.1007/978-3-032-15700-3_6.png)
摘要
En 中文
深度神经网络的广泛应用需要高效的技术来验证其安全性。DNN验证器是复杂的工具,可能包含会破坏其正确性并削弱验证过程可靠性的错误。这一担忧可以通过证明来缓解:证明是可由外部可靠证明检查器检查的工件,并证明验证过程的正确性。然而,此类证明往往极其庞大,限制了其在许多场景中的使用。在本工作中,我们通过最小化DNN验证器生成的不可满足性证明来解决此问题。我们提出了移除在验证过程中学习但本身对证明不必要的结论的算法。概念上,我们的方法分析用于推导UNSAT的结论之间的依赖关系,并移除未做出贡献的结论。然后,我们进一步通过两种替代程序消除剩余的不必要依赖关系,以最小化证明。我们在一个产生证明的DNN验证器上实现了我们的算法,并在多个基准测试中进行了评估。结果表明,我们表现最佳的算法将证明大小减少了37%-82%,证明检查时间减少了30%-88%,同时为验证过程本身引入了7%-20%的运行时开销。
Keyword:
Neural Network Verification
Proof Minimization
Unsatisfiability Proofs
DNN Verifiers
Proof Checking
期刊
V

