Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2512.24379 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917177738657792 |
|---|---|
| author | Gokavarapu, Chandrasekhar |
| author_facet | Gokavarapu, Chandrasekhar |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_24379 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Incremental Certificate Learning for Hybrid Neural Network Verification . A Solver Architecture for Piecewise-Linear Safety Queries Gokavarapu, Chandrasekhar Rings and Algebras 68T07, 68N30, 68Q60, 90C05, 90C25 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. |
| title | Incremental Certificate Learning for Hybrid Neural Network Verification . A Solver Architecture for Piecewise-Linear Safety Queries |
| topic | Rings and Algebras 68T07, 68N30, 68Q60, 90C05, 90C25 |
| url | https://arxiv.org/abs/2512.24379 |