forgo.cloud
Sign in
Repo workspace

forkjoin-ai/gnosis

Gemma4 Inference Speedup — Mesh-Voting-Backed Angles

docs/GEMMA4_SPEEDUP_BRIEF.md
forkjoin-ai/gnosis

Gemma4 Inference Speedup — Mesh-Voting-Backed Angles

Short version: four angles compose to ~8× prefill speedup on existing softmax gemma4 weights, zero retraining, formally bounded error. Two further angles require retraining and are deferred.

The unlock: the mesh-attention = voting-system identity means multi-head attention's sum-over-heads is a mesh fold, and FFN's column-parallel sum is a mesh fold. Tensor-parallel sharding is formally exact — not an approximation. Parallelism is free in the formal sense; engineering cost is comm overhead, not numerical error.

TL;DR — the deployable four

Angle Status Per-layer / structural gain Lean citation
5. Head tensor parallelism (WASM threads in-node) Ships today — kernel rewrite 4–8× per layer on 4-vCPU, no accuracy loss TensorParallelism.headShardingExact
6. FFN column parallelism Ships today — kernel rewrite 4–6× per layer on FFN, no accuracy loss TensorParallelism.ffnColumnShardingExact
4. Median-shift + charisma-floor truncation Ships today — kernel rewrite 0.87–0.90× per layer cost, bounded error InferenceSpeedup.droppedMassLinearBound + massConservation
2. Early exit via cumulative IIA deficit Ships today — coordinator gate 40–60% layers run on easy tokens InferenceSpeedup.earlyExitCumulativeBound

Composed on easy tokens: 15–25× theoretical, 5–10× realistic after comm overhead. Weighted on typical prefill: ~8× end-to-end.

Ordering plan — ship cheapest-first

Step What Cost Cumulative speedup
1 Paris validation (in flight) baseline
2 8 vCPU Cloud Run bump config change only ~2×
3 Head TP inside single node, WASM threads kernel rewrite + SharedArrayBuffer build ~8×
4 Angle 2 coordinator gate (early exit) TS gate, already scaffolded ~14× (on easy tokens)
5 Angle 4 kernel (median-shift truncation) kernel rewrite ~16× (on easy tokens)
6 Cross-node head TP (formal self-shape, speculative pipeline) full mesh rewrite ~20×+

After step 3 you're at ~8× prefill — ~1.5 min per token instead of ~13s/layer × 60. Paris validates in ~5 min total. That kills the 60-min timeout problem.


Angle 5 — Head tensor parallelism (the self-shape match)

The formal identity

Gemma4-31B has 32 attention heads per layer, each operating on independent Q, K, V slices of the hidden dimension. The multi-head output is exactly a sum over heads:

multi_head_output = Σ_h (W_o_h · head_h_output)

where W_o is block-decomposed as W_o = [W_o_0 | W_o_1 | ... | W_o_{H-1}]. Each term W_o_h · head_h_output is self-contained on its worker. Gather + sum = allreduce. Mesh fold.

TensorParallelism.headShardingExact proves this in Lean: the sum of per-worker partial aggregates equals the monolithic aggregate on the flattened multi-head mesh. Exact, not approximate. No accuracy loss from sharding.

Why this is the self-shape match

MeshAttentionAsVoting.meshAttentionAsVotingMaster already proved multi-head attention is a MultiHeadElection in the formal voting-system sense. Each head is a voter; the aggregator is aggregateAbsorbed; the aggregator is linear by aggregateLinear. Sharding = distributing voters across polling stations. Allreduce = sum-of-tallies. The math was already a fold; we just let the runtime match the proof.

Associativity + commutativity = free topology choice

TensorParallelism.headShardingAssociative + headShardingCommutative together prove: the partition topology (how heads are grouped across workers) and gather order (ring / tree / butterfly allreduce) are load-balancing choices, not correctness decisions. You can add/remove workers mid-run, change topology at deploy time, use any allreduce pattern — output is bit-identical.

Implementation — step 3 of the ordering

In-node WASM threads (the cheapest head-TP win):

  • Cloud Run container: 1 process, N WASM worker threads sharing a SharedArrayBuffer
  • Per layer: split 32 heads into 4 groups of 8. Each worker computes its group.
  • After local head_outputs, each worker computes its partial W_o_h · head_h_output contribution.
  • Barrier + sum into the residual stream.
  • On 4 vCPU + 4 WASM threads: ~4× per layer speedup. On 8 vCPU with the bump from step 2: ~8× per layer relative to current single-threaded baseline.

