---
license: mit
library_name: mlx
pipeline_tag: question-answering
tags:
- mlx
- math
- gsm8k
- symbolic
- math-word-problems
- from-scratch
datasets:
- codelion/gsm8k-synth
model-index:
- name: sprog-9m
  results:
  - task:
      type: text2text-generation
    dataset:
      name: GSM8K
      type: openai/gsm8k
    metrics:
    - name: Accuracy (single-answer, self-consistency)
      type: accuracy
      value: 11.8
---

# SPROG-9M

SPROG (Symbolic PROGram solver) is a 9.37M-parameter, from-scratch model that solves
grade-school math word problems without any LLM at inference time.

Instead of generating text, SPROG abstracts the numbers in a question to slots
(`[N0]`, `[N1]`, and so on) and predicts a postfix program over them, which is then
executed symbolically. It draws 96 temperature samples and selects a single answer with a
free symbolic verifier (0 trainable parameters) that never sees the ground truth. That is
self-consistency selection rather than a pass@k oracle. The whole thing runs on a
CPU or Apple-Silicon GPU via MLX.

Trained on [`codelion/gsm8k-synth`](https://huggingface.co/datasets/codelion/gsm8k-synth).

## Quick start

```bash
pip install mlx numpy huggingface_hub
huggingface-cli download codelion/sprog-9m --local-dir ./sprog-9m
python sprog-9m/inference.py -q "A baker had 24 muffins. She sold 3/4 of them, then baked 10 more. How many muffins does she have now?"
# Answer: 16.0
```

```python
from huggingface_hub import snapshot_download
from pathlib import Path
import sys

p = snapshot_download("codelion/sprog-9m"); sys.path.insert(0, p)
from inference import load_model, solve

model, stoi, cfg = load_model(Path(p))
print(solve(model, stoi, "Tom has 15 apples. He buys 27 more, then gives away 12. How many does he have?"))
# 30.0
```

## Results

Evaluated on the full GSM8K test set (1,319 problems), averaged over 3 training seeds.

The model commits to one answer per question. It draws 96 temperature samples, then a
0-parameter symbolic verifier picks a single answer without ever seeing the gold answer.
This is a single-answer accuracy, in the self-consistency family, and not a pass@k oracle.

| metric | GSM8K test | what it measures |
|---|---|---|
| verifier @ 96 (headline) | 11.8% (best seed 12.6%) | verifier commits to one answer; gold never used |
| plurality @ 96 | about 9.3% | most-voted answer; gold never used |
| pass@96 (oracle) | about 39% | gold is somewhere in the 96 samples, an upper bound that uses the gold to check |
| trainable parameters | 9.37M | |
| LLM used at inference | none | |

So 11.8% is a committed single answer. The pass@96 oracle figure of about 39% is a
different measurement and an upper bound. The free symbolic verifier adds roughly 2.5
points over majority voting, at 96 times the inference cost of a single decode. Results
are stable across seeds, with a range of 11.1% to 12.6%.

### Why 96 samples

Recall rises with sample count. The gold answer is in the pool about 39% of the time at 96
samples and about 50% at 288. But the verifier's conversion peaks around 64 to 96 samples
and then declines, because extra samples add plausible but wrong distractors that hurt
selection. We measured 8.5% at 192 samples and 8.3% at 288. So 96 sits at the sweet spot
between recall and selectability.

## How it was built

- **Number-slot abstraction.** The model never sees raw numbers. They become slots, so it
  learns program structure rather than arithmetic, and generalizes across values.
- **Symbolic program target.** It predicts a postfix program (`[N0] [N1] * [N2] -`) executed
  by a tiny deterministic evaluator.
- **Self-consistency and a free verifier.** 96 sampled programs are scored by a 0-parameter
  symbolic verifier (number-coverage, magnitude sanity, intermediate-value sanity), tie-broken
  by vote frequency.
- **Data is the main lever.** Trained on real GSM8K-train plus about 117K LLM-generated
  GSM8K-style problems (Claude and Gemini). What mattered most was matching the real GSM8K
  step-distribution and rigorous decontamination (0% test overlap), rather than raw data
  volume or model size. A deeper or bigger model did not help beyond noise.

## Constraints (by design)

- At most 10M trainable parameters (9.37M here)
- From scratch, with no pretrained weights, no frozen LLM, and no linear probe on a
  foundation model
- LLM-free at inference, using pure MLX and symbolic execution
- Decontaminated, with 0% 8-gram overlap between the training data and the GSM8K test set

## Files

| file | purpose |
|---|---|
| `model.npz` | MLX weights (9.37M, d=304, 4 enc + 4 dec layers) |
| `config.json` | architecture config |
| `src_vocab.json` | source vocabulary (6,000 tokens) |
| `inference.py` | self-contained inference (model + slot tokenizer + verifier) |

## Why not `mlx-lm` or `AutoModel`?

SPROG is a custom encoder-decoder seq2seq with a slot tokenizer and a symbolic decode and
verify pipeline, so it is not a standard causal LM. It ships its own `inference.py` rather
than loading through `mlx-lm` or `transformers.AutoModel`. The script has no dependencies
beyond `mlx` and `numpy`.

## Limitations

This is a research model showing how far a tiny, LLM-free, from-scratch solver can go on
GSM8K, which is about 12%. It handles 1 to 4 step arithmetic word problems with common
operations. It misses many multi-step problems that need deeper reading comprehension. It
is not a general math model and should not be used as one.

## License

MIT.