Update KV-cache card with accurate template and fork requirements

README.md

@@ -1,101 +1,138 @@
 ---
+license: apache-2.0
 base_model: mistralai/Leanstral-2603
-library_name: transformers
 tags:
   - rotorquant
   - kv-cache-quantization
-  - leanstral
+  - mistral
+  - moe
   - lean4
   - formal-proofs
-  - theorem-proving
   - quantized
-  - mistral
-  - moe
-license: apache-2.0
+library_name: transformers
+pipeline_tag: text-generation
 ---
 
 # Leanstral-RotorQuant
 
-**KV-cache quantized [Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) using [RotorQuant](https://github.com/scrya-com/rotorquant) for high-throughput Lean 4 formal proof generation.**
+**RotorQuant KV cache compression** for [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603).
+
+This is a **documentation repository** that explains how to combine Leanstral's weights with RotorQuant inference-time KV cache compression. No weights are stored here — use the base model directly and apply RotorQuant via the Python package or llama.cpp fork.
 
-Leanstral is the first open-source AI agent purpose-built for Lean 4 formal proofs -- generating both executable code and machine-checkable mathematical proofs. This variant applies RotorQuant KV-cache quantization, delivering **5.3x faster prefill** and **28% faster decode** compared to TurboQuant while preserving full BF16 model weights.
+## What is this?
 
-## Overview
+KV cache compression reduces the memory used by the attention cache during inference. Unlike weight quantization (which is baked into the GGUF/MLX file), KV cache compression is applied at runtime — so the same base weights can be used with or without compression.
 
-This repository provides the **RotorQuant KV-cache-only** configuration of Leanstral-2603. The model weights remain at full precision; only the KV cache is quantized during inference using RotorQuant's rotation-aware quantization scheme.
+| Technique | Where it's applied | Savings |
+|-----------|-------------------|---------|
+| Weight quantization (GGUF/MLX/AWQ) | Baked into model file | Reduces disk + weight memory |
+| **RotorQuant KV cache** | At inference time | Reduces attention memory (critical for long context) |
 
-| Spec | Value |
-|------|-------|
-| Base model | [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) |
-| Architecture | Mistral MoE (~119B parameters, 7 consolidated shards) |
-| Compression | RotorQuant KV-cache quantization |
-| Weight precision | BF16 (unmodified) |
-| KV-cache precision | Mixed-precision quantized |
-| Prefill speedup | 5.3x vs TurboQuant |
-| Decode speedup | 28% vs TurboQuant |
-| License | Apache 2.0 |
-| Use case | Lean 4 formal verification, theorem proving, mathematical proofs |
+Both can be combined for maximum efficiency.
 
 ## Quickstart
 
+### Option A — Python / transformers
+
+Install the `rotorquant` package:
+
+```bash
+pip install rotorquant
+```
+
+Then use it with the base model:
+
 ```python
+import torch
 from transformers import AutoModelForCausalLM, AutoTokenizer
-from turboquant import IsoQuantCache
+from rotorquant import IsoQuantCache
 
-model_id = "majentik/Leanstral-RotorQuant"
-
-tokenizer = AutoTokenizer.from_pretrained(model_id)
+tokenizer = AutoTokenizer.from_pretrained("mistralai/Leanstral-2603", trust_remote_code=True)
 model = AutoModelForCausalLM.from_pretrained(
-    model_id,
+    "mistralai/Leanstral-2603",
+    torch_dtype=torch.bfloat16,
     device_map="auto",
-    torch_dtype="auto",
+    trust_remote_code=True,
 )
 
-# Enable RotorQuant KV-cache quantization
-cache = IsoQuantCache(model)
-
-prompt = "Prove that for all natural numbers n, n + 0 = n in Lean 4:"
-inputs = tokenizer(prompt, return_tensors="pt").to(model.device)
+# Apply RotorQuant to the KV cache
+cache = IsoQuantCache(bits=4)  # or bits=2 for more aggressive compression
 
+inputs = tokenizer("Hello, how are you?", return_tensors="pt").to(model.device)
 outputs = model.generate(
     **inputs,
-    max_new_tokens=512,
+    max_new_tokens=128,
     past_key_values=cache,
+    use_cache=True,
 )
-print(tokenizer.decode(outputs[0], skip_special_tokens=True))
+print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:], skip_special_tokens=True))
 ```
 
+
+### Option B — llama.cpp / LM Studio / Ollama (with fork)
+
+RotorQuant KV cache types (`iso3`) are **not** in upstream llama.cpp. They require:
+- [llama-cpp-turboquant fork](https://github.com/johndpope/llama-cpp-turboquant/tree/feature/planarquant-kv-cache)
+
+Once built:
+
+```bash
+llama-cli -m Leanstral.gguf \
+  --cache-type-k iso3 --cache-type-v iso3 \
+  -ngl 99 -fa \
+  -p "Hello"
+```
+
+For standard runtimes (LM Studio, Ollama, upstream llama.cpp), use conventional KV cache types (`q8_0`, `q4_0`). You lose the RotorQuant-specific benefits but keep GGUF weight quantization.
+
+## Model Specifications
+
+| Property | Value |
+|----------|-------|
+| Base Model | [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) |
+| Architecture | Sparse MoE (128 experts, 4 active) |
+| Parameters | 119B total (MoE) |
+| Context Length | 256K |
+| BF16 Size | ~238 GB |
+| Modalities | Text |
+| License | apache-2.0 |
+
 ## What is RotorQuant?
 
-[RotorQuant](https://github.com/scrya-com/rotorquant) is an advanced KV-cache quantization method that leverages rotation-aware quantization to achieve superior throughput compared to standard KV-cache compression. By exploiting the rotary positional embedding structure, RotorQuant achieves:
+[RotorQuant](https://github.com/scrya-com/rotorquant) is a KV cache compression method based on Clifford algebra (Cl(3,0)) rotors — a faster, more parameter-efficient alternative to Google's TurboQuant. Uses lightweight block-diagonal rotations (independent 2D/4D rotations per pair/quartet) achieving O(d) complexity instead of O(d log d), fully parallelisable with no inter-element dependencies.
+
+**Benchmarks** (from the RotorQuant repository, Llama 3.1 8B on RTX 5090 — results vary by model and hardware):
+
+- Prefill: 3,822 tok/s (vs TurboQuant 722 tok/s)
+- Decode: 119 tok/s (vs TurboQuant 93 tok/s)
+- Perplexity: 6.91 (vs TurboQuant 7.07)
+- Parameters: 4 per rotor (vs TurboQuant 16,384)
 
-- **5.3x faster prefill** -- critical for long Lean 4 proof contexts
-- **28% faster decode** -- faster token-by-token proof generation
-- Equivalent memory savings to TurboQuant with better computational efficiency
+> Benchmarks are from the RotorQuant repository using Llama 3.1 8B. Performance on Leanstral will differ. Please open a discussion if you have independent results.
 
-This makes RotorQuant the preferred choice for interactive theorem proving sessions where latency matters.
+## Current Ecosystem Support
 
-## Memory Estimates
+| Runtime | RotorQuant Support | Notes |
+|---------|----------------------|-------|
+| Python transformers + `rotorquant` | ✅ Full | Drop-in cache class |
+| llama.cpp upstream | ❌ Not merged | Use fork below |
+| llama-cpp-turboquant fork | ✅ `planar3`, `iso3` | [GitHub](https://github.com/johndpope/llama-cpp-turboquant/tree/feature/planarquant-kv-cache) |
+| LM Studio | ❌ [Requested](https://github.com/lmstudio-ai/lmstudio-bug-tracker/issues/1719) | Use `q8_0` as alternative |
+| Ollama | ❌ Not supported | Use `OLLAMA_KV_CACHE_TYPE=q8_0` |
+| vLLM | ❌ Not supported | — |
+| koboldcpp | ❌ Not supported | — |
 
-| Component | Estimate |
-|-----------|----------|
-| Model weights (BF16) | ~238 GB |
-| KV-cache savings | 2-4x reduction vs FP16 KV cache |
-| Recommended VRAM | 4x A100 80GB or equivalent |
+## Pre-quantized weight variants
 
-## Lean 4 Use Case
+If you want combined weight + KV cache compression, majentik hosts pre-quantized versions:
 
-Leanstral excels at:
-- **Formal verification** -- generating machine-checkable proofs of mathematical theorems
-- **Theorem proving** -- interactive and automated proof search in Lean 4
-- **Code generation** -- writing verified Lean 4 programs with correctness guarantees
-- **Proof repair** -- fixing incomplete or broken proof scripts
+- [MLX (Apple Silicon)](https://huggingface.co/majentik?search=Leanstral+MLX)
+- [GGUF (llama.cpp / Ollama / LM Studio)](https://huggingface.co/majentik?search=Leanstral+GGUF)
 
 ## See Also
 
-- [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) -- Base model
-- [majentik/Leanstral-TurboQuant](https://huggingface.co/majentik/Leanstral-TurboQuant) -- TurboQuant KV-cache variant
-- [majentik/Leanstral-RotorQuant-MLX-4bit](https://huggingface.co/majentik/Leanstral-RotorQuant-MLX-4bit) -- MLX 4-bit + RotorQuant
-- [majentik/Leanstral-RotorQuant-MLX-2bit](https://huggingface.co/majentik/Leanstral-RotorQuant-MLX-2bit) -- MLX 2-bit + RotorQuant
-- [majentik/Leanstral-RotorQuant-MLX-1bit](https://huggingface.co/majentik/Leanstral-RotorQuant-MLX-1bit) -- MLX 1-bit + RotorQuant
-- [RotorQuant repository](https://github.com/scrya-com/rotorquant)
+- [RotorQuant GitHub](https://github.com/scrya-com/rotorquant)
+- [TurboQuant paper (arXiv 2504.19874)](https://arxiv.org/abs/2504.19874)
+- [llama-cpp-turboquant fork](https://github.com/johndpope/llama-cpp-turboquant/tree/feature/planarquant-kv-cache)
+- [Base model: mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603)
+- [Leanstral announcement](https://mistral.ai/news/leanstral)