PaperlayerView exact revision on arXiv

Source-linked AI summary

Seal, Then Sample: Sampled Layerwise Proofs for Verifiable LLM Inference from GPT-2 to 70B

Youki Lim, Sam Yong

arXiv:2609.27367v1cs.CRcs.IR

TL;DR

Outsourced language-model inference proofs can be too costly for large transformers, while returned tokens alone do not identify the computation performed. SLP commits chunk boundaries before sampling and proves selected chunks, with measured cost reductions for sampled and packed proofs; its guarantees and fidelity remain bounded by the stated scope.

  • Problem

    Large-transformer proof workloads and representation memory exceed ordinary inference by orders of magnitude, while returned tokens alone do not identify the computation that produced them.

    Source: §1 · p. 1

  • Method

    SLP commits every chunk boundary before sampling, proves verifier-selected chunks plus endpoint-binding chunks, and packs concurrent requests into a trace with per-request prompt and answer binding.

    Source: §1 · p. 1, §3.4 · p. 5

  • Results

    Seven of 47 TinyLlama chunks take 22% of the time and 7% of the proof size of proving all 47; twelve packed requests take 6.5 times less proving time than separate proofs at the measured single-proof cost.

    Source: §1 · p. 1, §10 · pp. 13–14

  • Takeaways & Limitations

    SLP provides a configurable audit interface over one set of commitments, but its guarantees apply to proven chunks rather than unproved interior transitions.

    Source: §2.4 · p. 3, §10 · p. 13

    A manifest-only Fiat-Shamir schedule can be ground through retries, so the adaptive audit model requires an externally ordered challenge.

    Source: §3.2 · p. 4

Abstract

from arXiv · show

Verifying outsourced language-model inference requires a precisely identified computation and an audit whose cost a service can afford. We present Sampled Layerwise Proofs (SLP), a protocol and prototype that commits the boundary activations of every chunk of an inference trace, absorbs all commitments before any challenge is drawn, and then proves a verifier-selected subset of chunks together with the chunks that bind the prompt and the answer. Audit coverage becomes a runtime parameter over one set of commitments: on a TinyLlama-1.1B trace, proving seven of 47 chunks takes 22.0% of the time and 6.8% of the proof size of proving all 47. Because proof cost is dominated by weights rather than tokens, SLP packs concurrent requests into one trace under a block-diagonal causal mask and binds the prompt and answer of each request to its slot. Twelve packed requests are proved in 181.9 s, 6.5 times less than twelve separate proofs at the measured single-proof cost, and a simulated service proves twelve requests at 30.6 s per request with 0.6 s of verification each, rejecting a tampered answer. Disk-backed integer weights and streamed polynomial commitments let a single Llama-2-70B run complete on a 2 TB CPU host: 163 chunks sealed, five proved, a 4.34 MiB proof in 1,259 s, verified in 46.3 s without the weights. The proven object is a fixed-point canonical model; we trace a severe fidelity loss to the residual-stream bit width, repair it with an LLM-aware observer, and measure 84.8-84.9% argmax agreement with the floating-point reference over 334,705 WikiText-2 test positions. The limits are stated as precisely: guarantees cover proven chunks only, a fixed invalid chunk in the 70B setting is covered with probability 3/161, a manifest-only Fiat-Shamir schedule can be ground at 12.5 ms per attempt and needs an externally ordered challenge, and all measurements use a test reference string.

1 Introduction

SLP makes inference audit coverage adjustable by committing every chunk boundary before sampling and proving selected chunks plus prompt- and answer-binding endpoints. It also addresses proof-cost scaling through packed requests and streamed 70B registration, while measuring fidelity and protocol limits.

