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.
This work explores the application of solver-level warmstarting for neural network verification to exploit information from previous solutions, using a pipeline that is generalisable and potentially adaptable to state-of-the-art verifiers.
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
This paper explores one such problem, SAT solving, by synthesizing hundreds of workload-specific SAT solvers at an average cost of $37 each, and conjecture that coding agents make automated hyperspecialization cheap, effective, and safe for problems with measurable performance and checkable output.
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
SAILOR, a proof-of-concept system that detects such unsupported numerical choices, asks the user targeted follow-up questions, and updates the optimization model before returning a solution, is presented.
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.
