Nondeterminism-Aware Optimistic Verification for Floating-Point Neural Networks

• URL: http://arxiv.org/abs/2510.16028v2
• Date: Tue, 21 Oct 2025 17:28:04 GMT
• Title: Nondeterminism-Aware Optimistic Verification for Floating-Point Neural Networks
• Abstract summary: Nondeterministic Aware Optimistic verification protocol for floating-point execution on heterogeneous accelerators.<n>We implement NAO as a PyTorch-compatible runtime and a contract layer currently deployed on Holesky testnet.
• Score: 11.159101812934503
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Carry-Through Checksum: A Lightweight Fault-Detection for CNN Inference at the Edge [0.21748200848556343]
  We propose carry-through, a fundamentally new scheme for soft-error detection in CNN inference on embedded GPU.<n>The proposed method detects 95.86% and 86.56% of critical faults for FP32 and FP16, respectively, at almost no additional per-image overhead.
  arXiv  Detail & Related papers  (2026-09-15T07:15:30Z)
• Bit-Exact AI Inference Verification Without Performance Tradeoffs [0.0]
  Covert adversaries can exploit unverifiable degrees of freedom in monitored computation.<n>We analyze how modern inference engines produce deterministic but non-invariant outputs.<n>We demonstrate that bitwise-precise re-computation does not require access to identical hardware.
  arXiv  Detail & Related papers  (2026-05-29T19:15:15Z)
• Neuro-Symbolic Financial Reasoning via Deterministic Fact Ledgers and Adversarial Low-Latency Hallucination Detector [2.950245545999729]
  Verifiable Numerical Reasoning Agent (VeNRA) trained to forensically audit Python traces with only one token test budget.<n>VeNRA Sentinel: 3-billion parameter SLM trained to forensically audit Python traces with only one token test budget.
  arXiv  Detail & Related papers  (2026-03-04T22:55:16Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• NEXUS: Bit-Exact ANN-to-SNN Equivalence via Neuromorphic Gate Circuits with Surrogate-Free Training [0.7614628596146601]
  Spiking Neural Networks (SNNs) promise energy-efficient computing through event-driven sparsity.<n>Existing approaches sacrifice accuracy by approximating continuous values with discrete spikes.<n>We propose NEXUS, a framework that achieves bit-exact ANN-to-SNN equivalence.
  arXiv  Detail & Related papers  (2026-01-29T05:23:56Z)
• A Graph-Based Forensic Framework for Inferring Hardware Noise of Cloud Quantum Backend [0.5352699766206807]
  Cloud quantum platforms give users access to many backends with different qubit technologies, coupling layouts, and noise levels.<n>Execution of a circuit depends on internal allocation and routing policies that are not observable to the user.<n>We introduce a Graph Neural Network (GNN)-based forensic framework that predicts per-qubit and per-qubit link error rates of an unseen backend.
  arXiv  Detail & Related papers  (2025-12-16T16:17:04Z)
• Reinforcement Learning with Verifiable yet Noisy Rewards under Imperfect Verifiers [90.50039419576807]
  Reinforcement Learning with Verifiable Rewards (RLVR) trains policies against automated verifiers to avoid costly human labeling.<n>To reduce vulnerability to verifier hacking, many RLVR systems collapse rewards to binary $0,1$ during training.<n>This choice carries a cost: it introduces textitfalse negatives (rejecting correct answers, FNs) and textitfalse positives (accepting incorrect ones, FPs)
  arXiv  Detail & Related papers  (2025-10-01T13:56:44Z)
• Distributed Training under Packet Loss [8.613477072763404]
  Leveraging unreliable connections will reduce latency but may sacrifice model accuracy and convergence once packets are dropped.<n>We introduce a principled, end-to-end solution that preserves accuracy and convergence guarantees under genuine packet loss.<n>This work bridges the gap between communication-efficient protocols and the accuracy and guarantees demanded by modern large-model training.
  arXiv  Detail & Related papers  (2025-07-02T11:07:20Z)
• Exact Certification of (Graph) Neural Networks Against Label Poisoning [50.87615167799367]
  We introduce an exact certification method for label flipping in Graph Neural Networks (GNNs)<n>We apply our method to certify a broad range of GNN architectures in node classification tasks.<n>Our work presents the first exact certificate to a poisoning attack ever derived for neural networks.
  arXiv  Detail & Related papers  (2024-11-30T17:05:12Z)
• On the Convergence of FedProx with Extrapolation and Inexact Prox [55.2480439325792]
  We investigate the behavior of FedExProx without the assumption that each client computes a certain operator exactly. We show that inexactness leads to convergence to a neighborhood of the solution. Our theoretical insights are validated through comprehensive numerical experiments.
  arXiv  Detail & Related papers  (2024-10-02T10:42:27Z)
• Robust Implicit Networks via Non-Euclidean Contractions [63.91638306025768]
  Implicit neural networks show improved accuracy and significant reduction in memory consumption. They can suffer from ill-posedness and convergence instability. This paper provides a new framework to design well-posed and robust implicit neural networks.
  arXiv  Detail & Related papers  (2021-06-06T18:05:02Z)
• AQD: Towards Accurate Fully-Quantized Object Detection [94.06347866374927]
  We propose an Accurate Quantized object Detection solution, termed AQD, to get rid of floating-point computation. Our AQD achieves comparable or even better performance compared with the full-precision counterpart under extremely low-bit schemes.
  arXiv  Detail & Related papers  (2020-07-14T09:07:29Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.