about
Verifiable ML Without Determinism: Tolerance-Aware Optimistic Verification (arxiv.org)
1 point by cnyaojz 348 days ago | hide | past | pdf | 1 comment on HN

In plain words: To check a service ran the promised model, it accepts tiny floating-point differences instead of demanding exact matches, and when challenged splits the computation to a single step to judge the gap. Its measured limits are 100 to 1000 times tighter than worst-case bounds.

Abstract · TAO: Tolerance-Aware Optimistic Verification for Floating-Point Neural Networks

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 TAO: a Tolerance Aware Optimistic verification protocol that accepts outputs within principled operator-level acceptance regions rather than requiring bitwise equality. TAO 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 TAO 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. Together, TAO reconciles scalability with verifiability for real-world heterogeneous ML compute.

Jianzhu Yao, Hongxu Su, Taobo Liao, Zerui Cheng, Huan Zhang, Xuechao Wang, Pramod Viswanath
arXiv:2510.16028 · cs.CR, cs.AI, cs.LG, eess.SY · submitted Oct 15, 2025 · updated Jun 6, 2026
abstract · pdf · html · 18 pages, 8 figures

add comment on HN

Modern ML is mostly run on other people's hardware (clouds, inference marketplaces, heterogeneous GPU fleets). Today, you can't verify what actually ran: which model, what inputs, or whether your result was silently downgraded (model swap, early exit, quantization, ad-embedding tweaks). The usual fix (recompute and compare) breaks because GPUs are nondeterministic: IEEE-754 is non-associative, kernels reorder reductions, and thread schedules/atomics vary. Bitwise replay at scale is brittle and costly.

We built a system that makes ML results verifiable without requiring determinism. Instead of demanding exact equality, we verify outputs up to principled, per-operator error bounds and resolve disagreements with an optimistic, Merkle-anchored dispute game.

What's inside (precise + concise):

Semantics: "Tolerance-aware correctness" for tensor programs and operator-specific acceptance regions induced by IEEE-754 rounding.

Two error models:

Theoretical IEEE-754 bounds (sound, per-operator, element-wise; conservative but cheap to verify).

Empirical percentile thresholds calibrated across GPUs (tight, model-specific).

Dispute protocol: If a result is challenged, we recursively partition the traced graph (Merkle proofs) until a single operator. At the leaf, we either (i) certify with the theoretical bound or (ii) run a small committee vote against the empirical threshold. Violations are slashed.

Runtime + coordinator: PyTorch-compatible runtime that traces graphs, computes bounds on the fly, records subgraph I/O, and emits/validates commitments; a lightweight coordination layer (we prototyped on Ethereum for authenticated logs/bonds, but the protocol doesn't depend on a blockchain). Overhead ~0.3% latency on Qwen3-8B; no extra memory beyond native subgraph execution.

Scope: Designed for the open-model setting (public weights/graphs enable subgraph extraction and thresholding). Closed-model APIs can still expose commitments to permissioned verifiers. No TEEs required; no deterministic kernels needed.

We’d love feedback on blind spots in the threat model, better partition policies for the dispute game, and where empirical thresholds might be gamed or leak information.