1 Introduction

  • SLP makes the proved computation adjustable: after committing boundary activations, it selects chunks while always proving those adjoining the input and output; larger samples increase coverage, and selecting every candidate recovers full coverage.Source: §1 · p. 1
  • SLP commits every chunk boundary before deriving a verifier-selected sample, always proves the input- and output-adjoining chunks, and permits later escalation to full chunk coverage over the same commitments.The verifier checks boundary connections and arithmetic within selected chunks.Source: §1 · p. 1
  • Twelve concurrent requests are packed into one trace with per-request prompt and answer binding, achieving 6.5 times less proving time than separate proofs at the measured single-proof cost.The design uses a block-diagonal causal mask and lockstep decoding; the simulated service rejects a tampered answer.Source: §1 · pp. 1–2
  • A manifest-only Fiat-Shamir schedule can be ground at 12.5 ms per attempt, so the library separates sealing from proving and accepts an externally ordered challenge.The stated protocol gap arises when a worker can inspect the sample and repeat after fabricating a boundary.Source: §1 · p. 2
  • A Llama-2-70B sealing, sampled proof, and verification run completes on a 2 TB host using disk-backed integer weights and bounded-batch weight commitments.Loading and commitment stages peaked at about 387 GB resident memory, while inference still materializes model-sized integer state.Source: §1 · p. 2
  • An LLM-aware observer repairs residual-stream quantization damage, yielding 84.8-84.9% argmax agreement with the floating-point reference over 334,705 WikiText-2 test positions.The generic observer compressed the residual stream to 12 bits and produced nonsense; the repair keeps it at about 24 bits.Source: §1 · p. 2

2 Computation, Commitments, and Scope

The paper defines verification as a proof of a registered fixed-point relation, while separating circuit semantics from proof-system soundness. Its scope depends on authenticated configuration and challenge assumptions, and its audit strengths range from endpoint-only to full chunk coverage.

2.1 The object being verified

  • The encoded relation covers chunk boundary inputs and outputs, registered weights, and an internal witness; identifying it with the intended model requires the rounding, range, normalization, and token-selection rules to be constrained as intended.The authors have not proved that every witness admitted by the normalization approximation range yields the same output tokens.Source: §2.1 · p. 2
  • A receipt is only a compact audit handle: a registry must also bind normalization parameters, graph interpretation, tokenizer revision, decoding policy, and backend version to the verification context.The implementation exposes SHA-256 digests for linear weights and activation-scaling metadata.Source: §2.1 · pp. 2–3
  • The fidelity comparison is with an f32 execution in the same framework under specified input construction, not arbitrary fp16 services or other frameworks or quantization schemes.A proof of canonical replay does not establish that an earlier native floating-point execution occurred.Source: §2.1 · p. 3

2.2 Backend and representation

  • The prototype uses HyperKZG over BN254 and Blake3, but all performance results use locally generated test parameters that are not secure against their generator.Deployment requires appropriately sized, authenticated parameters from a ceremony and authenticated verification contexts.Source: §2.2 · p. 3

2.3 Actors and adversary

  • The worker may fabricate states, skip computation, change precision, return another answer, or influence chunk selection, but the adaptive audit model assumes it cannot predict or bias the challenge before the manifest is fixed.It may refuse after an unfavorable challenge; handling refusal is left to external policy.Source: §2.3 · p. 3

2.4 Audit strengths

  • Zero random candidates still proves input and output anchors, while all candidates yield full chunk coverage conditional on the backend and encoded relation, not proof of physical computation performed.Freivalds checks are described as a separate diagnostic, not an integrated commitment-bound audit tier for LLM matrix products.Source: §2.4 · p. 3

3 Seal-Then-Sample Protocol

SLP commits a complete inference-trace manifest before deriving a verifier-controlled sample, then proves selected chunks and the chunks binding the input and output. Its conditional coverage is configurable, but unproved interior relations remain unchecked and adaptive deployment requires externally ordered challenges.

3.1 Registration and complete manifests

  • Sealing fixes a complete manifest of shared chunk-boundary commitments, but does not prove that its values came from an honest execution.The model-derived plan determines anchors and candidates, and the prover must supply exactly the anchors plus selected candidates.Source: §3.1 · pp. 3–4

3.2 Challenge generation and external ordering

  • The transcript absorbs the manifest before sampling; adaptive audits additionally require an external challenge and one accepted manifest per request obligation.Manifest-only Fiat–Shamir sampling can be ground by repeatedly fabricating manifests, while retries or alternative manifests preserve that advantage unless uniqueness is enforced.Source: §3.2 · p. 4

3.3 What acceptance establishes

  • Coverage bounds are conditional on binding commitments, rejected invalid anchors, sound selected proofs, and uniform sampling; missing an invalid candidate leaves it unchecked.The trace has no error-correcting encoding that amplifies one invalid chunk into multiple sampled inconsistencies.Source: §3.3 · p. 4
  • 3/161 (1.863%) is the coverage probability for a fixed single invalid candidate in the recorded 70B plan, with three sampled candidates among 161.The plan proves five chunks total, including two anchors; five is not the sample count.Source: §3.3 · p. 4

