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.

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

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.