Leanstral-WhiteDwarf — seed-v3 (EARLY CHECKPOINT, run not complete)

Status: this is an early-stopped checkpoint of an in-progress autoresearch quantization run — the ratchet loop has NOT completed. The trajectory is promising (see numbers), the eval harness is frozen, and the run is designed to be resumed. Steps to continue are at the bottom.

47 GB GGUF of mistralai/Leanstral-1.5-119B-A6B (119B MoE Lean 4 prover, 128 experts / 4 active, MLA) — 39.5% of the FP8 weights, ~3.2 bits/weight effective, targeted at 2×24 GB + 91 GB RAM boxes.

Measured quality (vs the same model's FP8 golden run)

Metric	FP8 golden	this checkpoint	retention
miniF2F-test slice, compiler-verified (4 attempts)	38/120	29/120	76%
PutnamBench slice	1/60	0/60 (partial: 0/10 scored at stop)	—
Teacher-forced top-1 agreement (135×32 tok, Lean)	1.0	0.789	—
Repetition battery (5-turn proof convs)	pass	pass	no degeneration
Decode on 2×RTX 4090 + DDR5 (experts on CPU)	—	33 t/s	—

Verification = Lean 4 compiler in loop (mathlib-pinned), statement anti-cheat, no sorry/admit/native_decide. Golden reference data: SEBK4C/Leanstral-WhiteDwarf-golden.

Recipe (the interesting part)

Routed experts: ffn_gate_exps/ffn_up_exps → IQ2_XXS everywhere (verified safe). ffn_down_exps → Q6_K on layers {0–3, every 3rd, 30–35}, Q4_K elsewhere — this promotion pattern is load-bearing: flattening it to ≤Q4_K produces hard NaN on real Lean input while remaining coherent on casual English (seven falsified recipe variants; test on your target domain, not chit-chat). Everything else (attention/MLA, router gates, shared experts, embeddings, output) Q8_0. imatrix: 1.3M tokens of Lean-domain text (mathlib/STP/LeanDojo), included as imatrix-lean-v1.dat.

Lineage: the asymmetric experts-2bit/rest-Q8 split follows antirez/ds4's DeepSeek recipe; built with llama.cpp (quantized at master bec4772). The last-layers-only protection prior from ds4/DeepSeek does NOT transfer to this arch — early layers have the flattest expert routing and need the most down-projection precision.

Serving (llama.cpp ≥ bec4772 recommended)

llama-server -m Leanstral-WhiteDwarf-seed-v3.gguf \
  --host 127.0.0.1 --port 8080 -np 4 -c 131072 \
  -b 2048 -ub 512 -fa on --jinja \
  --chat-template-file chat_template.jinja \
  -ngl 999 --override-tensor 'ffn_.*_exps.*=CPU'

• Keep expert tensors OFF CUDA (--override-tensor 'ffn_.*_exps.*=CPU'): 2-bit expert tensors on the CUDA backend produced NaN on the builds tested. Non-expert layers + KV on GPU, experts in RAM: ~33 t/s on 2×4090.
• The GGUF embeds no chat template (tekken v15): use the bundled chat_template.jinja (from Leanstral-2603, community consensus for 1.5).
• Sampling per model card: temperature 1.0, top_p 0.95.

Continuing the run

The full harness (program spec, recipes, tiered evals with Lean compiler-in-loop, golden anchors, resume journals) lives in the project repo SEBK4C/Leanstral-WhiteDwarf. Remaining route: finish t2 noise replicas → golden/noise.json → gate check (anchor 0.2167, local verifier) → ratchet loop (first phase: promote ffn_down_exps floor Q4_K→Q5_K until the gate passes, then shrink from above — expected gate-passing size 51–55 GB, then descend). notes/CONTINUE-RUN.md has exact commands for both local (2×4090, ~2 days) and rented-GPU (1×H100-80G, ~hours) execution.