3.4 Anchors and verification

  • Input and output anchors bind the proof to the public prompt and claimed answer, while six verifier checks validate the plan, manifest, sample, proofs, and anchor relations.Anchors reject an answer changed after proof fixation but do not establish that interior arithmetic is correct.Source: §3.4 · p. 5

3.5 Full coverage and escalation

  • Full coverage can reuse commitments and boundaries, but requires a new proof object, retained trace, and service-arranged execution; the 70B all-candidate run was not performed.Witness reconstruction, sealing, serialization, and communication recur for escalation.Source: §3.5 · p. 5

4 Packed Batch Proving

Packing amortizes weight-dominated proof work by placing concurrent requests in isolated slots of one trace. The layout defines a distinct computation, and a shared sample gives the batch—not each request—one set of audit challenges.

4.1 Layout and block-diagonal mask

  • A block-diagonal causal mask isolates equal-length request slots, while lockstep decoding advances them together and each prompt plus continuation must fit its slot.The layout fixes slot offsets, capacities, and prompt lengths.Source: §4.1 · pp. 5–6

4.2 Per-slot binding and verification

  • Each slot’s committed tokens are checked against its public prompt and claimed continuation, binding returned text to the request it represents.The layout is part of the registered computation configuration.Source: §4.2 · p. 6

4.3 Position semantics and non-interference

  • Neighboring-slot changes leave a fixed slot’s outputs unchanged token for token, but nonzero-offset slots can differ from standalone execution.Rotary positions and fixed-point rounding cause the differences, so fidelity to floating point must be measured for the registered layout.Source: §4.3 · p. 6

4.4 Security accounting of a shared sample

  • A packed batch shares one sampled audit set, so request count does not multiply the opportunities to detect an invalid chunk relation.Detection depends on the batch’s invalid relations and candidate set; cumulative detection counts apply to independent audits, not requests in one batch.Source: §4.4 · p. 6

5 Streamed Registration and Integer Runtime

Streamed registration moves quantized weights and commitment work through bounded disk-backed stages, enabling the measured 70B run on a 2 TB host. Integer storage width remains a constraint on inference residency and the available GPU evaluations.

5.1 Weight residency and streamed registration

  • 387 GB was the peak for 70B loading and quantization, while weight commitment used about 60 GB of working memory.Disk-backed integer tensors are converted to field elements one tensor at a time, with bounded batches and only commitment and reconstruction metadata retained.Source: §5.1 · p. 6

5.2 Integer inference and operator costs

  • 64-bit integer storage keeps a 7B model’s weights at about 56 GB, beyond the 24 GB GPU used here, so GPU measurements stop at 1.1B.A quantized 70B model is larger in memory than its fp16 parent; separating storage width from accumulator width could reduce memory by four to eight times.Source: §5.2 · p. 6
  • After device-side lookup and requantization changes, TinyLlama forward passes took about 1.0–1.4 s at context 32, 4.0 s at context 128, and 26 s at context 512.These were short profiling runs on one device; context 1024 exhausted device memory.Source: §5.2 · p. 6

6 Experimental Evaluation

The evaluation measures sampled and packed proving across GPT-2, TinyLlama, and Llama-2-70B, with most timings based on single observations. It reports cost savings at lower audit strengths and a completed sampled 70B run, alongside functional-negative and grinding tests.

6.1 Platforms, configurations, and evidence status

  • GPT-2, TinyLlama, and Llama-2-70B provide separate measurements rather than a controlled scaling curve; most timings are single observations, and the 70B execution is one run.All proofs use BN254/HyperKZG with locally generated test parameters and the manifest-only, beacon-less challenge schedule; all proofs and verifications were produced on CPUs.Source: §6.1 · p. 7, Table 1 · p. 8

6.2 Same-trace full and sampled proving

  • At five random samples, TinyLlama seal-plus-prove took 22.0% of full-coverage time, proof size was 6.8% of full, and verification took 1.7 s versus 17.7 s.This proved seven of 47 chunks; the full-coverage baseline used the same chunked interface after the monolithic prover overflowed its stack.Source: §6.2 · p. 7, Table 2 · p. 8