Cross-node head-TP (step 6 — the full mesh fold):

  • Heads split across the existing 10-node pipeline cluster at layer-group granularity.
  • gRPC allreduce between nodes, ring topology OK by commutativity theorem.
  • Comm overhead becomes the bottleneck (not compute) at high TP degree; realistic ceiling ~8 workers.

What gemma4 needs to know

Nothing. The weights are unchanged. Only the runtime kernel layout changes — Q, K, V weight tiles are physically sharded across workers at load time. The math is identical because addition is commutative.


Angle 6 — FFN column parallelism

The formal identity

Gemma4-31B FFN (gated variant used by Gemma/Llama):

FFN(x) = W_down · (activation(W_up · x) ⊙ (W_gate · x))

Shapes: W_up: [5376 → 21504], W_gate: [5376 → 21504], W_down: [21504 → 5376].

Column-split W_up and W_gate along the intermediate dim (21504 divides evenly by 8, 16, 32). Each worker computes a slice of the intermediate activation locally. Row-split W_down correspondingly. Final output is:

FFN_output = Σ_i W_down_i · (activation(W_up_i · x) ⊙ (W_gate_i · x))

Sum over workers = mesh fold. TensorParallelism.ffnColumnShardingExact proves the sharded sum equals the monolithic FFN output.

Why this composes independently of Angle 5

Head TP partitions on the head axis. FFN column TP partitions on the intermediate axis. They are orthogonal axes — no cross-interference. You can apply both in the same layer simultaneously.

Impact on gemma4-31b

FFN dominates per-layer cost (~60% of layer, vs attention at ~40%). Splitting 21504 → 21504/N across N workers gives ~`N/comm_overhead` × speedup. Practical: 4–6× on the FFN portion alone, so ~3–4× on the layer.

Implementation

Per-worker local state: W_up_i, W_gate_i, W_down_i (the i-th vertical slice of each weight matrix). Loaded once at startup from R2 cache (already warm per your fleet telemetry). Forward pass: local matmul, local elementwise activation + gate, local W_down_i · act_i, allreduce sum into the residual stream.


Angle 4 — Median-shift + charisma-floor truncation

Unchanged from prior brief. Quick recap:

  • Subtract per-row score median (softmax is shift-invariant — exact null op)
  • Apply charisma Nat floor: drop the ~50% of positions now below zero
  • Softmax over the kept set only (drop both num and denom — see pedantry below)
  • Skip V-matmul on dropped positions

Pedantry: masked positions must be excluded from the softmax denominator. Element-wise scores · mask with mask[i] = 0 yields exp(0) = 1 for every dropped slot, inflating the sum.

// CORRECT
const keptIdx = shifted.map((s, i) => s > 0 ? i : -1).filter(i => i >= 0);
const keptScores = keptIdx.map(i => shifted[i]);
const maxK = Math.max(...keptScores);
const exps = keptScores.map(s => Math.exp(s - maxK));
const Z = exps.reduce((a, b) => a + b, 0);
const w = new Float32Array(scores.length);
keptIdx.forEach((origIdx, k) => { w[origIdx] = exps[k] / Z; });

Bounded error: ||out_approx − out_true||_∞ ≤ 2 · (Z_dropped/Z_full) · max|V|. Runtime-observable. Peaky attention (meaningful tokens): ≤5% dropped mass. Flat attention (BOS, ambiguous context): >20% possible — runtime guardrail falls back to full softmax when Z_dropped/Z_full > 0.15.

Per-layer gain: ~10–13% weighted. Compose with Angles 5 + 6 + 2 for the multiplicative stack.

Formal backing: InferenceSpeedup.partitionLengthSplit, droppedMassLinearBound, massConservation, keptMassExact, zeroThresholdKeepsPositive.


Angle 2 — Early exit via cumulative IIA deficit

Unchanged. Ships today via apps/edge-workers/src/lib/distributed-inference/charisma-divergence.ts. Formal backing: InferenceSpeedup.earlyExitCumulativeBound + earlyExitZeroSuffixExact. Per-token gate in recordAndGate. Calibrate τ on 500 grounded tokens.

Low-entropy tokens exit by layer 15–25 → 2–4× prefill on that class. High-entropy tokens run full stack → 1×. Weighted: ~1.5–1.8× on typical code / prose.


