File size: 1,638 Bytes
f1aac54 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 | ---
license: apache-2.0
base_model: openbmb/MathForm-8B
tags:
- mlx
- math
- lean
- lean4
- formalization
- qwen3
- apple-silicon
---
# MathForm-8B-MLX-4bit
4-bit MLX conversion of `openbmb/MathForm-8B` for Apple Silicon.
MathForm-8B is focused on mathematical autoformalization and Lean 4. This conversion reduces memory and storage requirements for local MLX inference.
## Quantization
- MLX-LM: 0.31.3
- Quantization: 4-bit
- Group size: 64
- Effective weight precision: 4.500 bits/weight
- Model size: ~4.3 GB
## 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:
```lean
import Mathlib.Data.Real.Basic
theorem my_favorite_theorem {x y : ℝ} (h : x = y) :
x ^ 2 = y ^ 2 := by sorry
```
Performance:
- Prompt processing: 183.786 tokens/s
- Generation: 27.155 tokens/s
- Peak unified memory: 4.839 GB
Autoformalization validation: PASS
## Usage
```bash
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.
|