P1: Qwen3.8-27B port, tracking (M1 DeltaNet head -> M2 layer -> M3 GPU block)

Tracking issue for the first real-model port. Feasibility: #28. Order (decided): Qwen3.8-27B first, then GLM 5.3 Flash / DeepSeek v4.1 Flash (#11).

P1: Qwen DeltaNet M1, one head at real state shape #33 M1: one Gated DeltaNet head at real 128x128 state, 4 tokens, synthetic, hostile proofs rejected, state growth over 1024 steps (go/no-go)
P1: Qwen recurrent-state commitment strategy #34 State commitment strategy: avoid per-token state commits (~38.7B cells / 1024 tok)
P1: Qwen missing operator constraints #35 Missing operators: 4-tap conv1d, partial rotary 64/256, per-head qk norm, sigmoid gates, softplus/exp decay table, limit loosening
M2: one full layer at exact shape, synthetic weights (CPU)
M3: 4-layer block on one H100 (needs spend approval)

experiments: Qwen DeltaNet M1 review fixes (issue #33, amendments A1-…

M1b (PR #52, draft): KILLED. The lookup smallness test was not wired into the research harness by the deadline, so there is no proof and H1/H2 were not run. The range study alone shows F=12 two-limb delta/v fits 20/20 realistic runs, including R3 (high limb at most 2), and F=10 single-limb fits 20/20 at about 3x the divergence. M2 not started. Next: a dedicated lane for the RNG/LKP + product-oracle composition, or prove F=10 single-limb on the existing M1 harness as a cheap fallback.

research: Qwen DeltaNet head on the wide product oracle with RNG/LKP …

M1b lookup redo opened as draft #63. PREREG is the first commit (bc38a37). The RNG/LKP range check now composes with the wide product oracle in one group, with range cells laid directly on product row a. First honest 128x128 T=4 proof was accepted: prove 39.8 s, verify 7.4 s, 25.4 MB, table 2^21 (M1 was 51 s, 11.6 s, 50 MB, 2^22). The registered runs (H1 10 seeds, H2, H3b R3 windows) are in progress. I'll post the verdict here.

experiments: M1b lookup results, H1 10/10, H2 44/44, H3 pass (Part of #…

M1b lookup verdict (#63): PASS vs prereg, so GO for M2 design. M2 is not started; that decision is the coordinator's. H1: 10/10 accepted, prove median 39.2 s (38.8 to 40.1), verify 7.1 s, 25.4 MB. H2: 44/44 rejected, including the limb-recombination tamper and an out-of-range state cell. H3: 5/5 R3 windows where M1 overflowed now prove. Compared with M1: table 2^21 vs 2^22, 17.4 vs 35.7 columns per state cell per token, proof half the size. Remainder bits are now the dominant cost. Unreplicated, research security (N = 10).

research: Qwen DeltaNet M1b, RNG/LKP smallness test composed with the…

M2 design lane opened: #66 (draft, Part of #32). PREREG landed first (8477689), before any code.

Registered design decisions:

M2 = one V head of one DeltaNet layer at T = 16, from the in_proj outputs to the gated-norm output. The layer matmuls are dense operators that are already proved elsewhere, and the 48-head cost is extrapolated.
Gates, conv1d, SiLU and the q/k L2 norm are functions of public integers at this boundary. The verifier recomputes them. The gated RMSNorm of the now-private o is proved in-relation.
RNG sizing keeps 16 x honest bound <= 2^22.
Remainders get two arms: exact bits vs lookup-exact via direct LKP keys into a 2^12 table.
A verifier entry point that decodes and range-checks its own integer public inputs, with no skippable admissible(). A hostile test sends a huge field element as public o (the research: Qwen DeltaNet M1b, RNG/LKP smallness test composed with the product oracle (Part of #32) #63 review's R9) and must be rejected by the verifier alone.

Verdict to follow on this issue.

research: M2 design prototypes: verifier-side admission, counting mod…

experiments: Qwen DeltaNet M2 design, results and DESIGN.md (Part of #32

research: results.yaml entry for the Qwen M2 design, regenerate READM…

M2 design verdict (#66, draft): PASS on H1 to H5. GO for an M2 build lane, primary arm B (lookup-exact remainders).

M2 scope. One V head, from in_proj outputs to gated-norm output, at T = 16.
- The verifier recomputes conv, SiLU, the L2 norm and the gates from public integers.
- The recurrence and the gated RMSNorm of the private o are proved.
- The matmuls, pre-norm, residual and MLP are not proved.
H1. The count model reproduces M1 and M1b exactly: columns, relations, terms, range cells and log-length.
H2 (remainders). Arm B over arm A at the M1b shape: 0.349 on columns per state cell per token (17.41 to 6.07) and 0.273 on relations.
H3. The M2 head at T = 16 needs a 2^21 table under arm B. Arm A needs 2^23 and does not fit; its largest T is 14.
H4. Whole-head ranges fit 20/20, with every RNG class under 2^18 (16 x 2^18 = 2^22 = D):
- max S' 150,189
- max o 6,379
- max w 4,048
H5 (admission). verify_from_words accepted 10/10 honest runs.
- Derive took a median 0.182 s; verify a median 7.61 s [7.53, 7.86].
- Hostile: 34/34 at the expected stage, including a huge element (p+1)/2 in each of the 8 public classes.
- R9 (o' = o - 2^-F mod p, honest proof): the caller path with admissible() skipped ACCEPTS it. The new entry rejects it at decode.

Open:

Arm B needs a second LKP keyed on product cells. This is not built yet.
Recomputed nonlinearities need pinned tables.
y fidelity is poor at F = 12 (worst error 1.23). That is for M0/P1: quantify integer-model fidelity against pinned BF16 and FP8 references #8.
48-layer extrapolation: 231M product cells per token, so M3 needs chunked state.

experiments: Qwen M2 design, review fixes: witness not private, conv …

PR #66 (M2 design) review fixes are pushed in 2512c97. M2 is now framed as a rehearsal for M3: at its boundary every input is public, so the statement is verifier-computable. The conv history is a public, class-bounded input. Arm B at T = 16 still fits 2^21 with both lookups' multiplicities sized. H5 rerun: honest 10/10 and hostile 41/41, clean under UBSan. The GO for an arm-B build stands. Merge #66 with a merge commit, not a squash.

experiments: Qwen M2 design, second review: disclose D5 deviation, ch…

PR #66: the second review's must-fixes are in 8ec7c79. The PREREG D5 deviation is disclosed (+512 relations at the M1b shape, ratio 0.273 unchanged). The verifier derivation now uses checked i64 arithmetic and returns a derive reject on overflow. The hostile suite passes 44/44 with 0 UBSan reports. Honest 10/10. The GO for an arm-B build stands. Merge with a merge commit.

Navigation Menu

Repository navigation

P1: Qwen3.8-27B port, tracking (M1 DeltaNet head -> M2 layer -> M3 GPU block) #32

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

P1: Qwen3.8-27B port, tracking (M1 DeltaNet head -> M2 layer -> M3 GPU block) #32

Description

Activity

wakesync commented on Nov 4, 2026

wakesync commented on Nov 5, 2026

wakesync commented on Nov 5, 2026

wakesync commented on Nov 5, 2026

wakesync commented on Nov 5, 2026

wakesync commented on Nov 5, 2026

wakesync commented on Nov 5, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions