提出前瞻分支策略，显著提升神经网络验证效率
Lookahead Branching for Neural Network Verification
- 将前瞻思想融入分支定界验证器，优化分支决策
- 在两个主流验证器上实现验证速度提升，最多多解决57%实例
- 适合关注神经网络形式化验证的研究者
本文研究了前瞻分支策略在神经网络验证中的作用。我们提出一种通用方法，可将前瞻机制集成到任意分支定界验证器中，并表明当前最先进的分支启发式算法FSB可视为前瞻分支策略的特例。此外，前瞻不仅提升分支决策质量，还能生成额外引理以加速验证过程。我们在两种代表性分支定界验证器（Marabou 和 α-β-CROWN）中实现了该方法，实验表明其在验证时间上持续提速，最多可多解决57%的实例。代码已公开于 https://github.com/ai-ar-research/lookahead-branching。
原文摘要 · Abstract (English)
In this work, we investigate the effect of lookahead branching strategies in neural network verification. We present a general recipe to integrate lookahead into any branch-and-bound verifier and demonstrate how one of the current state-of-the-art branching heuristics, FSB, can be viewed as a special instantiation of the lookahead branching strategy. We also describe how, in addition to improving the quality of branching decisions, lookahead can generate additional lemmas that accelerate verification. We instantiate the method in two representative branch-and-bound-based verifiers (Marabou and $α$-$β$-CROWN), and demonstrate that lookahead leads to consistent speedups in verification time and up to $57\%$ more solved instances. Code is available at https://github.com/ai-ar-research/lookahead-branching.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。