Incremental Certificate Learning for Hybrid Neural Network Verification . A Solver Architecture for Piecewise-Linear Safety Queries

TL;DR

This paper introduces an incremental certificate learning approach for neural network verification that combines relaxation techniques with selective exact reasoning, improving efficiency in verifying piecewise-linear safety properties.

Contribution

It proposes a novel solver architecture that integrates incremental learning, lemma reuse, and selective exact checks for efficient neural network verification.

Findings

Effective pruning of verification search space.

Reusability of learned lemmas accelerates verification.

Selective exactness reduces computational overhead.

Abstract

Formal verification of deep neural networks is increasingly required in safety-critical domains, yet exact reasoning over piecewise-linear (PWL) activations such as ReLU suffers from a combinatorial explosion of activation patterns. This paper develops a solver-grade methodology centered on \emph{incremental certificate learning}: we maximize the work performed in a sound linear relaxation (LP propagation, convex-hull constraints, stabilization), and invoke exact PWL reasoning only through a selective \emph{exactness gate} when relaxations become inconclusive. Our architecture maintains a node-based search state together with a reusable global lemma store and a proof log. Learning occurs in two layers: (i) \emph{linear lemmas} (cuts) whose validity is justified by checkable certificates, and (ii) \emph{Boolean conflict clauses} extracted from infeasible guarded cores, enabling DPLL(T)-style pruning across nodes. We present an end-to-end algorithm (ICL-Verifier) and a companion hybrid pipeline (HSRV) combining relaxation pruning, exact checks, and branch-and-bound splitting. We prove soundness, and we state a conditional completeness result under exhaustive splitting for compact domains and PWL operators. Finally, we outline an experimental protocol against standardized benchmarks (VNN-LIB / VNN-COMP) to evaluate pruning effectiveness, learned-lemma reuse, and exact-gate efficiency.