granite-4.2-3b

conformance ✓ spec 1.0 granite The Model Spec of ibm-granite/granite-4.2-3b in TheFormalEra.Spec.Registry. The constants below are transcribed from its published config.json, and the official transformers.GraniteForCausalLM is checked against them.

At a glance


Model key	`ibm-granite/granite-4.2-3b`
Parameters (text model)	3,659,737,600
Layers	40 (40 full attention)
Hidden size	2,560
MLP width	8,192 (silu)
Vocabulary	100,352
Norm	`w·x̂`, ε = 1e-05
Embedding	separate from the LM head
Logits	no soft-capping
Hugging Face class	`GraniteForCausalLM`
Shape domain	`T` ∈ [1, 131,072] tokens, `B` ∈ [1, 256] sequences, `S` ∈ [1, 131,072] cached positions, page size 16

What to watch for

Every layer is full causal attention: 40 query heads, 8 KV heads (5 query heads per KV head), head dim 64.
The attention scale is the checkpoint’s attention_multiplier, 1/64, not 1/√64.
No q/k norms. RMSNorm weights are applied as w, with ε = 1e-5.
RoPE over the full head, θ = 10,000,000. The language-model head is separate from the embedding.

Compute-graph nodes

Use these paths in Spec Keys: ibm-granite/granite-4.2-3b@1.0:layers[*].<node> for per-layer nodes, ibm-granite/granite-4.2-3b@1.0:<node> for the others.

Node	Op Spec	Layers	Formula	Constants
`embed`	`embed`	—	`y[t] = 1 · w[tokens[t]]`	mul=1, norm=False
`input_norm`	`rmsnorm`	all 40	`y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]`	H=2560, eps=1e-05
`attn.qkv_proj`	`linear`	all 40	`y[t,n] = Σₖ x[t,k] · w[n,k]`	K=2560, N=3584
`attn.rope`	`rope`	all 40	`rotate pairs (i, i + 32) by pos · θ^(-2i/64), i < 32; coordinates ≥ 64 unchanged`	D=64, active=32, denom=64, rot=64, theta=10000000
`attn.core`	`decodeGQA`	all 40	`o[b,h] = Σ_{s < seq_lens[b]} softmax_s(1/64 · ⟨q[b,h], k[b,s,h / 5]⟩) · v[b,s,h / 5]`	D=64, heads=40, kv_heads=8, scale=1/64
`attn.o_proj`	`linear`	all 40	`y[t,n] = Σₖ x[t,k] · w[n,k]`	K=2560, N=2560
`attn_residual`	`residual`	all 40	`y = x + h`	H=2560, layer_scalar=False, r=1
`post_attn_norm`	`rmsnorm`	all 40	`y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]`	H=2560, eps=1e-05
`mlp.gate_up`	`linear`	all 40	`y[t,n] = Σₖ x[t,k] · w[n,k]`	K=2560, N=16384
`mlp.act`	`siluMul`	all 40	`y[t,i] = silu(gate_up[t,i]) · gate_up[t,8192+i]`	I=8192, act=silu
`mlp.down`	`linear`	all 40	`y[t,n] = Σₖ x[t,k] · w[n,k]`	K=8192, N=2560
`mlp_residual`	`residual`	all 40	`y = x + h`	H=2560, layer_scalar=False, r=1
`final_norm`	`rmsnorm`	—	`y[t,i] = x[t,i] / √(Σⱼ x[t,j]² / H + ε) · w[i]`	H=2560, eps=1e-05
`lm_head`	`lmHead`	—	`z = x wᵀ`	mul=1, tied=False

Nodes listed twice have different constants in different layers (for example, sliding-window and global attention). A kernel annotated with layers[*].<node> is verified against each variant.

Tensors of the main nodes

Node	Inputs and outputs
`embed`	`tokens` [T], `y` [T, 2560]
`input_norm`	`x` [T, 2560], `y` [T, 2560]
`attn.qkv_proj`	`x` [T, 2560], `y` [T, 3584]
`attn.rope`	`q` [T, 40, 64], `k` [T, 8, 64], `pos` [T], `q_out` [T, 40, 64], `k_out` [T, 8, 64]
`attn.core`	`q` [B, 40, 64], `k` [B, S, 8, 64], `v` [B, S, 8, 64], `seq_lens` [B], `o` [B, 40, 64]
`attn.o_proj`	`x` [T, 2560], `y` [T, 2560]
`attn_residual`	`x` [T, 2560], `h` [T, 2560], `y` [T, 2560]
`post_attn_norm`	`x` [T, 2560], `y` [T, 2560]
`mlp.gate_up`	`x` [T, 2560], `y` [T, 16384]
`mlp.act`	`gate_up` [T, 16384], `y` [T, 8192]
`mlp.down`	`x` [T, 8192], `y` [T, 2560]
`mlp_residual`	`x` [T, 2560], `h` [T, 2560], `y` [T, 2560]
`final_norm`	`x` [T, 2560], `y` [T, 2560]
`lm_head`	`x` [T, 2560], `logits` [T, 100352]

Conformance

The official transformers.GraniteForCausalLM agrees with this spec, layer by layer in float64, to a maximum relative error of 2.3e-15 (reduced-width profile, 2 weight draws × 2 lengths). On the published checkpoint, the full-size spec evaluated by the Lean oracle agrees with the official implementation to 5.1e-15 on a real prompt (121.8 s).

theformalera-conformance verify ibm-granite/granite-4.2-3b                    # the official implementation
theformalera-conformance verify ibm-granite/granite-4.2-3b path/to/model.py   # your implementation
theformalera-conformance spec ibm-granite/granite-4.2-3b                      # the architecture, as Lean derives it

Published configuration

The hyperparameters as the spec renders them (config.json form)

{
  "vocab_size": 100352,
  "tie_word_embeddings": false,
  "rope_theta": 10000000,
  "rope_parameters": {
    "rope_type": "default",
    "rope_theta": 10000000
  },
  "rms_norm_eps": 1e-05,
  "residual_multiplier": 1,
  "num_key_value_heads": 8,
  "num_hidden_layers": 40,
  "num_attention_heads": 40,
  "mlp_bias": false,
  "logits_scaling": 1,
  "intermediate_size": 8192,
  "hidden_size": 2560,
  "hidden_act": "silu",
  "embedding_multiplier": 1,
  "attention_multiplier": 0.015625,
  "attention_bias": false,
  "architectures": [
    "GraniteForCausalLM"
  ]
}

Spec Hub

Qwen

Gemma

Granite

Muse

At a glance

What to watch for

Compute-graph nodes

Tensors of the main nodes

Conformance

Published configuration

​At a glance

​What to watch for

​Compute-graph nodes

​Tensors of the main nodes

​Conformance

​Published configuration

At a glance

What to watch for

Compute-graph nodes

Tensors of the main nodes

Conformance

Published configuration