Leanstral-1.5-119B-A6B-NVFP4A16

Leanstral 1.5 119B A6B - NVFP4A16

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

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

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.

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.

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:

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:

Example smoke output:

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:

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

1. Started from the official FP8 Mistral consolidated checkpoint.
2. Reindexed the safetensors shards for model-free routed-expert processing.
3. Materialized FP8 source weights with qscale_weight before quantization.
4. Quantized only routed expert matrices with llm-compressor using the NVFP4A16 scheme.
5. 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.