AI 中文总结
本文提出一种前瞻驱动的神经网络验证内处理框架，将其应用于Marabou和α-β-CROWN两款验证器，可提升性能，最多多证明34%的不可满足实例。
AI 中文摘要
当前最先进的神经网络验证器以分支定界法为核心求解机制。本文提出一种由前瞻过程驱动的神经网络验证内处理框架，该框架中，前瞻过程会在不稳定ReLU阶段推导新引理，这些引理会被收集到蕴含图中，用于剪枝搜索空间并激活布尔割。我们将该框架实例化到Marabou和α-β-CROWN这两款最先进的验证器中，结果表明其提升了两者的性能，最多可多证明34%的不可满足实例。
英文摘要
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.
