为神经网络鲁棒性认证提供形式化验证，确保认证结果可信。
A Formally Verified Robustness Certifier for Neural Networks (Extended Version)
- 用Dafny语言实现并验证了全局鲁棒神经网络的认证函数。
- 发现此前未验证的实现存在可被利用的不严谨漏洞。
- 适合关注模型安全与形式化验证的研究者或工业应用。
神经网络对输入的微小扰动常敏感，易导致误分类。近期解决方案是采用全局鲁棒神经网络，通过认证函数确保输入分类不会因扰动而改变，通过认证的输出称为“已认证鲁棒”。然而，据作者所知，这些认证函数尚未在实现层面经过形式化验证。本文揭示了此前未验证的实现存在可被利用的不严谨性；且其常用近似算法（如幂迭代）并不保证正确性。为此，我们在Dafny中实现了并形式化验证了一个全局鲁棒神经网络的认证函数。文中描述了程序设计、规格说明及关键决策，并分享了实际应用中的经验。
原文摘要 · Abstract (English)
Neural networks are often susceptible to minor perturbations in input that cause them to misclassify. A recent solution to this problem is the use of globally-robust neural networks, which employ a function to certify that the classification of an input cannot be altered by such a perturbation. Outputs that pass this test are called certified robust. However, to the authors' knowledge, these certification functions have not yet been verified at the implementation level. We demonstrate how previous unverified implementations are exploitably unsound in certain circumstances. Moreover, they often rely on approximation-based algorithms, such as power iteration, that (perhaps surprisingly) do not guarantee soundness. To provide assurance that a given output is robust, we implemented and formally verified a certification function for globally-robust neural networks in Dafny. We describe the program, its specifications, and the important design decisions taken for its implementation and verification, as well as our experience applying it in practice.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。