Lookahead Branching for Neural Network Verification

Davis, Liam; Zhou, Duo; Zhang, Huan; Katz, Guy; Barrett, Clark; Wu, Haoze

doi:10.24963/ijcai.2026/59

Lookahead Branching for Neural Network Verification

Liam Davis, Duo Zhou, Huan Zhang, Guy Katz, Clark Barrett, Haoze Wu

Download BibTeX Cite

Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence. Main Track. Pages 518-526.

https://doi.org/10.24963/ijcai.2026/59

Keywords

AI Ethics, Trust, Fairnes: Safety and robustness
AI Ethics, Trust, Fairnes: Trustworthy AI

Abstract

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.

Liam Davis, Duo Zhou, Huan Zhang, Guy Katz, Clark Barrett, and Haoze Wu. 2026. Lookahead Branching for Neural Network Verification. In Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26. IJCAI, 518–526. https://doi.org/10.24963/ijcai.2026/59

@inproceedings{ijcai2026p59,
  title     = {Lookahead Branching for Neural Network Verification},
  author    = {Davis, Liam and Zhou, Duo and Zhang, Huan and Katz, Guy and Barrett, Clark and Wu, Haoze},
  booktitle = {Proceedings of the Thirty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-26}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Diego Calvanese},
  pages     = {518--526},
  year      = {2026},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2026/59},
  url       = {https://doi.org/10.24963/ijcai.2026/59},
}

TY  - CPAPER
TI  - Lookahead Branching for Neural Network Verification
AU  - Davis, Liam
AU  - Zhou, Duo
AU  - Zhang, Huan
AU  - Katz, Guy
AU  - Barrett, Clark
AU  - Wu, Haoze
T2  - Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2026
SP  - 518
EP  - 526
DO  - 10.24963/ijcai.2026/59
UR  - https://doi.org/10.24963/ijcai.2026/59
ER  -