MathForm-8B-MLX-6bit

6-bit MLX conversion of openbmb/MathForm-8B for Apple Silicon.

This is the balanced variant between the smaller 4-bit build and the higher-precision 8-bit build.

Quantization

• MLX-LM: 0.31.3
• Quantization: 6-bit
• Group size: 64
• Effective weight precision: 6.500 bits/weight
• Model size: ~6.3 GB
• Stored as 7 safetensors shards

Local validation

Tested on:

• Apple M3 Pro
• 18 GB unified memory
• Python 3.12.14
• MLX 0.32.2
• MLX-LM 0.31.3

Validation prompt:

For all real numbers x and y, if x = y then x^2 = y^2.

Result:

import Mathlib.Data.Real.Basic

theorem my_favorite_theorem :
    ∀ x y : ℝ, x = y → x ^ 2 = y ^ 2 := by sorry

Performance:

• Prompt processing: 144.983 tokens/s
• Generation: 19.977 tokens/s
• Peak unified memory: 6.866 GB

Autoformalization validation: PASS

Usage

mlx_lm.generate \
  --model <model-path> \
  --prompt "Please convert the following informal math problem to a formal one in Lean 4 with a header. Use the following theorem names: my_favorite_theorem.

For all real numbers x and y, if x = y then x^2 = y^2." \
  --max-tokens 4096 \
  --temp 0.6 \
  --top-p 0.95

Notes

MathForm is primarily an autoformalization model. Generated Lean code may contain sorry as a proof placeholder.

See openbmb/MathForm-8B for upstream architecture, training details, benchmarks, intended use, and limitations.

License

Apache-2.0, following the upstream model.