Pith. sign in

REVIEW 5 major objections 6 minor 64 references

Floating-point neural networks can be verified on untrusted heterogeneous hardware by accepting outputs within per-operator tolerance regions and resolving disputes with a Merkle-anchored game that terminates at a single operator.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

T0 review · deepseek-v4-flash

2026-08-04 09:37 UTC pith:WDLKFIT2

load-bearing objection Promising tolerance-aware optimistic verification for FP neural networks, but 'sound' is claimed too strongly and the empirical thresholds are not yet proven to generalize beyond the 4 calibration GPUs. the 5 major comments →

arxiv 2510.16028 v4 pith:WDLKFIT2 submitted 2025-10-15 cs.CR cs.AIcs.LGcs.SYeess.SY

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

classification cs.CR cs.AIcs.LGcs.SYeess.SY
keywords verifiable machine learningoptimistic verificationfloating-point nondeterminismIEEE-754 error boundsdispute gameoperator-level acceptance regionMLaaS accountabilitytolerance-aware correctness
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to make ML-as-a-service accountable without requiring bitwise reproducibility, deterministic kernels, or trusted hardware. It argues that the right correctness target for floating-point neural networks is an operator-level acceptance region: a sound IEEE-754 worst-case bound together with a tight empirical error-envelope calibrated across devices. Verification then becomes a localization problem, with a dispute game that recursively narrows any disagreement to one operator, where a cheap bound check or a small committee vote against empirical thresholds settles it. If the construction holds, providers can be held to the agreed model and input at roughly 0.3% optimistic overhead, with disputes costing roughly 0.39–1.24x a forward pass. The reported experiments show empirical thresholds 100–1000x tighter than theoretical bounds and 0% adversarial attack success under those thresholds.

Core claim

The central discovery is that the apparent obstacle — floating-point nondeterminism across GPUs — can be treated as a calibrated distribution rather than eliminated. Each operator's benign cross-device error is small, flat across depth, and concentrated, so a percentile envelope computed offline separates honest executions from tampering. The protocol commits to model weights, graph topology, and these envelopes; a proposer's output finalizes unless a challenger finds a discrepancy beyond the envelope, which triggers an N-way partition of the traced graph with Merkle proofs until one operator remains. At the leaf, the proposer's result is either checked against the sound IEEE-754 bound or vo

What carries the argument

The carrying object is the per-operator acceptance region, defined for each primitive tensor function (matrix multiply, convolution, activation, and so on) by two envelopes: a sound element-wise IEEE-754 worst-case rounding bound computed from a first-order sensitivity template, and a calibrated empirical percentile profile (max-envelope over device pairs and sampled inputs, inflated by a factor of three). The dispute game is the mechanism that uses it: the proposer partitions the committed graph into N disjoint subgraphs, the challenger recomputes each slice and selects the first child whose error percentiles exceed the committed thresholds, and recursive partitioning reaches a single opera

Load-bearing premise

The protocol stands or falls on the calibrated empirical thresholds: they must be loose enough that every honest device's benign floating-point drift stays inside them, yet tight enough that no bounded adversarial perturbation can hide inside them, measured on only 50 inputs per model across four GPU types and then inflated by a factor of three.

What would settle it

Run an honest GPU or kernel that was not part of the calibration set through the same models and check whether any operator's cross-device error exceeds the committed 3x-inflated thresholds; one benign violation means honest nodes can be slashed. Symmetrically, run the paper's own projected-gradient attack with thresholds inflated by 3x on a held-out model family: if the attack success rate exceeds zero, the empirical envelopes are not as tight as claimed.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

