Proof-Carrying Verification for ReLU Networks via Rational Certificates

TL;DR

This paper introduces a proof-carrying verification method for ReLU neural networks that uses rational certificates to ensure the trustworthiness of safety claims, providing an exact and certified reasoning framework.

Contribution

It develops a formal proof core with rational certificates for verifying PWL neural constraints, bridging SMT/MILP encodings with exact proof checking.

Findings

Certificates validate linear consequences and infeasibility in rational arithmetic.

The proof kernel is sound and complete for entailment, ensuring reliable verification.

End-to-end examples demonstrate certified reasoning without solver trust.

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.