ReLU networks are piecewise-linear (PWL), enabling exact symbolic verification via \SMT(\LRA) or \MILP. However, safety claims in certification pipelines require not only correctness but also \emph{checkable evidence}. We develop a proof-carrying verification core for PWL neural constraints: (i) we formalize ReLU networks as unions of polyhedra indexed by activation patterns; (ii) we present exact \SMT/\MILP encodings and the canonical convex-hull relaxation for each bounded ReLU; and (iii) we introduce a certificate calculus in which bound tightening, stabilization, strengthening, and pruning steps emit explicit algebraic witnesses (LP dual multipliers and Farkas infeasibility certificates). Crucially, these witnesses are \emph{symbolic objects} that admit independent verification in exact arithmetic over $\Q$. We provide a symbolic certificate checker, normalization rules that preserve validity, and a compositional view of region-wise certificates as a global proof artifact for universal safety.

翻译：ReLU网络具有分段线性特性，可通过SMT(LRA)或MILP实现精确符号验证。然而，认证流程中的安全性声明不仅要求正确性，更需要可检验的证据支撑。本文为分段线性神经约束开发了一个证明携带式验证核心：(i) 将ReLU网络形式化为按激活模式索引的多面体并集；(ii) 针对每个有界ReLU提出精确的SMT/MILP编码及标准凸包松弛方法；(iii) 构建证书演算体系，使边界紧缩、稳定性优化、约束强化与剪枝步骤能生成显式代数见证（LP对偶乘子与Farkas不可行性证书）。关键的是，这些见证作为符号对象支持在Q上的精确算术独立验证。我们提供了符号证书检查器、保持有效性的规范化规则，以及将区域化证书组合为全局安全性证明的复合视角。