An unofficial weight-only 4-bit NVFP4A16 / W4A16 quantization of mistralai/Leanstral-1.5-119B-A6B, an open-source Lean 4 code-agent model from Mistral AI.

The routed MoE experts are quantized to NVFP4; attention, shared experts, routers, embeddings, norms, and the language head are kept in higher precision. The resulting checkpoint is intended for text-only vLLM serving.

TL;DR: Leanstral 1.5 119B-A6B, routed-experts-only NVFP4A16, about 68 GB on disk, served successfully with vLLM 0.24.0 on a single NVIDIA DGX Spark / GB10 using the MARLIN NvFp4 MoE backend.

Base Model

Leanstral 1.5 is designed for Lean 4 theorem proving and formal verification. The base model card describes it as part of the Mistral Small 4 family with:

MoE: 128 experts, 4 active per token
Model size: 119B parameters, about 6.5B active per token
Context length: 256k tokens, with <=200k recommended by the base card
Input modality: text and image in the base model; this quantized build is validated for text-only serving

See the base model card for full intended-use details: mistralai/Leanstral-1.5-119B-A6B.

What Is Quantized

Component	Precision	Notes
Routed experts (`layers..experts..w{1,2,3}`)	NVFP4A16 / W4A16	36 layers x 128 experts x 3 matrices = 13,824 expert projections
Attention / MLA projections	BF16	Materialized from the official FP8 checkpoint using `qscale_weight`
Shared experts	BF16	Always-on path; kept out of FP4 quantization
Routers and routing metadata	BF16 / F32	Kept unchanged
Embeddings, `lm_head`, norms	BF16 / F32	Kept unchanged

The final vLLM-ready checkpoint contains:

weight_packed / weight_scale / weight_global_scale triplets for all 13,824 routed expert projections
no remaining .qscale_act or .qscale_weight tensors
no remaining FP8 .weight tensors

Format & Footprint


Format	`compressed-tensors`, `nvfp4-pack-quantized`, weight-only W4A16
Structure	E2M1 4-bit packed weights + FP8-E4M3 group-16 scales + FP32 global scales
Checkpoint form	Mistral consolidated `params.json` / `tekken.json` / `consolidated*.safetensors`
Disk size	about 68 GB
Validated serving stack	`vllm/vllm-openai:v0.24.0`

Weight-Reconstruction Fidelity (SQNR)

SQNR was measured against the official FP8 checkpoint after materializing each source weight with its qscale_weight:

source_real_weight = fp8_weight.to(fp32) * qscale_weight.to(fp32)

The dequantized NVFP4 routed expert weights were compared against that materialized source. This avoids the common mistake of comparing against raw FP8 storage values.

Scope	Modules	SQNR
Full routed experts, global	13,824	20.536 dB
Per-module mean	13,824	20.535 dB
Per-module median	13,824	20.537 dB
`w1` projections	4,608	20.535 dB
`w2` projections	4,608	20.537 dB
`w3` projections	4,608	20.535 dB

The full measurement covers all 36 layers, all 128 routed experts, and all three expert matrices (w1, w2, w3). SQNR measures weight fidelity only; task-level Lean proof accuracy must be measured separately with a Lean compiler-based benchmark.

Compiler-Checked Lean Evaluation

In addition to SQNR, this build was evaluated with a small local Lean 4 compiler-checked benchmark. The model was asked to complete theorem proofs and the generated proof bodies were checked by lean. Any output containing sorry, admit, axiom, or unsafe was counted as a failure.

Benchmark	Judge	Setting	Result
Lean 4 core/prelude theorem set	Lean 4.31.0 compiler	32 proofs, temperature 0.0, max tokens 512	27/32 = 84.4% pass@1

This benchmark uses only Lean's core/standard prelude and does not require mathlib. It is useful as a sanity check that generated proofs compile, but it is not an official miniF2F, ProofNet, or mathlib-project benchmark.

The same 32-case run was repeated three times after the corrected qscale-aware conversion and produced the same score each time:

Run	Pass@1
1	27/32 = 84.4%
2	27/32 = 84.4%
3	27/32 = 84.4%

Observed failures were mostly proof-state tracking errors: re-introducing already-bound hypotheses, failing to destruct existential witnesses, swapping Iff.mp / Iff.mpr, and giving a constructive-looking proof for classical double-negation elimination.

