Jul 2026· Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence· Vol abs/2607.17290· 1 citation· 24 references
Computer Science
TL;DR
This work presents a general recipe to integrate lookahead into any branch-and-bound verifier and demonstrates how one of the current state-of-the-art branching heuristics, FSB, can be viewed as a special instantiation of the lookahead branching strategy.
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.
Neural network verification has become a key tool for providing formal guarantees on the behaviour of neural networks. However, many verification problems remain computationally intractable in the worst case: even for common adversarial robustness specifications, verification is NP-complete. Here, we explore the applic...
Annelot W. Bosman, Ming-Hao Liu, Marta Z. Kwiatkowska et al.· 0 citations
SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously quickly produced proof to fail or time out. This paper addresses a common cause of outcome instability (i.e., unsat/unknown fluctuations) i...
Can Cebeci, Nikolaj S. Bjørner, George Candea et al.· 0 citations
A branch-and-bound framework to mitigate the issue of verifying relational specifications against relational specifications, which iteratively splits the problem until all sub-problems are verified, and devise a relational neuron selection strategy based on the dual formulation of the verification problem.
Kota Fukuda, Zhen-Ya Zhang, Guan-Qin Zhang et al.· 0 citations
The software status quo is to use one system to process many different kinds of inputs. In contrast, we propose hyperspecialization: creating new software that is optimized for a single class of inputs. Hyperspecializing manually is anywhere from expensive to impossible. We conjecture that coding agents make automated...
Harrison Green, Claire Le Goues, Fraser Brown· 0 citations
VeRe is proposed, a verification-guided repair framework that leverages linear relaxation to precisely and efficiently estimate the repair significance of neurons and synthesizes ideal intervals that provide sound guarantees for correct behaviors, thereby facilitating surgical and targeted adjustments of neuron paramet...
Jia-Nan Ma, Wei Chen, Pengfei Yang et al.· ACM Transactions on Software...· 0 citations
Natural-language descriptions of optimization problems may be incomplete or vague about numerical information that a solver requires, including costs, capacities, demands, bounds, and penalties. A language model can translate the description into code, but when a required value is absent it must either stop or guess. W...
Shaghayegh Sadeghi, Steve Smith, D. C. Del Rey Fernández· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
