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.

Quick start

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

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.