通过前瞻推导新结论，提升神经网络验证效率
Learning Lookahead Lemmas for Neural Network Verification
- 利用前瞻机制动态生成不稳定ReLU的逻辑结论
- 在两个主流验证器上使不可满足实例数提升34%
- 适合需要高效验证神经网络的科研与工程人员
当前先进的神经网络验证器以分支定界法为核心求解机制。本文提出一种基于前瞻过程的内处理框架，通过在不稳定ReLU阶段推导新的逻辑引理，并将其汇总到蕴含图中，用于剪枝搜索空间并激活布尔切割。该框架在两款前沿验证器Marabou和α-β-CROWN中实现，实验表明性能显著提升，在相同时间内可证明最多34%的额外不可满足实例。
原文摘要 · Abstract (English)
State-of-the-art neural network verifiers use the branch-and-bound procedure as their core solving mechanism. We introduce an inprocessing framework for neural network verification driven by the lookahead procedure. Under this framework, lookahead derives new lemmas over the phases of unstable ReLUs, which are collected into an implication graph that is used to prune the search space and vivify boolean cuts. We instantiate the framework in two state-of-the-art verifiers, Marabou and $α$-$β$-CROWN, and demonstrate that it improves performance in both, proving up to 34% more instances unsatisfiable.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。