Composition — the end-to-end number

Multiplicative composition because each angle attacks a disjoint cost surface:

Token class Angle 5 (Head TP) Angle 6 (FFN TP) Angle 2 (layers run) Angle 4 (per-layer) Combined
Low-entropy 0.5 0.88× ~28× theoretical, ~10× realistic
High-entropy 1.0 0.88× ~14× theoretical, ~6× realistic
Weighted (code/prose) 0.7 0.88× ~20× theoretical, ~8× realistic

The "realistic" column assumes 30–50% comm overhead on allreduce. That's a conservative estimate on Cloud Run gRPC; in-node WASM-thread barriers are much cheaper.

Bottom line for Paris validation: after step 3 of the ordering (head TP in-node, ~8× cumulative), the 13s/layer becomes ~1.5s/layer, total prefill ~1.5 min. Comfortable inside the 60-min timeout.


Pre-existing deliverables the other agent can import

  • apps/edge-workers/src/lib/distributed-inference/charisma-attention.ts (271 L) — charisma kernel.
  • apps/edge-workers/src/lib/distributed-inference/charisma-divergence.ts (155 L) — emits HeadDivergenceMetric.
  • apps/edge-workers/src/lib/distributed-inference/gcp-layer-node.ts — plug-in point.
  • open-source/gnosis/lean/Lean/ForkRaceFoldTheorems/InferenceSpeedup.lean — Angles 2 + 4 formal backing.
  • open-source/gnosis/lean/Lean/ForkRaceFoldTheorems/TensorParallelism.lean — Angles 5 + 6 formal backing.
  • open-source/gnosis/lean/Lean/ForkRaceFoldTheorems/MeshAttentionAsVoting.lean — underlying self-shape identity.
  • open-source/gnosis/lean/Lean/ForkRaceFoldTheorems/HallucinationSteering.lean — IIA deficit structural theorems.

Blocked angles — future work only

Angle 1 (sparsity skip, charisma-native): requires charisma-trained weights. Does not apply to existing softmax gemma4. InferenceSpeedup.skipZerosPreservesSum proves it exact for charisma aggregators.

Angle 3 (charisma draft / softmax verifier spec decode): requires training a charisma variant. Months of compute. Bench expects 2–3× throughput once available. Accept-rate geometry: InferenceSpeedup.l1EqualsIiaSum.


Things that fix the 13s/layer number independent of our work

Each composes multiplicatively with Angles 2, 4, 5, 6:

  1. INT8 runtime compute quantization (weights already Q4; compute is F32). 2–4× matmul speedup.
  2. Batched prefill — if not already.
  3. Tiled block-matmul for cache locality. 1.5–2× on d=5376.

For the other agent — the minimum-sufficient instruction

Immediate (cost-free): bump Cloud Run to 8 vCPU. Re-measure Paris. Should drop to ~6.5 s/layer.

Next (kernel rewrite — the big unlock): implement head tensor parallelism using WASM threads with SharedArrayBuffer in a single container. Shard 32 attention heads across 4 workers. Per-worker local Q_i, K_i, V_i, local head output, local W_o_i · head_i, then Atomics.wait barrier + sum into residual stream. TensorParallelism.headShardingExact in InferenceSpeedup.lean guarantees bit-identical output; any allreduce topology works (headShardingAssociative + headShardingCommutative). Expected: ~4× per layer on 4-vCPU, ~8× with the 8-vCPU bump.

Then: FFN column parallelism using the same WASM thread pool. Split W_up, W_gate along dim-21504 axis (divides by 8). Row-split W_down correspondingly. Each worker: W_up_i · x, elementwise gate, W_down_i · act_i, allreduce sum. TensorParallelism.ffnColumnShardingExact is the correctness proof. Expected: ~4× per layer on FFN — composes with head TP orthogonally.

Then: Angle 2 coordinator gate using the already-shipped charisma-divergence.ts. Calibrate τ on 500 grounded tokens.

Then: Angle 4 kernel (median-shift truncation). Pedantry non-negotiable: drop masked positions from both numerator and denominator of the softmax, not element-wise multiply. Runtime guardrail: fall back to full softmax when Z_dropped/Z_full > 0.15.

Composed: ~8× end-to-end prefill on realistic traffic after step 3, ~10–20× once all four angles land. Paris timeout problem goes away after step 3.

Do not touch Angles 1 or 3 — those require retraining.