Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Note on Non-Composability of Layerwise Approximate Verification for Neural Inference

Or Zamir

TL;DR

The paper demonstrates that simple layerwise delta-consistency checks for floating-point neural inference do not guarantee a correct final output, by constructing a functionally equivalent network F' that admits delta-consistent transcripts steering the final result to any target z with ||z||_infty ≤ R. It provides a concrete trigger-channel construction that widens hidden layers and augments the final layer so that exact inference matches F while allowing adversarial perturbations to accumulate and control the final output under delta-consistency. The key contribution is a rigorous demonstration that layerwise approximate verification is not inherently composable, highlighting the need for stability assumptions or protocol-level reasoning about error propagation in zk-ML. Practically, this warns against assuming naive per-layer checks suffice for verifiable ML inference and urges careful design of threat models and verification protocols that consider adversarially structured networks.

Abstract

A natural and informal approach to verifiable (or zero-knowledge) ML inference over floating-point data is: ``prove that each layer was computed correctly up to tolerance $δ$; therefore the final output is a reasonable inference result''. This short note gives a simple counterexample showing that this inference is false in general: for any neural network, we can construct a functionally equivalent network for which adversarially chosen approximation-magnitude errors in individual layer computations suffice to steer the final output arbitrarily (within a prescribed bounded range).

A Note on Non-Composability of Layerwise Approximate Verification for Neural Inference

TL;DR

The paper demonstrates that simple layerwise delta-consistency checks for floating-point neural inference do not guarantee a correct final output, by constructing a functionally equivalent network F' that admits delta-consistent transcripts steering the final result to any target z with ||z||_infty ≤ R. It provides a concrete trigger-channel construction that widens hidden layers and augments the final layer so that exact inference matches F while allowing adversarial perturbations to accumulate and control the final output under delta-consistency. The key contribution is a rigorous demonstration that layerwise approximate verification is not inherently composable, highlighting the need for stability assumptions or protocol-level reasoning about error propagation in zk-ML. Practically, this warns against assuming naive per-layer checks suffice for verifiable ML inference and urges careful design of threat models and verification protocols that consider adversarially structured networks.

Abstract

A natural and informal approach to verifiable (or zero-knowledge) ML inference over floating-point data is: ``prove that each layer was computed correctly up to tolerance ; therefore the final output is a reasonable inference result''. This short note gives a simple counterexample showing that this inference is false in general: for any neural network, we can construct a functionally equivalent network for which adversarially chosen approximation-magnitude errors in individual layer computations suffice to steer the final output arbitrarily (within a prescribed bounded range).
Paper Structure (6 sections, 1 theorem, 13 equations)

This paper contains 6 sections, 1 theorem, 13 equations.

Table of Contents

  1. Introduction
  2. Model: layerwise approximate verification
  3. Construction: exact equivalence, arbitrary approximate outputs
  4. Construction.
  5. Proof of Theorem \ref{['thm:steer']}.
  6. Takeaway

Key Result

Theorem 1

Fix the activation $\sigma=\mathrm{ReLU}$ on hidden layers and let the final layer be linear. Fix any network $F=(A_1,\dots,A_k)$ with width $\bar{m}$, output dimension $m$, weight bound $g>1$, output bound $R>0$, and any tolerance $\delta>0$. Here output bound $R$ means that for all inputs $x$ unde Consequently, verifying each layer "up to $\delta$" does not imply that the verified output is clos

Theorems & Definitions (3)

  • Definition 1: Layerwise $\delta$-consistency
  • Theorem 1: Universal steering under layerwise $\delta$-checks
  • Remark 1: Parameter choices