Nondeterminism-Aware Optimistic Verification for Floating-Point Neural Networks

TL;DR

NAO addresses verifiable neural-network inference under floating-point nondeterminism on heterogeneous hardware by combining portable IEEE-754 bounds with tight empirical per-operator error percentiles. It localizes disputes through a Merkle-anchored, four-phase protocol and resolves leaf disagreements with either a fast theoretical bound check or a small honest-majority committee against empirical thresholds, enabling vendor-agnostic verification with minimal overhead. Empirical results across ResNet-152, BERT-large, Qwen-8B, and Stable Diffusion on A100/H100/RTX GPUs show empirical thresholds are 10^2–10^3× tighter than worst-case theory and yield 0% attack success under tested threat models, with modest on-chain costs. NAO preserves native GPU kernels and performance while delivering scalable, auditable accountability for real-world ML compute in open-model settings.

Abstract

Neural networks increasingly run on hardware outside the user's control (cloud GPUs, inference marketplaces). Yet ML-as-a-Service reveals little about what actually ran or whether returned outputs faithfully reflect the intended inputs. Users lack recourse against service downgrades (model swaps, quantization, graph rewrites, or discrepancies like altered ad embeddings). Verifying outputs is hard because floating-point(FP) execution on heterogeneous accelerators is inherently nondeterministic. Existing approaches are either impractical for real FP neural networks or reintroduce vendor trust. We present NAO: a Nondeterministic tolerance Aware Optimistic verification protocol that accepts outputs within principled operator-level acceptance regions rather than requiring bitwise equality. NAO combines two error models: (i) sound per-operator IEEE-754 worst-case bounds and (ii) tight empirical percentile profiles calibrated across hardware. Discrepancies trigger a Merkle-anchored, threshold-guided dispute game that recursively partitions the computation graph until one operator remains, where adjudication reduces to a lightweight theoretical-bound check or a small honest-majority vote against empirical thresholds. Unchallenged results finalize after a challenge window, without requiring trusted hardware or deterministic kernels. We implement NAO as a PyTorch-compatible runtime and a contract layer currently deployed on Ethereum Holesky testnet. The runtime instruments graphs, computes per-operator bounds, and runs unmodified vendor kernels in FP32 with negligible overhead (0.3% on Qwen3-8B). Across CNNs, Transformers and diffusion models on A100, H100, RTX6000, RTX4090, empirical thresholds are $10^2-10^3$ times tighter than theoretical bounds, and bound-aware adversarial attacks achieve 0% success. NAO reconciles scalability with verifiability for real-world heterogeneous ML compute.

Figures (7)

• Figure 1: Tolerance-aware optimistic verification on two example tasks.Left: Using LLM agents for automated transaction Honest proposer ($y_0$) returns the correct destination: 0xA173****d422, amount: 0.01. Malicious ($y_1$) applies unbounded node-wise perturbations and outputs an absurd amount to send (rejected). ($y_2$) stays within IEEE-754 worst-case bounds but violates empirical thresholds (slashed). ($y_3$) fits both bounds (accepted). Right: Image classification the honest proposer outputs "Cat", while three similar types of malicious proposers output "Rock" (rejected), "Rabbit" (rejected), and "Cat" (accepted). Middle: tolerance-aware check. Malicious proposers inject perturbations after each operator. Results are rejected if they fall outside IEEE-754 theoretical bounds or empirical thresholds, while bounded, no explicit deviations are accepted. ($\oplus$: post-operator add)
• Figure 2: Mean empirical errors vs. normalized operator position (log-scale y-axis). The x-axis follows the canonical topological order. Profiles remain essentially flat with localized spikes, indicating limited room for attack.
• Figure 3: NAO overview. Phase 0 (Model Setup): model owner commits to weights, graph, empirical error percentile thresholds, and per-operator trace schema. Phase 1 (Optimistic Execution): proposer posts a commitment for $(x,y)$. Phase 2 (Dispute Localization): an $N$-way, Merkle-anchored dispute game recursively narrows disagreement to a single operator following a canonical partition policy. Phase 3 (Single-Operator Adjudication): either a sound IEEE-754 error-bound check or a committee vote against empirical thresholds decides the outcome, triggering payment or slashing.
• Figure 4: Comparison between deterministic and probabilistic theoretical error bounds for different operator types in Qwen-8B and BERT-large.
• Figure 5: Normalized margin change on failed attacks ($\alpha{=}1$). Empirical thresholds yield near-zero progress across models; theoretical bounds(p) show heavier tails for the LLM. Numbers above boxes show sample sizes.