If this is right

  • Unchallenged inferences finalize after a short challenge window at native speed, making the optimistic path cheap enough for large models (about 0.3% overhead on an 8B-parameter LLM).
  • Disputes cost only a fraction of a re-execution: challenger FLOPs to reach and adjudicate the leaf range from 0.39x to 1.24x a forward pass across the evaluated models.
  • Accepting outputs up to tolerance means no trusted hardware and no deterministic operator libraries; any IEEE-754-compliant vendor kernel can participate.
  • Because empirical thresholds are 100–1000x tighter than worst-case bounds, bound-aware adversarial perturbations cannot flip decisions: the paper reports 0% attack success across CNNs, transformers, and diffusion models even with thresholds inflated 3x.
  • The remaining attack surface is the two error models themselves: theory-only checks admit up to 2.4% attack success on an 8B LLM, which is why the protocol routes leaf adjudication to empirical-threshold committee voting when the bound check is inconclusive.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same two-dimensional localization — bisect over time to the earliest offending step, then over operators within that step — could extend the protocol to autoregressive decoding and training, giving prefix finality for early tokens; the paper sketches this as ongoing work, but it is a testable consequence of the mechanism, not yet a demonstrated result.
  • If thresholds are committed on-chain, they become public knowledge; a stronger adversary than the one tested could tune perturbations to fit the exact envelope shape. A natural stress test is to evaluate the PGD attacks against thresholds calibrated on a disjoint set of devices and inputs, and to probe interpolated percentiles between the committed grid points.
  • The 0% false-positive result is an empirical point estimate from finite samples; deployment would benefit from an online recalibration protocol that updates envelopes when new device families join, since the paper acknowledges calibration churn as a limitation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

5 major / 6 minor

Summary. The paper presents NAO (also titled TAO in the arXiv metadata), an optimistic verification protocol for floating-point neural network inference on heterogeneous hardware. Rather than requiring bitwise reproducibility, NAO verifies outputs against per-operator acceptance regions built from two error models: theoretical IEEE-754 rounding bounds (§4.1) and empirically calibrated percentile thresholds (§4.2). A Merkle-anchored dispute game recursively partitions the computation graph until a single operator is isolated, where adjudication is by a theoretical-bound check or a small committee vote. The system is implemented as a PyTorch runtime and Ethereum Holesky contracts; evaluation on CNNs, Transformers, and diffusion models across four GPUs reports ~0.3% optimistic overhead, empirical thresholds 10^2–10^3 tighter than theory, and 0% attack success under bound-aware adversarial perturbations.

Significance. If the central claims were rigorously established, this would be a meaningful contribution to verifiable ML: it addresses the practical gap between worst-case floating-point analysis and real cross-hardware nondeterminism, and it avoids the costs of zkML, deterministic replay, and TEEs. The operator-level dispute localization and the combination of sound theoretical bounds with tight empirical thresholds are both timely and well-motivated. The paper ships a working runtime and contract layer, and the attack study goes beyond the usual anecdotal evaluation. However, the current manuscript overstates the rigor of its theoretical bounds and does not establish the cross-device generality of its empirical thresholds, which are load-bearing assumptions for the protocol's economic and security guarantees. With careful revision, the work could become an influential system/security paper.