No official miniF2F, ProofNet, or mathlib score is reported for this upload. Small miniF2F/ProofNet canary probes were useful for debugging the evaluation harness, but they were not robust enough to publish as task-level benchmark numbers.

Smoke Evaluation

The model was smoke-tested through the OpenAI-compatible vLLM API at max_model_len=131072. Short prompts produced coherent outputs:

Prompt type	Observed behavior
Arithmetic sanity check	`2 + 2` -> `4`
Logic sanity check	Correct concise statement of modus ponens
Lean-style proof body	Produced plausible Lean 4 proof snippets for simple propositions

Example smoke output:

lean

theorem imp_trans_example (p q r : Prop) (hpq : p -> q) (hqr : q -> r) : p -> r := by
  intro hp
  apply hqr
  apply hpq
  exact hp

These smoke tests only verify that the quantized model is not obviously corrupted. They are weaker than the compiler-checked benchmark above and are not a substitute for larger pass@k evaluation on miniF2F-style, ProofNet-style, mathlib, or project-specific theorem sets.

Practical Notes From Use

Compared with the earlier local qscale-unaware build, this corrected build is clearly better: it more reliably recognizes real APIs, and its tracking of purchase flows and boundary conditions is reasonable. However, it still has a tendency to overproduce false positives around concurrency issues. It should be used only in workflows that include the skill-defined human cross-check against the actual source code, API documentation, and runtime behavior before acting on its findings.

For high-stakes code-review or formal-verification work, treat the model as a strong assistant for hypothesis generation and proof/code drafting, not as an autonomous verifier.

Serving With vLLM

Install or use a container with vLLM >= 0.24.0. The base model card also expects recent mistral_common support for Leanstral.

This build is a weight-only FP4 model. On GB10 it is served by vLLM with the MARLIN NvFp4 MoE backend. Let vLLM choose the MoE backend automatically.

Minimal text-only serving command:

bash

vllm serve kamiyugi/Leanstral-1.5-119B-A6B-NVFP4A16 \
  --served-model-name leanstral-nvfp4 \
  --tokenizer-mode mistral \
  --config-format mistral \
  --load-format mistral \
  --quantization compressed-tensors \
  --max-model-len 131072 \
  --gpu-memory-utilization 0.85 \
  --tool-call-parser mistral \
  --reasoning-parser mistral \
  --enable-auto-tool-choice \
  --generation-config vllm \
  --skip-mm-profiling \
  --limit-mm-per-prompt '{"image": 0}'

Notes:

--quantization compressed-tensors is passed explicitly because this consolidated Mistral-format checkpoint can otherwise be misdetected as FP8.
The quantized checkpoint has been validated for text-only serving. The base model is multimodal, but image input was not validated for this build.
--skip-mm-profiling and --limit-mm-per-prompt '{"image": 0}' are used to keep startup on the text path.
Start with a shorter --max-model-len such as 4096 when validating a new machine, then raise it after loading and generation are confirmed.

How It Was Made

Started from the official FP8 Mistral consolidated checkpoint.
Reindexed the safetensors shards for model-free routed-expert processing.
Materialized FP8 source weights with qscale_weight before quantization.
Quantized only routed expert matrices with llm-compressor using the NVFP4A16 scheme.
Removed stale FP8 activation/weight scale tensors from the final vLLM-ready checkpoint so non-quantized modules load as BF16 and routed experts load as compressed-tensors NVFP4.

Important: an earlier local conversion that compared and quantized raw FP8 storage values was discarded. The SQNR numbers above are from the corrected qscale-aware build.

Limitations

This is an unofficial quantization, not a Mistral AI release.
Weight-only NVFP4 reduces storage and memory, but may change behavior versus the official FP8 model. Evaluate on your Lean projects before relying on it.
The reported Lean score is a small local core/prelude compiler benchmark, not a full official miniF2F, ProofNet, mathlib, or project-specific pass@k score.
Multimodal/image input is not validated for this quantized build.
Local smoke tests showed improved practical behavior versus the previous qscale-unaware local build, but concurrency analysis may still produce many false positives and needs human verification.

License

Apache License 2.0, inherited from the base model mistralai/Leanstral-1.5-119B-A6B.

Acknowledgements

Base model by Mistral AI. Quantization built with llm-compressor, compressed-tensors, and vLLM.