arrow
返回

Proof Minimization in Neural Network Verification

delete2026-01-01
delete0
PRE
AI
O
Omri Isac *
I
Idan Refaeli
H
Haoze Wu
C
C. BARRETT
G
Guy Katz
DOI:10.1007/978-3-032-15700-3_6delete
delete原文链接
delete原文求助
delete分享
delete收藏
摘要

摘要

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

期刊

V
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2026
IF:
0
论文数:
18
被引数:
0

机构

A
amherst college
学者数:
102
论文数: 72
被引数: 0
S
stanford university
学者数:
1.1W
论文数: 4.3K
被引数: 0
H
hebrew university of jerusalem
学者数:
2.5K
论文数: 1.1K
被引数: 0
学者 查看更多机构
引用论文

引用论文

err分享
err收藏
err分享
err收藏
err分享
err收藏
Towards a Certified Proof Checker for Deep Neural Network Verification
err2023-01-01
err0
PREAI
errDesmartin,Remi; Isac,Omri; Passmore,Grant; Stark,Kathrin; Komendantskaya,Ekaterina; Katz,Guy
err分享
err收藏
AI in health and medicineAI在健康和医学
err2022-01-20
err859
PREAI
errRajpurkar, Pranav; Chen, Emma; Banerjee, Oishi; Topol, Eric J.
err分享
err收藏
Reluplex: a calculus for reasoning about deep neural networks
err2021-07-01
err0
PREAI
errGuy Katz; Clark Barrett; David L. Dill; Kyle Julian; Mykel J. Kochenderfer
err分享
err收藏
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation
err2018-05-01
err0
errOAAI
errTimon Gehr; Matthew Mirman; Dana Drachsler-Cohen; Petar Tsankov; Swarat Chaudhuri; Martin Vechev
err分享
err收藏
Verification of Deep Convolutional Neural Networks Using ImageStars
err2020-07-14
err0
errOAAI
errHoang-Dung Tran; Stanley Bak; Weiming Xiang; Taylor T. Johnson
err分享
err收藏
学者 查看更多内容