Proof-Carrying Verification for ReLU Networks via Rational Certificates
Chandrasekhar Gokavarapu
TL;DR
This work introduces a proof-carrying verification core for ReLU-based neural networks by formalizing exact piecewise-linear semantics as a union of activation-pattern polyhedra and linking them to exact SMT/LRA and MILP encodings. It provides a compositional certificate calculus with two rational certificate types—Farkas certificates for infeasibility and entailment certificates for validated propagation—and proves soundness, completeness for linear entailment via LP duality, and dimension-based sparsity for infeasibility proofs. A solver-agnostic pipeline exports small, checkable rational certificates that can be independently verified via exact arithmetic, enabling trustworthy UNSAT claims even when solvers are imperfect. The approach yields compact proof logs, supports stabilization and learned cuts, and demonstrates end-to-end certified reasoning through worked examples. The framework advances trustworthy, scalable, and verifiable AI safety verification for PWL networks, with potential extensions to nonlinear activations and richer specifications.
Abstract
Rectified Linear Unit (ReLU) networks are piecewise-linear (PWL), so universal linear safety properties can be reduced to reasoning about linear constraints. Modern verifiers rely on SMT(LRA) procedures or MILP encodings, but a safety claim is only as trustworthy as the evidence it produces. We develop a proof-carrying verification core for PWL neural constraints on an input domain $D \subseteq \mathbb{R}^n$. We formalize the exact PWL semantics as a union of polyhedra indexed by activation patterns, relate this model to standard exact SMT/MILP encodings and to the canonical convex-hull (ideal) relaxation of a bounded ReLU, and introduce a small certificate calculus whose proof objects live over $\mathbb{Q}$. Two certificate types suffice for the core reasoning steps: entailment certificates validate linear consequences (bound tightening and learned cuts), while Farkas certificates prove infeasibility of strengthened counterexample queries (branch-and-bound pruning). We give an exact proof kernel that checks these artifacts in rational arithmetic, prove soundness and completeness for linear entailment, and show that infeasibility certificates admit sparse representatives depending only on dimension. Worked examples illustrate end-to-end certified reasoning without trusting the solver beyond its exported witnesses.