major comments (5)
  1. [§4.1, softmax derivation and 'We ignore the additional numerical errors introduced while computing these error bounds th] The theoretical bound is a first-order sensitivity envelope, not a sound worst-case bound. The softmax derivation uses terms like ε_z ≤ u(|x|+|m|) and then propagates only first-order derivatives, omitting second-order products of errors. More importantly, the paper explicitly ignores errors introduced while computing the bounds themselves, despite using FP64. The abstract and §2.3 call these bounds 'sound by construction', and §6.4's theoretical leaf check depends on this soundness. As written, the theoretical path does not meet the 'soundness' objective defined in §5.1. Please either compute rigorously certified bounds (e.g., directed rounding/interval arithmetic, or rigorous error-free transformations in the bound computation) or downgrade the claim from 'sound' to 'approximate'. This is load-bearing because the leaf adjudication and the economic slashing rules assume a certified chec
  2. [§4.2, Eq. (5)–(7) and §5.5/Table 2] The empirical thresholds are calibrated on a max-envelope over 4 GPUs and 50 inputs, then inflated by α=3. The 0% false-positive result in §5.5 is measured by running the pipeline on 1k inputs on the same 4 GPUs used for calibration; it does not validate the behavior on unseen hardware or kernels. If an honest node uses a GPU or kernel outside the calibration set whose benign deviation exceeds the committed α=3 threshold, the challenger will raise a dispute and the honest proposer will be slashed. The paper's §9 dismisses this as 'a minor limitation', but it undermines the device-agnostic verifiability claim that is central to the paper. The stability metrics in Table 1 (SupNorm, Jackknife, TailAdj, RollSD) measure drift of running medians within the calibration sample, not coverage of unseen devices. Please either provide a rigorous generalization argument (e.g., distribution-free worst
  3. [§6.4, 'Routing policy'] The routing policy appears to be stated backwards. The text says: 'If any element exceeds τ_theo_v*, it invokes path (i); otherwise, it invokes path (ii) to apply the tighter empirical thresholds.' Path (i) then requires the proposer to prove |y^P_v* − y^ref_v*| ≤ τ_theo_v*, which is impossible if the threshold was already exceeded. The natural semantics, and the one shown in Fig. 3 ('Exceeds theoretical bound -> Slash Proposer'), is that exceeding the theoretical cap is itself proof of fraud. Please clarify or correct this paragraph; as written it is internally inconsistent and makes the leaf adjudication logic ambiguous.
  4. [§7.3 and §3.1, '0.3% overhead'] The Abstract, §3, and §7.3 claim 'negligible overhead (0.3% on Qwen3-8B)' for the NAO runtime. However, the experiment in §7.3 measures only the overhead of the 'software deterministic settings' (CUBLAS_WORKSPACE_CONFIG, fixed seeds, disabling TF32/benchmark, etc.), not the overhead of the full NAO instrumentation: the FX-based co-execution, on-the-fly bound computation, trace recording, and commitment generation. These two cost components are additive, and the abstract's attribution of 0.3% to the whole system is unsupported. Please report the end-to-end runtime overhead of the complete pipeline, ideally separating calibration, optimistic execution, and dispute phases.
  5. [§6.5, Economic soundness] The paper's contribution list includes 'economic finality' and 'economic soundness', but §6.5 contains only a paragraph deferring to prior work ([41], [52], [55]) without analyzing the new failure modes introduced by the tolerance machinery. These include: threshold-gaming (a malicious proposer choosing perturbations that stay just below the committed thresholds across many operators), the incentives of the committee to execute the leaf faithfully, and the effect of the empirical-threshold slashing rule on honest parties. The cited mechanisms address generic optimistic-rollup/watchtower settings, not the specific per-operator tolerance checks here. Please provide a self-contained incentive analysis, or, if the paper is positioned primarily as a system design, move the economic-soundness claim from a contribution to a stated assumption.
minor comments (6)
  1. [Title/abstract vs. full text] The arXiv metadata and initial abstract use 'TAO', while the full text consistently uses 'NAO'. Please harmonize the terminology throughout.
  2. [References [20] and [27]] The probabilistic rounding-error model is cited as '[20, 27]' in §4.1 and '[27]' in Appendix A.2, but reference [27] is Madry et al. (adversarial attacks), not a probabilistic rounding error analysis. The correct citation appears to be [20] (Higham & Mary) and possibly another source. Please fix.
  3. [§4.1, '35 operators'] The text says 'Analogous templates cover other 35 common operators', but Appendix A.3 lists a smaller set (approximately 20–30 distinct operator types). Please provide a complete list or reconcile the count.
  4. [Eq. (15) and threshold division] The max-ratio p_max_i in Eq. (15) divides by τ_abs/rel. If any calibrated threshold is zero (e.g., a constant tensor), the ratio is undefined. Specify the handling of zero thresholds or guarantee positivity.
  5. [Table 2, theoretical-bound rows] The false-positive column is '-' for the theoretical-bound attack rows. Since the theoretical bound is claimed to be sound, it would be informative to report the honest-run false-positive rate for the theoretical check as well, especially given the first-order (non-rigorous) nature of the bound.
  6. [§5.4, projection onto empirical thresholds] The projection in Eq. (12) sorts the magnitude of the tentative perturbation vector and clips order statistics to a quantile cap. The actual discrepancy checked by the protocol is |proposer_output − challenger_output|, which includes the benign reordering error plus the injected perturbation. The attack's feasible set (Eq. 8) is defined on the perturbation alone, so the projection is an approximation of the true feasible set. Please clarify this discrepancy.

Circularity Check

1 steps flagged

Economic-soundness conclusion is delegated to self-cited prior work; the technical verification chain itself is self-contained.

specific steps
  1. self citation load bearing [Section 6.5, 'Economic soundness and incentives']
    "Such mechanisms have been extensively developed in other accountability frameworks for off-chain execution, including in incentive-secure proof-of-learning protocols [55], sampling-and-penalty schemes [52], and watchtower-style networks [41]. We directly use these mature mechanisms to support our protocol: honest execution remains individually rational, voluntary challenges are properly incentivized, and committee participation under randomized audits is sustainable."

    The paper's central claim includes 'economic finality' and 'economically verifiable' ML, but the only support for the incentive-compatibility premises is this citation block. Refs [55] and [41] share authors with the present paper (Xuechao Wang and Hongxu Su; Pramod Viswanath), and their results are not re-derived, machine-checked, or shown to hold under NAO's tensor-operator dispute game with empirical thresholds. The economic soundness of this protocol is thus imported from the authors' own prior work rather than established in this context.

full rationale

The technical core of NAO is not circular. Section 4.1 derives operator-local IEEE-754 bounds from the standard FP model (Eqs. 16-26); the thresholds in Section 4.2 are calibrated measurements, and the 0% ASR/FP numbers in Table 2 are empirical evaluations against those calibrated regions, not identities forced by construction. The dispute game (Section 6) is built from Merkle commitments and partition rules, independently of the claimed guarantees. The main load-bearing circularity is Section 6.5: the paper's economic-soundness conclusion is transferred from self-cited prior work [41,55] rather than proved, and the transfer is an assumption about mechanism applicability, not a derivation. The paper's own Section 9 limitation ('calibration churn: onboarding new devices or kernels requires efficiently updating empirical thresholds and validating them') is a robustness/generalization gap rather than a definitional circularity. Score 3 reflects one load-bearing self-citation while the central tolerance-aware verification construction retains independent content.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 0 invented entities

The protocol introduces roles (proposer, challenger, committee) and Merkle commitments but no new physical or mathematical entity. The load-bearing free parameters are the empirically calibrated per-operator thresholds and the inflation factor α=3; the theoretical bound claims rest on first-order floating-point error models whose strict soundness is asserted rather than fully proven.

free parameters (3)
  • Per-operator empirical error thresholds τ_abs, τ_rel = Max-envelope percentile profiles over calibration inputs/devices, inflated by α=3 (§4.2, Eqs. 5–7)
    These thresholds define the acceptance regions; they are fitted to observed cross-device deviations on 50 samples × 4 GPUs and are load-bearing for both false-positive rate and attack success rate.
  • Probabilistic bound constant λ = 4 (≈99.93% confidence)
    Hand-selected constant in §4.1 used in the γ̃_k(λ) probabilistic rounding bound; controls tightness of the theoretical leaf check.
  • Calibration inflation factor α = 3
    Multiplicative safety margin applied to every empirical percentile value (§4.2, Eq. 7); chosen by hand and directly affects how tight or permissive the acceptance regions are.
axioms (5)
  • domain assumption IEEE-754 round-to-nearest-even, unit roundoff u=2^-24, no overflow/underflow/subnormal, fast-math disabled
    Stated in §A.1 and §3.1; required for the theoretical error bounds and for the measured 0.3% deterministic-execution overhead.
  • ad hoc to paper First-order sensitivity envelope with ignored second-order and bound-computation errors is a sound worst-case bound
    §4.1: 'We ignore the additional numerical errors introduced while computing these error bounds themselves.' If this fails, the leaf theoretical check is not actually sound as claimed.
  • domain assumption Empirical percentile thresholds calibrated on 50 samples × 4 GPUs generalize to all proposer/challenger hardware, inputs, and kernels
    §4.2 and §5.5: threshold construction and the 0% FP/ASR results depend on this generalization; §9 acknowledges 'calibration churn' for new devices.
  • domain assumption Committee has an honest majority, and incentive mechanisms from [41,52,55] apply unchanged
    §3.1 assumes honest majority; §6.5 defers economic soundness to prior work, including papers with overlapping authors, rather than providing a new proof.
  • domain assumption Probabilistic rounding errors are independent, mean-zero, and bounded, and vendor-stated max-ULP errors for CUDA intrinsics are correct
    Used in §4.1 and §A.2 for the probabilistic γ̃_k bounds and for library intrinsics; standard but not verified inside the paper.

pith-pipeline@v1.3.0-alltime-deepseek · 25488 in / 12824 out tokens · 106633 ms · 2026-08-04T09:37:00.036158+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of TAO: Tolerance-Aware Optimistic Verification for Floating-Point Neural Networks." pith.science (2026). https://pith.science/paper/WDLKFIT2

@misc{pith2026251016028,
  author       = {Pith},
  title        = {Pith review of: TAO: Tolerance-Aware Optimistic Verification for Floating-Point Neural Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WDLKFIT2}},
  note         = {Machine review of arXiv:2510.16028}
}
Share X Bluesky LinkedIn Reddit HN
read the original 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 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.

