发表机构
Amherst College; University of Illinois Urbana-Champaign; Hebrew University of Jerusalem; Stanford University（阿默斯特学院; 伊利诺伊大学厄巴纳-香槟分校; 耶路撒冷希伯来大学; 斯坦福大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究神经网络验证中前瞻分支策略，提出通用集成方法，以FSB为例说明，还阐述其能生成加速验证的引理，通过在两个验证器中实例化，实现验证时间加速及解决实例数增加。
AI 中文摘要
在这项工作中，我们研究了前瞻分支策略在神经网络验证中的作用。我们提出了一种将前瞻集成到任何分支定界验证器中的通用方法，并展示了当前最先进的分支启发式算法之一FSB如何可被视为前瞻分支策略的一种特殊实例。我们还描述了除提高分支决策质量外，前瞻如何能生成加速验证的附加引理。我们在两个基于分支定界的代表性验证器（Marabou和α-β-CROWN）中实例化该方法，证明前瞻能使验证时间持续加速，且解决实例数量最多增加57%。代码可在指定网址获取。
英文摘要
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.
CommentsAccepted to IJCAI 2026. Lookahead branching is part of the Marabou and $α$-$β$-CROWN verifiers
