--- license: apache-2.0 base_model: - mistralai/Leanstral-1.5-119B-A6B base_model_relation: quantized tags: - gguf - llama-cpp - lean4 - moe - theorem-proving - autoresearch - work-in-progress --- # 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](https://huggingface.co/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](https://huggingface.co/datasets/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](https://github.com/antirez/ds4)'s DeepSeek recipe; built with [llama.cpp](https://github.com/ggml-org/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) ```bash 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.
