| --- |
| |
| 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. |
|
|
|
|
