Bit-Exact AI Inference Verification Without Performance Tradeoffs

Technical Summary: Bit-Exact AI Inference Verification Without Performance Tradeoffs

Problem Statement
The paper addresses the challenge of verifying AI computations performed by "covert adversaries"—entities that comply with monitoring only when the likelihood of detection is high. Current verification methods face a significant hurdle: the apparent non-determinism of GPU floating-point arithmetic. Due to non-associative summation in parallel reductions and hardware-specific approximations, auditors are often forced to accept approximate output matches. This ambiguity creates "unverifiable degrees of freedom" that adversaries can exploit for steganography, unreported software modifications, or covert computation (e.g., hidden batch elements). While zero-knowledge proofs (ZKPs) offer a path forward, they typically require strict determinism as a precondition, which has historically necessitated performance-compromising flags or custom kernel libraries.

Methodology
The authors investigate the root causes of output variance in modern inference engines (vLLM, HuggingFace Transformers) running on NVIDIA GPUs (L40, L40S, A100, H100) without enabling performance-degrading determinism flags. Their approach involves:

1. Root Cause Analysis: Distinguishing between true non-determinism (caused by atomic functions like atomicAdd where warp scheduling varies) and non-invariance (deterministic but varying reduction trees due to software stack, batch size, or hardware topology).
2. Empirical Testing: Running inference across various hardware SKUs, software versions, batch sizes, and quantization formats (BF16, FP8, INT8, INT4) to measure L2 distances between signal vectors (log-probabilities, hidden states).
3. Software-Only Emulation: Developing a C/Python emulator that runs entirely on CPU to predict the exact bit-level output of GPU-accelerated LLM inference. This emulator models:
   • Tensor Core Arithmetic: Replicating the specific Fixed-Point alignment windows, truncation, and accumulation logic of Tensor Cores (e.g., A100's 26-bit window) and MMA instructions.
   • Special Function Units (SFUs): Caching exact hardware outputs for transcendental functions (exponential, reciprocal square root) which deviate from IEEE 754 but are deterministic.
   • Kernel-Specific Reductions: Mirroring the exact reduction trees, tile boundaries, and accumulation orders dictated by specific kernel configurations (e.g., CUTLASS, FlashAttention-2, cuBLAS dispatch logic).
   • Data Boundaries: Enforcing precise BF16 quantization boundaries between pipeline stages to match hardware behavior.

Key Results

• Determinism without Flags: The study demonstrates that modern inference engines produce bitwise-identical outputs when the software stack, hardware SKU, and input shapes (including batch size) are fixed. The apparent non-determinism is largely a function of changing reduction orders based on these parameters, not random noise.
• Source of Variance: The only genuine source of non-determinism identified was the use of atomicAdd in specific INT-dequantization kernels (e.g., the default exllama kernel for GPTQ in vLLM). When these are avoided or replaced (e.g., using the marlin kernel), outputs are deterministic.
• Batch Size Invariance: The authors observed "equivalence classes" where changing batch sizes did not alter the output of the first batch element, particularly at longer sequence lengths (>4,000 tokens) where kernel selection stabilizes.
• Emulation Accuracy: The software-only emulator achieved 0 bit-differences (BF16 and FP32 accumulator) against ground truth GPU runs for full FFN blocks and complex FlashAttention-2 blocks across multiple GPU architectures. This confirms that accumulated rounding errors can be precisely predicted and audited without access to the original hardware.

Key Contributions

1. Reframing Rounding Errors: The paper argues that rounding errors should not be viewed as a constraint on verifiability but as an "auditable signature" of the specific software and hardware setup used.
2. Bit-Exact Verification Protocol: It establishes that bitwise-precise re-computation is possible without identical hardware, provided the verifier knows the key static factors (hardware SKU, software versions, model weights, parallelism topology) and the dynamic batch size.
3. Software-Only Emulation: The demonstration of a CPU-based emulator capable of modeling GPU-specific arithmetic (including Tensor Core reduction trees and SFU approximations) to predict LLM inference outputs bit-for-bit.
4. Performance Preservation: The verification method does not require the performance tradeoffs associated with forcing determinism flags or using custom invariant kernels; it relies on the existing deterministic nature of standard inference engines when conditions are fixed.

Significance and Claims
The paper concludes that "plausible deniability" in AI inference outputs is removable. By reporting the concurrent batch size and configuration details alongside the output, a prover can collapse verification into a simple pass/fail check against a bit-exact re-computation. The authors claim that the numeric sensitivity of outputs serves as a high-fidelity fingerprint of the prover's hardware and software stack. This enables credible governance of covert adversaries by ensuring that any deviation from the claimed computation (e.g., hidden steganography or unauthorized software modifications) would result in a detectable bitwise mismatch, provided the verification setup accounts for the specific configuration factors identified. The work suggests that the "non-determinism" often cited as a barrier to AI verification is actually a deterministic, reproducible artifact of the computing environment.