Proof Minimization in Neural Network Verification
Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, Guy Katz
深度神经网络(DNN)的广泛采用需要验证其安全性的有效技术。 DNN验证器是复杂的工具,可能包含可能损害其健全性并破坏验证过程可靠性的bug。 使用证明可以减轻这种担忧:由外部和可靠的证明检查器可检查的工件,并证明验证过程的正确性。 然而,这种证明往往非常大,限制了它们在许多情况下的使用。 在这项工作中,我们通过最小化DNN验证器产生的不满足性证明来解决这个问题。 我们提出了删除在验证过程中学到的事实的算法,但对于证明本身来说是不必要的。 从概念上讲,我们的方法分析了用于推断UNSAT的事实之间的依赖关系,并删除没有贡献的事实。 然后,我们通过使用两个替代程序,消除剩余的不必要的依赖关系,进一步最小化了证明。 我们在生成 DNN 验证器的证明之上实现了我们的算法,并在几个基准测试中对其进行了评估。 我们的结果表明,我们表现最佳的算法将证明大小减少了37%-82%,验证检查时间减少了30%-88%,同时为验证过程本身引入了7%-20%的运行时开销。
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, li...
