# Verification research, 12 September 2026

This is an isolated research note. The running learning milestone remains on its committed implementation and recipe. No code from this probe is in the protocol package or active chain.

## Reading

- [zkDL](https://arxiv.org/abs/2307.16273) reports proof generation for training an 8-layer, 10M-parameter neural network. This is relevant evidence for verifiable training, but does not establish a compatible full SmolLM2 training implementation. The [authors' repository](https://github.com/SafeAILab/zkDL) describes an MLP backend and lists restoring training support among future work.
- [zkLLM](https://arxiv.org/abs/2404.16109) reports an inference proof for a 13B model, with proving under 15 minutes and proof size under 200 kB. Its inference result does not cover our optimizer and backward graph. There is an [official CUDA implementation](https://github.com/jvhs0706/zkllm-ccs2024).
- [The June 2026 frontier-training proposal](https://arxiv.org/html/2606.05433v1) explicitly lists floating-point GEMM verification, backward kernels, hardware anchors and protocol tooling as open problems. Its appendix explains why ordinary field-based Freivalds checks do not reproduce rounded BF16/FP32 computation. Projected costs and its proposed 36-month development horizon are not an available implementation.

## Small experiment

The accompanying `integer_relation_probe.py` checks one synthetic integer product of dimensions 256 × 576 × 1536. It uses two prime fields, fresh verifier randomness after hashing private input copies, and eight projections per field. Explicit operand/output bounds ensure that a nonzero integer discrepancy cannot disappear modulo both primes. The conditional arithmetic error bound is at most the smallest modulus to power −8, under the stated exact arithmetic and independent challenge assumptions. This does not account for a deployed randomness or commitment protocol, which does not exist here.

The probe rejects a modified entry, a discrepancy hidden modulo one field, and a discrepancy hidden modulo both fields that violates the range bound. Binary64 BLAS can evaluate its modular projections exactly because every integer product and partial sum is below 2^53; reductions occur in int64. That bounded case does not license approximation checks for arbitrary floating-point neural operations.

Measured complete verification was about 0.188 seconds median. Naive int64 multiplication took about 0.977 seconds, but the optimized exact product took about 0.0108 seconds. The latter is exact in this particular bounded int8-input example because all binary32 products and partial sums fit its exact integer range. Comparing only with naive int64 would misleadingly suggest a useful speedup. The verifier is roughly 17.5 times slower than the optimized baseline in this probe, before communication.

All measurements include concurrent activity from the existing services, the learning run and input reconstruction. There are only three timing repetitions. They are a rejection of the current prototype as a performance solution, not a reliable production benchmark.

## What remains

An integer training profile would require its own useful-learning test, exact nonlinear and surrogate-gradient semantics, overflow proofs, graph bindings, artifact availability, and a challenge protocol that resists advance prediction and grinding. The present check proves none of those. Public weights and data do not inherently require zero knowledge, so a later design may avoid that extra requirement, but still needs sound integrity checks and measured end-to-end costs. Any follow-up must beat the optimized execution path, including transfer, commitments and retries.


## Follow-up: bounded projections without modular reduction

A second probe uses fresh 16-bit integer challenge coordinates and eight columns. For a fixed nonzero integer error row, conditioning on all but one coordinate leaves at most one coordinate value that can cancel the dot product, giving an algebraic undetected-error bound of 2^-128 under independent challenges. This is an application of the existing randomized matrix-checking idea, not a new full-training proof. [Slalom](https://arxiv.org/abs/1806.03287) is relevant prior work applying randomized linear checks to neural inference with trusted hardware; its trust and inference scope differ from NeuroShard's target.

At the measured shape and int8 operand bounds, every multiplication and partial sum in the projected products remains below 2^53 in magnitude. Binary64 can therefore compute these integer relations exactly without modular reductions. The maximum conservative bound is 949,963,550,883,840. This reasoning does not hold for arbitrary rounded FP32 computation.

The first seven-repeat run measured complete verification at about 57.8 ms and the optimized exact product alone at 7.45 ms. A follow-up measured matching private snapshots, range checks and commitment hashes for both verification and optimized replay: medians were 51.78 ms and 54.02 ms, respectively; the product alone was 6.03 ms. A roughly 4% end-to-end difference on this shared host is not an established performance advantage. Both runs are retained. The bounded checks rejected positive/negative modifications, field-alias-sized changes, a rank-one error and an out-of-range value; an input-bound edge case passed. These few tests do not measure a 128-bit failure probability.

The source and measurements are integer_projection_probe.py and integer_projection_result*.json. No distributed commitment/randomness protocol, full neural graph, useful integer-training recipe or GPU comparison is supplied. Input authentication and materialization dominate this small CPU case. A future implementation would need to reduce repeated artifact work safely and beat the complete optimized replay path, including network costs.