6.3 Packed proving and service simulation

  • Twelve packed requests took 15.3% of the derived separate-proof cost, a factor of 6.53; the service simulation averaged 30.6 s proving and 0.63 s verification per request.The packed comparison shares one sampled set; the service rejected a post-proof changed answer token, while its per-request times are amortizations over three windows.Source: §6.3 · p. 7, Table 3 · p. 9

6.4 A complete 70B run

  • Five chunks proved from 163 sealed boundaries in the Llama-2-70B run; weight-free verification took 46.3 s, while integer inference accounted for 97.4% of per-inference time.Registration stages ran at about 387 GB resident memory and a 60 GB working set; the run does not establish a 70B full-coverage cost or fidelity score.Source: §6.4 · pp. 7–8

6.5 Microbenchmarks

  • The synthetic feed-forward sweep supports weight-representation-governed working sets, but adjacent-point growth exponents of 0.2–0.7 do not support one asymptotic exponent or per-parameter memory constant.On TinyLlama, increasing context from eight to sixteen changed proving time from 94.8 to 99.0 s and proof size from 0.43 to 1.41 MiB.Source: §6.5 · p. 8

6.6 Functional negatives and grinding

  • Seven functional-negative tests rejected their respective tampering or mismatch cases; manifest-only grinding averaged the predicted attempts, while a post-seal challenge gives escape probability q per obligation under stated ordering and uniqueness conditions.The measured 12.5 ms per boundary-recommitment attempt is a GPT-2 laptop result; 70B search figures are algebraic.Source: §6.6 · pp. 8–9

7 Canonical-Model Fidelity

The fidelity evaluation diagnoses residual-stream precision as a major source of canonical-model mismatch, then measures agreement with an f32 reference on paired WikiText-2 data. Its conclusions are limited to the tested model, framework, and execution settings.

7.1 Calibration identity and residual precision

  • Keeping the residual stream at about 24 bits restored agreement after the generic 12-bit observer caused degenerate continuations; raising global precision to 16 bits instead exceeded an arithmetic budget.The observer change retained the nominal 12-bit linear-input setting, and MinMax tracking outperformed percentile clipping in the tested scaling paths.Source: §7.1 · pp. 9–10

7.2 Generation-level diagnostic

  • Teacher-forced agreement rose from 16% to about 90% after the observer change, while the 16-prompt first-token estimate remained imprecise.One prompt changes a prompt-level metric by 6.25 points; the 88% first-token result has a 95% Wilson interval of about 64–97%.Source: §7.2 · p. 10

7.3 Paired WikiText-2 evaluation

  • Perplexity rose about 8.5%, true-token accuracy fell 1.3 points, and argmax disagreement was about 15%; the two calibration arms differed by 0.1 percentage points in argmax agreement.The paired comparison used 334,705 scored positions; calibration choice did not affect fidelity at logged precision in this experiment.Source: §7.3 · p. 10

7.4 Repeated GPU execution

  • Repeated inferences matched token-for-token in 16 of 20 comparisons, although a fixed model and input still varied across GPU runs.Ten registrations printed identical calibration, weight, and activation-scale fingerprint prefixes; the variability was attributed to device floating-point execution order.Source: §7.4 · pp. 10–11

7.5 Scope of the fidelity result

  • The fidelity comparison is against same-framework f32 execution, not a matched fp16 or conventional low-bit baseline, and 70B and nonzero-offset packed-slot fidelity remain unmeasured.The reported agreement therefore is not a ranking against fp16, W8A8, GPTQ, or AWQ.Source: §7.5 · p. 11

8 Deployment Implications and Limitations

The deployment discussion separates sampled coverage from stronger claims about correctness, authenticity, and computation performed. It identifies enforcement, scaling, and registration conditions that bound the demonstrated system.

8.1 Coverage, cheating cost, and enforcement

  • At a 10% audit rate, the illustrative penalty condition requires F/g > 537 when single-invalid-candidate coverage is 3/161.The condition assumes a registrar not controlled by the worker, a nonselectable beacon, enforced deadlines, and one accepted manifest per obligation; the figures are not a deposit schedule.Source: §8.1 · p. 11