Figures

Figures reproduced from arXiv: 2510.16028 by Hongxu Su, Huan Zhang, Jianzhu Yao, Pramod Viswanath, Taobo Liao, Xuechao Wang, Zerui Cheng.

Figure 1
Figure 1. Figure 1: Tolerance-aware optimistic verification on two example tasks. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. 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 local￾ized spikes, indicating limited room for attack. element-wise deviation between two valid executions of the same operator given the same inputs but on different (hard￾ware, library) configurations. Using traced models, we ran the identica… view at source ↗
Figure 3
Figure 3. 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 (𝑥, 𝑦). Phase 2 (Dispute Localization): an 𝑁-way, Merkle-anchored dispute game recursively narrows disagreement to a single operator following a canonical partition policy. Phase 3 (Single-Operator A… view at source ↗
Figure 4
Figure 4. Figure 4: Comparison between deterministic and probabilis￾tic theoretical error bounds for different operator types in Qwen-8B and BERT-large. fresh rounding. Analogous templates cover other 35 com￾mon operators (LayerNorm, MatMul, Conv2d, etc.); We ignore the additional numerical errors introduced while computing these error bounds themselves. Putting it together. Our library of operator templates yields 𝜏 theo 𝑣 c… view at source ↗
Figure 5
Figure 5. Figure 5: Normalized margin change on failed attacks (𝛼=1). Empirical thresholds yield near-zero progress across models; theoretical bounds(p) show heavier tails for the LLM. Num￾bers above boxes show sample sizes. (4) Margin-change distributions corroborate tightness [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Comparison between empirical and theoretical er￾ror bounds for different operator types in ResNet 152, Qwen￾8B and BERT-large models. Evaluation metrics. (i) Avg. dispute rounds: average num￾ber of rounds required to reach the leaf; (ii) Avg. dispute time: average off-chain dispute time (including both pro￾poser and challenger with disk I/O); (iii) Avg. Merkle checks: average number of weight/topology proo… view at source ↗
Figure 7
Figure 7. Figure 7: Microbenchmarks on BERT-large dispute game: vary split size 𝑁 and dispute round index. Left: avg dispute rounds decrease roughly as 𝑂(log𝑁 |𝑉 |). Mid-left: avg dispute time drops sharply from small 𝑁 and plateaus for 𝑁 ≥8. Mid-right: avg Merkle proof checks for weights/graph fall as 𝑁 grows. Right: per-round substep time (proposer partition vs. challenger re-execute plus selection) measured across eight pe… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

64 extracted references · 2 canonical work pages

  1. [1]

    Jason Ansel, Edward Yang, Horace He, Natalia Gimelshein, Animesh Jain, Michael Voznesensky, Bin Bao, Peter Bell, David Berard, Evgeni Burovski, et al. 2024. Pytorch 2: Faster machine learning through dynamic python bytecode transformation and graph compilation. In Proceedings of the 29th ACM International Conference on Architectural Support for Programmin...

  2. [2]

    Arasu Arun, Adam St Arnaud, Alexey Titov, Brian Wilcox, Viktor Kolobaric, Marc Brinkmann, Oguzhan Ersoy, Ben Fielding, and Joseph Bonneau. 2025. Verde: Verification via refereed delegation for machine learning programs.arXiv preprint arXiv:2502.19405(2025)

  3. [3]

    Sören Auer, Christian Bizer, Georgi Kobilarov, Jens Lehmann, Richard Cyganiak, and Zachary Ives. 2007. Dbpedia: A nucleus for a web of open data. Ininternational semantic web conference. Springer, 722–735

  4. [4]

    Juyang Bai, Md Hafizul Islam Chowdhuryy, Jingtao Li, Fan Yao, Chaitali Chakrabarti, and Deliang Fan. 2025. Phantom: Privacy- Preserving Deep Neural Network Model Obfuscation in Heteroge- neous TEE and GPU System. 34th USENIX Security Symposium

  5. [5]

    Rothblum

    Ran Canetti, Ben Riva, and Guy N. Rothblum. 2011. Practical Delega- tion of Computation Using Multiple Servers. InProceedings of the 18th ACM Conference on Computer and Communications Security (CCS). 445–454

  6. [6]

    Rothblum

    Ran Canetti, Ben Riva, and Guy N. Rothblum. 2013. Refereed Delega- tion of Computation.Information and Computation226 (2013), 16–36. doi:10.1016/j.ic.2013.03.003

  7. [7]

    Bing-Jyue Chen, Suppakit Waiwitlikhit, Ion Stoica, and Daniel Kang

  8. [8]

    Dami Choi, Yonadav Shavit, and David K Duvenaud. 2023. Tools for verifying neural models’ training data.Advances in Neural Information Processing Systems36 (2023), 1154–1188

  9. [9]

    Yuan Hsi Chou, Christopher Ng, Shaylin Cattell, Jeremy Intan, Matthew D Sinclair, Joseph Devietti, Timothy G Rogers, and Tor M Aamodt. 2020. Deterministic atomic buffering. In2020 53rd Annual IEEE/ACM International Symposium on Microarchitecture (MICRO). IEEE, 981–995

  10. [10]

    KD Conway, Cathie So, Xiaohang Yu, and Kartin Wong. 2024. opml: Optimistic machine learning on blockchain.arXiv preprint arXiv:2401.17555(2024)

  11. [11]

    Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei

  12. [12]

    Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova

  13. [13]

    Amir Esmaeili and Abderrahmen Mtibaa. 2024. SERENE: A collusion resilient replication-based verification framework. In2024 IEEE 13th International Conference on Cloud Networking (CloudNet). IEEE, 1–9

  14. [14]

    Zahra Ghodsi, Tianyu Gu, and Siddharth Garg. 2017. Safetynets: Verifiable execution of deep neural networks on an untrusted cloud. Advances in Neural Information Processing Systems30 (2017)

  15. [15]

    David Goldberg. 1991. What every computer scientist should know about floating-point arithmetic.ACM computing surveys (CSUR)23, 1 (1991), 5–48

  16. [16]

    Rothblum

    Shafi Goldwasser, Yael Tauman Kalai, and Guy N. Rothblum. 2008. Delegating Computation: Interactive Proofs for Muggles. InSTOC. 113–122

  17. [17]

    Design Guide. 2013. Cuda c programming guide.NVIDIA, July29, 31 (2013), 6

  18. [18]

    Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. 2016. Deep residual learning for image recognition. InProceedings of the IEEE conference on computer vision and pattern recognition. 770–778

  19. [19]

    2002.Accuracy and stability of numerical algo- rithms

    Nicholas J Higham. 2002.Accuracy and stability of numerical algo- rithms. SIAM

  20. [20]

    Nicholas J Higham and Theo Mary. 2019. A new approach to proba- bilistic rounding error analysis.SIAM journal on scientific computing 41, 5 (2019), A2815–A2835

  21. [21]

    Hengrui Jia, Mohammad Yaghini, Christopher A Choquette-Choo, Natalie Dullerud, Anvith Thudi, Varun Chandrasekaran, and Nicolas Papernot. 2021. Proof-of-learning: Definitions and practice. In2021 IEEE Symposium on Security and Privacy (SP). IEEE, 1039–1056

  22. [22]

    Kai Jia and Martin Rinard. 2021. Exploiting verified neural networks via floating point numerical error. InInternational Static Analysis Symposium. Springer, 191–205

  23. [23]

    William Kahan. 1996. IEEE standard 754 for binary floating-point arithmetic.Lecture Notes on the Status of IEEE754, 94720-1776 (1996), 11

  24. [24]

    Rothblum

    Yael Tauman Kalai, Ran Raz, and Ron D. Rothblum. 2022. How to Delegate Computations: The Power of No-Signaling Proofs.J. ACM 69, 1, Article 1 (2022). doi:10.1145/3456867

  25. [25]

    Harry Kalodner, Steven Goldfeder, Xiaoqi Chen, S Matthew Wein- berg, and Edward W Felten. 2018. Arbitrum: Scalable, private smart contracts. In27th USENIX Security Symposium (USENIX Security 18). 1353–1370

  26. [26]

    Assaf Lahiany and Yehudit Aperstein. 2022. PTEENet: Post-trained early-exit neural networks augmentation for inference cost optimiza- tion.IEEE Access10 (2022), 69680–69687

  27. [27]

    Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. 2018. Towards Deep Learning Models Re- sistant to Adversarial Attacks. InInternational Conference on Learning Representations

  28. [28]

    Stephen Merity, Caiming Xiong, James Bradbury, and Richard Socher

  29. [29]

    Ralph C Merkle. 1987. A digital signature based on a conventional encryption function. InConference on the theory and application of cryptographic techniques. Springer, 369–378

  30. [30]

    Michael Mirkin, Hongyin Chen, Ohad Eitan, Gal Granot, and Ittay Eyal

  31. [31]

    Myungsuk Moon, Minhee Kim, Joonkyo Jung, and Dokyung Song

  32. [32]

    Yue Niu, Ramy E Ali, and Salman Avestimehr. 2022. 3LegRace: Privacy- Preserving DNN Training over TEEs and GPUs.Proceedings on Privacy Enhancing Technologies(2022)

  33. [33]

    Optimism. 2025. Fault Proof.https://specs.optimism.io/fault-proof/ index.html. OP Stack Specification. Accessed: 2025-09-23

  34. [34]

    Optimism. 2025. Multithreaded Cannon Fault Proof Virtual Ma- chine.https://specs.optimism.io/fault-proof/cannon-fault-proof-vm. html. OP Stack Specification. Accessed: 2025-09-23

  35. [35]

    PyTorch Contributors. 2024. Reproducibility.https://docs.pytorch. org/docs/stable/notes/randomness.html. PyTorch 2.8 documentation. 14 Nondeterminism-Aware Optimistic Verification for Floating-Point Neural Networks Last updated: 2024-11-26. Accessed: 2025-09-23

  36. [36]

    PyTorch Contributors. 2025. torch.fx.https://docs.pytorch.org/docs/ main/fx.html. PyTorch main documentation. Last updated: 2025-07-15. Accessed: 2025-09-23

  37. [37]

    InProceedings 2025 Network and Distributed System Security Symposium

    ASGARD: Protecting On-Device Deep Neural Networks with Virtualization-Based Trusted Execution Environments. InProceedings 2025 Network and Distributed System Security Symposium

  38. [38]

    Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J. Liu. 2019. Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer.arXiv e-prints(2019). arXiv:1910.10683

  39. [39]

    Robin Rombach, Andreas Blattmann, Dominik Lorenz, Patrick Esser, and Björn Ommer. 2022. High-Resolution Image Synthesis With Latent Diffusion Models. InProceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). 10684–10695

  40. [40]

    Sanjif Shanmugavelu, Mathieu Taillefumier, Christopher Culver, Oscar Hernandez, Mark Coletti, and Ada Sedova. 2024. Impacts of floating- point non-associativity on reproducibility for HPC and deep learning applications. InSC24-W: Workshops of the International Conference for High Performance Computing, Networking, Storage and Analysis. IEEE, 170–179

  41. [41]

    Peiyao Sheng, Ranvir Rana, Senthil Bala, Himanshu Tyagi, and Pramod Viswanath. 2024. Proof of diligence: Cryptoeconomic security for rollups.arXiv preprint arXiv:2402.07241(2024)

  42. [42]

    Megha Srivastava, Simran Arora, and Dan Boneh. 2024. Optimistic verifiable training by controlling hardware nondeterminism.Advances in Neural Information Processing Systems37 (2024), 95639–95661

  43. [43]

    Wenjie Qu, Yijun Sun, Xuanming Liu, Tao Lu, Yanpei Guo, Kai Chen, and Jiaheng Zhang. 2025. zkGPT: An Efficient Non-interactive Zero- knowledge Proof Framework for LLM Inference. In34st USENIX Secu- rity Symposium (USENIX Security 25)

  44. [44]

    Attila Szász, Balázs Bánhelyi, and Márk Jelasity. 2025. No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks.arXiv preprint arXiv:2506.01054(2025)

  45. [45]

    Qwen Team. 2025. Qwen3 Technical Report. arXiv:2505.09388 [cs.CL] https://arxiv.org/abs/2505.09388

  46. [46]

    Jason Teutsch and Christian Reitwießner. 2024. A scalable verification solution for blockchains. InAspects of Computation and Automata Theory with Applications. World Scientific, 377–424

  47. [47]

    Florian Tramer and Dan Boneh. [n. d.]. Slalom: Fast, Verifiable and Private Execution of Neural Networks in Trusted Hardware. InInter- national Conference on Learning Representations

  48. [48]

    Haodi Wang and Thang Hoang. 2023. ezDPS: An Efficient and Zero- Knowledge Machine Learning Inference Pipeline.Proceedings on Privacy Enhancing Technologies2 (2023), 430–448

  49. [49]

    Haochen Sun, Jason Li, and Hongyang Zhang. 2024. zkllm: Zero knowledge proofs for large language models. InProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security. 4405–4419

  50. [50]

    Peichen Xie, Yanjie Gao, Yang Wang, and Jilong Xue. 2025. Revealing {Floating-Point}Accumulation Orders in{Software/Hardware}Im- plementations. In2025 USENIX Annual Technical Conference (USENIX ATC 25). 1425–1440

  51. [51]

    Tianyi Zhang, Cuiyun Gao, Lei Ma, Michael Lyu, and Miryung Kim

  52. [52]

    Yue Zhang, Shouqiao Wang, Sijun Tan, Xiaoyuan Liu, Ciamac C Moallemi, and Raluca Ada Popa. 2024. Proof of Sampling: A Nash Equilibrium-Based Verification Protocol for Decentralized Systems. arXiv preprint arXiv:2405.00295(2024)

  53. [53]

    Shanyu Zhao, Virginia Lo, and C Gauthier Dickey. 2005. Result verifi- cation and trust-based scheduling in peer-to-peer grids. InFifth IEEE International Conference on Peer-to-Peer Computing (P2P’05). IEEE, 31–38

  54. [54]

    Yilong Zhao, Chien-Yu Lin, Kan Zhu, Zihao Ye, Lequn Chen, Size Zheng, Luis Ceze, Arvind Krishnamurthy, Tianqi Chen, and Baris Kasikci. 2024. Atom: Low-bit quantization for efficient and accurate llm serving.Proceedings of Machine Learning and Systems6 (2024), 196–209

  55. [55]

    Lingxiao Wei, Bo Luo, Yu Li, Yannan Liu, and Qiang Xu. 2018. I know what you see: Power side-channel attack on convolutional neural network accelerators. InProceedings of the 34th Annual Computer Security Applications Conference. 393–406

  56. [56]

    Zihan Zheng, Peichen Xie, Xian Zhang, Shuo Chen, Yang Chen, Xiaobing Guo, Guangzhong Sun, Guangyu Sun, and Lidong Zhou

  57. [58]

    In2019 IEEE 30th international symposium on software reliability engineering (ISSRE)

    An empirical study of common challenges in developing deep learning applications. In2019 IEEE 30th international symposium on software reliability engineering (ISSRE). IEEE, 104–115

  58. [62]

    Zishuo Zhao, Zhixuan Fang, Xuechao Wang, Xi Chen, Hongxu Su, Haibo Xiao, and Yuan Zhou. 2025. Proof-of-Learning with Incentive Security. arXiv:2404.09005 [cs.CR]https://arxiv.org/abs/2404.09005

  59. [2009]

    In2009 IEEE conference on computer vision and pattern recognition

    Imagenet: A large-scale hierarchical image database. In2009 IEEE conference on computer vision and pattern recognition. Ieee, 248–255

  60. [2017]

    InInternational Conference on Learning Representations

    Pointer Sentinel Mixture Models. InInternational Conference on Learning Representations

  61. [2019]

    InProceedings of the 2019 conference of the North American chapter of the association for computational linguistics: human language technologies, volume 1 (long and short papers)

    Bert: Pre-training of deep bidirectional transformers for lan- guage understanding. InProceedings of the 2019 conference of the North American chapter of the association for computational linguistics: human language technologies, volume 1 (long and short papers). 4171–4186

  62. [2021]

    Agatha: Smart contract for DNN computation.arXiv preprint arXiv:2105.04919(2021). 15 Yao, Su, Liao, Cheng, Zhang, Wang, and Viswanath A Floating Point A.1 Floating Point Basics We assume IEEE 754 arithmetic with rounding to nearest, ties to even, and exclude overflow/underflow/NaNs unless stated otherwise. Let𝑢 denote theunit roundoff(machine epsilon divi...

  63. [2024]

    InProceedings of the Nineteenth European Conference on Com- puter Systems

    Zkml: An optimizing system for ml inference in zero-knowledge proofs. InProceedings of the Nineteenth European Conference on Com- puter Systems. 560–574

  64. [2025]

    Cryptology ePrint Archive(2025)

    Arbigraph: Verifiable Turing-Complete Execution Delegation. Cryptology ePrint Archive(2025)