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.
Abstract
Verification of neural networks against relational specifications, such as global robustness, is crucial for safety-critical applications of cyber-physical systems (CPS), given their increasing adoption of AI components. Compared to simple trace properties (e.g., local robustness), verifying relational specifications requires reasoning about the relationship between multiple network inferences, which brings significant technical challenges. Existing research has explored abstraction techniques based on sound and convex over-approximation of neural network outputs; however, since these approaches are inherently incomplete and may raise false alarms, they further underscore the need of effective abstraction refinement. In this paper, we propose a branch-and-bound (BaB) framework to mitigate the issue, which iteratively splits the problem until all sub-problems are verified. Specifically, our BaB framework features splitting of relational neurons rather than individual neurons as prior works do, and as the core of our technique, we devise a relational neuron selection strategy based on the dual formulation of the verification problem, which allows us to efficiently select the (most likely) optimal relational neuron that maximizes the refinement brought by problem splitting. We evaluate SaBRe on 817 verification problems across ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB. The results show that SaBRe outperforms different baseline approaches, in terms of the number of solved instances and verification efficiency, which demonstrates the effectiveness of our proposed techniques.
This study shows that template subsumption rates can vary widely across scenarios, and presents FastCert, a novel technique for automatically distributing templates across neural network layers to increase performance impact, eschewing templates entirely if they are unlikely to produce a speedup.
Kanak Das, Shubham Ugare, B. E. Chang et al.· 0 citations
An inprocessing framework for neural network verification driven by the lookahead procedure is introduced, which derives new lemmas over the phases of unstable ReLUs, which are collected into an implication graph that is used to prune the search space and vivify boolean cuts.
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 parameters to rectify faulty behaviors.
Jia-Nan Ma, Wei Chen, Pengfei Yang et al.· ACM Transactions on Software...· 0 citations
Large-scale neural architectures exhibit systematic failures in compositional generalization and formal verifiability despite remarkable pattern recognition capabilities. This paper introduces the Neural-Symbolic-Verification (NSV) Loop–a functional decomposition framework–and uses it to systematically survey neuro-symbolic integration as a principled pathway toward artificial general intelligence. The NSV Loop organizes hybrid architectures through four computational stages structuring perception, symbolic execution, verification, and feedback. We operationalize the Grounding-Instructibility-Alignment (G-I-A) framework for production assessment and demonstrate quantifiable advantages: perfect compositional accuracy on SCAN (100% vs 13.8% neural baseline, length split), sample efficiency gains exceeding 10
$$\times $$
×
on visual reasoning tasks, and formal verification achieving certification rates above 95% with sub-100ms latency in autonomous systems. Analysis documents critical bottlenecks–grounding complexity scaling exponentially with entity count, cross-domain transfer exhibiting near-zero retention, and adversarial robustness evaluation remaining absent. The NSV+G-I-A framework enables systematic comparison manifesting when hybrid integration justifies complexity: safety-critical applications requiring formal guarantees, data-scarce environments, and compositional reasoning tasks. We establish clear capability boundaries distinguishing reliable improvements from speculative claims while proposing testable research directions with explicit validation protocols.
Safayat Bin Hakim, Kanchon Gharami, H. Wang et al.· Progress in Artificial Intel...· 0 citations
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 $\alpha$-$\beta$-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 et al.· arXiv.org· 1 citation