8.2 Approximate relations and model authenticity

  • Full chunk coverage verifies the encoded relation, but does not establish unique native-model execution or force the advertised computation.Approximate normalization relations lack a network-wide equivalence guarantee, and the paper makes no compute-forcing claim at any coverage.Source: §8.2 · p. 12

8.3 Scalability and empirical validity

  • The largest result is one short-context 70B CPU run; the full 70B relation, 70B fidelity, and standard-task score were not measured.No proving-stage memory peak or memory-versus-sample curve was logged, and inference does not release weights layer by layer.Source: §8.3 · p. 12

8.4 Registration and artifact boundaries

  • Deployment requires authenticated configuration and artifacts, compatible setup, and layout-specific fidelity evidence; the library lacks global request namespacing and seal deadlines.Weight and scale hashes alone are insufficient for the registry boundary described.Source: §8.4 · p. 12

9 Related Work

The related work situates SLP among full transformer proofs, decomposed proofs, audits, and approximate verification. It distinguishes SLP’s sampling, systems, and fidelity contributions from those prior approaches.

9.1 Full and decomposed arithmetic proofs

  • zkLLM and DeepProve supply arithmetic arguments for transformer computations and generated sequences, while zkComposer links partitions through shared activation commitments [Sun et al., 2024; Sanjaya et al., 2026].SLP adds sampled proving and streamed weight commitments in this backend rather than improving full-coverage bounds.Source: §9.1 · pp. 12–13

9.2 Audits and approximate verification

  • SLP’s within-request chunk sampling differs from request sampling, and its approximate relations do not provide a composition theorem for arbitrary local tolerances [Guo et al., 2026; Yao et al., 2026; Bitan et al., 2025].Packing couples requests because several share one sampled set.Source: §9.2 · p. 13

9.3 Quantization and registered behavior

  • The fidelity diagnosis identifies residual-stream handling, rather than calibration data, as decisive for whether the canonical model tracked its parent in the tested pipeline.The paper distinguishes evidence about registered behavior from proof of computation identity; conventional quantization methods remain future matched-comparison baselines [Dettmers et al., 2022; Xiao et al., 2023; Frantar et al., 2023; Lin et al., 2024].Source: §9.3 · p. 13

10 Conclusion

The conclusion presents SLP as a configurable audit over committed chunk boundaries, with measured cost trade-offs and systems execution through 70B. It emphasizes that the guarantees remain bounded by sampled arithmetic coverage and the evaluation setup.

10 Conclusion

  • Proving seven of 47 TinyLlama chunks takes 22% of full-coverage time and 7% of its proof size; packing twelve requests takes 181.9 s, 6.5 times less than separate proofs at measured single-proof cost.The packed simulated service rejected a tampered answer; streamed registration also completed a sampled Llama-2-70B run on a 2 TB host, with verification in 46 s without weights.Source: §10 · pp. 13–14
  • The repaired canonical model achieved 84.8–84.9% argmax agreement with the floating-point reference over 334,705 WikiText-2 positions.Source: §10 · p. 14
  • A fixed invalid chunk in the measured 70B setting is covered with probability 3/161, and manifest-only Fiat–Shamir scheduling is grindable without an externally ordered challenge.The measurements use a test reference string, and exact verification of a bounded-error relation does not establish unique native-model execution.Source: §10 · p. 14

Declarations

The declarations describe publicly available experiment materials while noting that the modified backend is not included. They also disclose the study’s experimental scope, AI assistance, and the authors’ commercial interest.

Data and code availability

  • Raw logs, extracted tables, the experiment report, manuscript source, derived numerical tables, and figure scripts are publicly available; the modified backend is omitted pending resolution of redistribution status.Source: Declarations · p. 14

Ethics

  • The work uses existing checkpoints, public-corpus material, and diagnostic prompts, with no human participants or newly collected personal data.Source: Declarations · p. 14

AI assistance

  • Claude Code and Codex assisted implementation, analysis, drafting, reference checks, and manuscript preparation; AI-generated reviews were internal aids, not independent human peer review.Source: Declarations · p. 14

Authorship, funding, and competing interests

  • TrueOpen funded the work, both authors are affiliated with it, and the company’s planned deployment of the protocol gives the authors a commercial interest in its adoption.Source: Declarations · p. 14

Related papers

Loading 2609.27367v1…