docs: upstream-first KV-cache guidance (q8_0/q4_0, mainline Hadamard rotation); fork demoted to experimental
Browse files
README.md
CHANGED
|
@@ -18,6 +18,23 @@ tags:
|
|
| 18 |
license: apache-2.0
|
| 19 |
---
|
| 20 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 21 |
# Leanstral-RotorQuant-MLX-2bit
|
| 22 |
|
| 23 |
**2-bit MLX weight-quantized [Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) with [RotorQuant](https://github.com/scrya-com/rotorquant) KV-cache quantization for high-throughput Lean 4 formal proof generation on Apple Silicon.**
|
|
|
|
| 18 |
license: apache-2.0
|
| 19 |
---
|
| 20 |
|
| 21 |
+
> [!TIP]
|
| 22 |
+
> **KV-cache quantization without any fork (recommended, 2026):** upstream
|
| 23 |
+
> llama.cpp/Ollama now cover this natively — use `-ctk q8_0 -ctv q8_0`
|
| 24 |
+
> (~half KV memory, negligible quality loss: perplexity +0.002–0.05) or
|
| 25 |
+
> `-ctk q4_0 -ctv q4_0` (~quarter memory, ≈7.6% perplexity increase). In
|
| 26 |
+
> Ollama: `OLLAMA_KV_CACHE_TYPE=q8_0` with `OLLAMA_FLASH_ATTENTION=1`. Keep
|
| 27 |
+
> K and V types symmetric to stay on the fast fused Flash-Attention path.
|
| 28 |
+
> Since April 2026, mainline llama.cpp also applies Hadamard rotation to
|
| 29 |
+
> KV activations ([PR #21038](https://github.com/ggml-org/llama.cpp/pull/21038)),
|
| 30 |
+
> which greatly improves low-bit KV quality (opt-out:
|
| 31 |
+
> `LLAMA_ATTN_ROT_DISABLE=1`).
|
| 32 |
+
>
|
| 33 |
+
> The RotorQuant/TurboQuant fork flow below is **experimental/legacy**: the
|
| 34 |
+
> TurboQuant llama.cpp PR was closed without merging (June 2026) and the fork
|
| 35 |
+
> is unmaintained relative to mainline. It is NOT required to use this model.
|
| 36 |
+
<!-- kv-upstream-note -->
|
| 37 |
+
|
| 38 |
# Leanstral-RotorQuant-MLX-2bit
|
| 39 |
|
| 40 |
**2-bit MLX weight-quantized [Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) with [RotorQuant](https://github.com/scrya-com/rotorquant) KV-cache quantization for high-throughput Lean 4 formal proof generation on Apple Silicon.**
|