codelion commited on
Commit
625f50d
Β·
verified Β·
1 Parent(s): b36266d

Clean up model card prose (remove em-dashes and inline bold emphasis)

Browse files
Files changed (1) hide show
  1. README.md +48 -44
README.md CHANGED
@@ -27,15 +27,15 @@ model-index:
27
 
28
  # SPROG-9M
29
 
30
- **S**ymbolic **PROG**ram solver β€” a **9.37M-parameter, from-scratch** model that solves
31
- grade-school math word problems **without any LLM at inference time**.
32
 
33
  Instead of generating text, SPROG abstracts the numbers in a question to slots
34
- (`[N0]`, `[N1]`, …) and predicts a **postfix program** over them, which is then executed
35
- symbolically. It draws 96 temperature samples and selects **a single answer** with a **free
36
- symbolic verifier** (0 trainable parameters) that never sees the ground truth β€” i.e.
37
- self-consistency selection, **not** a pass@k oracle. The whole thing runs on a
38
- CPU/Apple-Silicon GPU via MLX.
39
 
40
  Trained on [`codelion/gsm8k-synth`](https://huggingface.co/datasets/codelion/gsm8k-synth).
41
 
@@ -63,50 +63,54 @@ print(solve(model, stoi, "Tom has 15 apples. He buys 27 more, then gives away 12
63
 
64
  ## Results
65
 
66
- Evaluated on the **full GSM8K test set** (1,319 problems), averaged over 3 training seeds.
67
 
68
- **The model commits to one answer per question.** It draws 96 temperature samples, then a
69
- 0-parameter symbolic verifier picks a **single** answer **without ever seeing the gold
70
- answer**. This is a single-answer accuracy (the self-consistency / maj@k family) β€” **not a
71
- pass@k oracle**.
72
 
73
  | metric | GSM8K test | what it measures |
74
  |---|---|---|
75
- | **verifier @ 96** (headline) | **11.8%** (best seed 12.6%) | verifier commits to one answer; gold never used |
76
- | plurality @ 96 | β‰ˆ9.3% | most-voted answer; gold never used |
77
- | pass@96 (oracle) | β‰ˆ39% | gold is *somewhere* in the 96 samples β€” an upper bound that **uses the gold to check** |
78
- | trainable parameters | 9.37M | β€” |
79
- | LLM used at inference | none | β€” |
80
 
81
- So **11.8% is a committed single answer, not pass@96** (that would be the β‰ˆ39% oracle). The
82
- free symbolic verifier adds β‰ˆ+2.5 points over majority voting, at 96Γ— the inference cost of a
83
- single decode. Results are stable across seeds (range 11.1–12.6%).
 
84
 
85
- **Why 96 samples?** Recall rises with sample count (β‰ˆ39% gold-in-pool at 96 β†’ β‰ˆ50% at 288),
86
- but the verifier's *conversion* peaks around 64–96 then declines β€” extra samples add
87
- plausible-but-wrong distractors that hurt selection (measured: 192 β†’ 8.5%, 288 β†’ 8.3%). 96 is
88
- the sweet spot between recall and selectability.
 
 
 
89
 
90
  ## How it was built
91
 
92
- - **Number-slot abstraction.** The model never sees raw numbers β€” they become slots, so it
93
- learns program *structure*, not arithmetic, and generalizes across values.
94
  - **Symbolic program target.** It predicts a postfix program (`[N0] [N1] * [N2] -`) executed
95
  by a tiny deterministic evaluator.
96
- - **Self-consistency + free verifier.** 96 sampled programs are scored by a 0-parameter
97
  symbolic verifier (number-coverage, magnitude sanity, intermediate-value sanity), tie-broken
98
  by vote frequency.
99
- - **Data is the main lever.** Trained on real GSM8K-train plus β‰ˆ117K LLM-generated
100
- GSM8K-style problems (Claude + Gemini). What mattered most was **matching the real GSM8K
101
- step-distribution** and **rigorous decontamination** (0% test overlap), not raw data volume
102
- or model size β€” a deeper/bigger model did not help beyond noise.
103
 
104
  ## Constraints (by design)
105
 
106
- - **≀10M trainable parameters** (9.37M)
107
- - **From scratch** β€” no pretrained weights, no frozen LLM, no linear probe on a foundation model
108
- - **LLM-free at inference** β€” pure MLX + symbolic execution
109
- - **Decontaminated** β€” training data has 0% 8-gram overlap with the GSM8K test set
 
110
 
111
  ## Files
112
 
@@ -117,19 +121,19 @@ the sweet spot between recall and selectability.
117
  | `src_vocab.json` | source vocabulary (6,000 tokens) |
118
  | `inference.py` | self-contained inference (model + slot tokenizer + verifier) |
119
 
120
- ## Why not `mlx-lm` / `AutoModel`?
121
 
122
- SPROG is a custom **encoder-decoder seq2seq** with a **slot tokenizer** and a **symbolic
123
- decode + verify** pipeline β€” not a standard causal LM. So it ships its own `inference.py`
124
- rather than loading through `mlx-lm` or `transformers.AutoModel`. The script has no
125
- dependencies beyond `mlx` and `numpy`.
126
 
127
  ## Limitations
128
 
129
- This is a research model demonstrating how far a tiny, LLM-free, from-scratch solver can go
130
- on GSM8K (β‰ˆ12%). It handles 1–4 step arithmetic word problems with common operations; it
131
- misses many multi-step problems that require deeper reading comprehension. It is not a
132
- general math model and should not be used as one.
133
 
134
  ## License
135
 
 
27
 
28
  # SPROG-9M
29
 
30
+ SPROG (Symbolic PROGram solver) is a 9.37M-parameter, from-scratch model that solves
31
+ grade-school math word problems without any LLM at inference time.
32
 
33
  Instead of generating text, SPROG abstracts the numbers in a question to slots
34
+ (`[N0]`, `[N1]`, and so on) and predicts a postfix program over them, which is then
35
+ executed symbolically. It draws 96 temperature samples and selects a single answer with a
36
+ free symbolic verifier (0 trainable parameters) that never sees the ground truth. That is
37
+ self-consistency selection rather than a pass@k oracle. The whole thing runs on a
38
+ CPU or Apple-Silicon GPU via MLX.
39
 
40
  Trained on [`codelion/gsm8k-synth`](https://huggingface.co/datasets/codelion/gsm8k-synth).
41
 
 
63
 
64
  ## Results
65
 
66
+ Evaluated on the full GSM8K test set (1,319 problems), averaged over 3 training seeds.
67
 
68
+ The model commits to one answer per question. It draws 96 temperature samples, then a
69
+ 0-parameter symbolic verifier picks a single answer without ever seeing the gold answer.
70
+ This is a single-answer accuracy, in the self-consistency family, and not a pass@k oracle.
 
71
 
72
  | metric | GSM8K test | what it measures |
73
  |---|---|---|
74
+ | verifier @ 96 (headline) | 11.8% (best seed 12.6%) | verifier commits to one answer; gold never used |
75
+ | plurality @ 96 | about 9.3% | most-voted answer; gold never used |
76
+ | pass@96 (oracle) | about 39% | gold is somewhere in the 96 samples, an upper bound that uses the gold to check |
77
+ | trainable parameters | 9.37M | |
78
+ | LLM used at inference | none | |
79
 
80
+ So 11.8% is a committed single answer. The pass@96 oracle figure of about 39% is a
81
+ different measurement and an upper bound. The free symbolic verifier adds roughly 2.5
82
+ points over majority voting, at 96 times the inference cost of a single decode. Results
83
+ are stable across seeds, with a range of 11.1% to 12.6%.
84
 
85
+ ### Why 96 samples
86
+
87
+ Recall rises with sample count. The gold answer is in the pool about 39% of the time at 96
88
+ samples and about 50% at 288. But the verifier's conversion peaks around 64 to 96 samples
89
+ and then declines, because extra samples add plausible but wrong distractors that hurt
90
+ selection. We measured 8.5% at 192 samples and 8.3% at 288. So 96 sits at the sweet spot
91
+ between recall and selectability.
92
 
93
  ## How it was built
94
 
95
+ - **Number-slot abstraction.** The model never sees raw numbers. They become slots, so it
96
+ learns program structure rather than arithmetic, and generalizes across values.
97
  - **Symbolic program target.** It predicts a postfix program (`[N0] [N1] * [N2] -`) executed
98
  by a tiny deterministic evaluator.
99
+ - **Self-consistency and a free verifier.** 96 sampled programs are scored by a 0-parameter
100
  symbolic verifier (number-coverage, magnitude sanity, intermediate-value sanity), tie-broken
101
  by vote frequency.
102
+ - **Data is the main lever.** Trained on real GSM8K-train plus about 117K LLM-generated
103
+ GSM8K-style problems (Claude and Gemini). What mattered most was matching the real GSM8K
104
+ step-distribution and rigorous decontamination (0% test overlap), rather than raw data
105
+ volume or model size. A deeper or bigger model did not help beyond noise.
106
 
107
  ## Constraints (by design)
108
 
109
+ - At most 10M trainable parameters (9.37M here)
110
+ - From scratch, with no pretrained weights, no frozen LLM, and no linear probe on a
111
+ foundation model
112
+ - LLM-free at inference, using pure MLX and symbolic execution
113
+ - Decontaminated, with 0% 8-gram overlap between the training data and the GSM8K test set
114
 
115
  ## Files
116
 
 
121
  | `src_vocab.json` | source vocabulary (6,000 tokens) |
122
  | `inference.py` | self-contained inference (model + slot tokenizer + verifier) |
123
 
124
+ ## Why not `mlx-lm` or `AutoModel`?
125
 
126
+ SPROG is a custom encoder-decoder seq2seq with a slot tokenizer and a symbolic decode and
127
+ verify pipeline, so it is not a standard causal LM. It ships its own `inference.py` rather
128
+ than loading through `mlx-lm` or `transformers.AutoModel`. The script has no dependencies
129
+ beyond `mlx` and `numpy`.
130
 
131
  ## Limitations
132
 
133
+ This is a research model showing how far a tiny, LLM-free, from-scratch solver can go on
134
+ GSM8K, which is about 12%. It handles 1 to 4 step arithmetic word problems with common
135
+ operations. It misses many multi-step problems that need deeper reading comprehension. It
136
+ is not a general math model and should not be used as one.
137
 
138
  ## License
139