Upload folder using huggingface_hub

notes/project-report.md

@@ -0,0 +1,190 @@
+# Can a small model check math better than it can do math?
+
+A write-up of what we tried, why, and what we found. It builds on the two research
+notes in this folder (`brainlift.md` and `research-small-vs-large-math.md`) and the
+runs saved under `results/`.
+
+## The question
+
+We wanted to take a small open model, fine-tune it on data we generate, and get it to
+reliably do one narrow thing that a plain prompt cannot: read a step-by-step math
+solution and point to the first step that is wrong. This is usually called process
+verification. We chose it because the background reading suggested it is one of the few
+math tasks where a small specialist has a real chance against a much larger model.
+
+The reason is the generator-verifier asymmetry. Checking a solution is generally easier
+than producing one, so a model that is weak at solving competition problems can still be
+useful at catching mistakes in someone else's work. If that holds, a small verifier is a
+sensible bet.
+
+We wrote the target as a spec so that a stranger could grade any output. Given a problem
+and a numbered solution, the model returns the index of the first incorrect step, or -1
+if every step is correct. We score this on ProcessBench, which reports the harmonic mean
+of accuracy on erroneous solutions and accuracy on correct ones. GPT-4o scores about
+61.9 there, so that was the number to have in mind.
+
+## What the reading told us going in
+
+Three findings from the research notes shaped the plan.
+
+Data matters more than the training run. Results like LIMA and s1 come mostly from a
+small, carefully chosen set of examples, so we put our effort into generating and
+filtering data rather than tuning hyperparameters.
+
+You should distill the process, not the style. Orca points out that copying a teacher's
+final answers teaches surface imitation while copying the reasoning teaches the actual
+skill. We ended up learning this the hard way.
+
+Scale is a real constraint. The math-specific note was blunt that most "small beats
+large" results live at 7B, and that genuine sub-4B wins are thin and usually need extra
+machinery. The clearest sub-4B verifier, GenPRM at 1.5B, only beats GPT-4o when it also
+runs generated Python to check arithmetic and votes over several samples. We noted this
+and started at 1.5B anyway, partly to see the ceiling ourselves.
+
+## How we built it
+
+The pipeline has three parts, and we reused all three across every experiment.
+
+Data. We took step-level labels from PRM800K, which are human judgments of where a
+solution first goes wrong. For each solution a frontier model (Claude, through a company
+gateway) wrote a paragraph-by-paragraph critique. We removed any training problem that
+also appears in ProcessBench or MATH-500, so we were not training on the test set.
+
+Training. QLoRA on Qwen2.5-Math, first the 1.5B instruct model and later the 7B. We
+trained the verifier as an ordinary generative model with supervised fine-tuning. The
+version of TRL we used has no dedicated process-reward trainer, and a generative verifier
+is what the GenPRM result used, so this was both the practical and the principled choice.
+
+Evaluation. ProcessBench for the main number and PRMBench as a harder, adversarial check.
+Both use exact, objective scoring, so there is no model acting as judge and no judge bias
+to worry about.
+
+## What happened
+
+### The first data recipe did not work
+
+Our first version told the teacher the correct answer and asked for a matching critique.
+This was a mistake. The critiques read well, but they were written backward from the
+answer, so they contained no real error-finding. The 1.5B model trained on them picked up
+the format and not the skill. On ProcessBench it caught errors about as often as the
+untuned base, and the only thing it clearly improved at was confidently declaring
+solutions correct. It learned to say "looks fine." That is the failure Orca describes.
+
+### The second recipe was honest but hit a wall
+
+We rebuilt the data so the teacher critiqued each solution without seeing the answer, and
+we kept a critique only when its predicted error index matched the PRM800K label. This is
+rejection sampling, and it gave us critiques that actually located the error. The keep
+rate was about 77 percent, and the kept set came out roughly balanced between erroneous
+and correct examples on its own. We also raised the LoRA rank, since a genuinely hard
+skill should need more capacity than a small low-rank update.
+
+It still did not move the score. At 1.5B the model kept defaulting to "all correct,"
+predicting -1 about 90 percent of the time on the gsm8k subset. More data and more
+capacity did not help, which usually means the problem is capability rather than data.
+
+### Why it was stuck
+
+The failure was not uniform across the test set, and that was the useful part. On
+PRMBench the same model flagged an error about 41 percent of the time, much more often
+than on gsm8k. The difference is the kind of error each set contains. PRMBench's injected
+errors are often structural, like circular reasoning or a step that contradicts an
+earlier one, and those can be caught by reading carefully. The gsm8k errors are
+arithmetic, and a 1.5B model cannot reliably redo the arithmetic, so it falls back on
+"looks fine." This matches GenPRM, which needed a Python interpreter for exactly this
+reason.
+
+### Two things that helped
+
+We tried the code-execution idea first, because it can be run at inference on a model we
+already had. We let the verifier write short Python snippets, ran them, and fed the
+output back before it committed to an answer. On the 7B base this roughly doubled
+error-localization on gsm8k, from about 11 to 21 (accuracy on erroneous steps), which is
+the arithmetic-heavy split where we expected it to matter.
+
+Moving from 1.5B to 7B helped on its own. The untuned 7B stopped collapsing to "all
+correct" on the harder subsets and localized errors at a real rate, where the 1.5B could
+not. This is the plainest evidence we have for the "wins live at 7B" point from the note.
+
+### Results so far
+
+Numbers are ProcessBench F1 on a 100-example sample per subset, greedy decoding, on the
+0-100 scale (so GPT-4o's 61.9 is the reference). These are sensitive to decoding
+settings; we say more about that below.
+
+| model | gsm8k | math | olympiad | omnimath | avg | notes |
+|---|---|---|---|---|---|---|
+| 1.5B base | ~16 | | | | | prompt alone is weak |
+| 1.5B tuned (v2) | ~16 | | | | | collapses to -1 (~90%) |
+| 7B base | 12-21 | ~14 | ~13 | ~9 | ~12-21 | stops collapsing on hard subsets |
+| 7B base + code-exec | ~32 | ~33 | | | | gsm8k acc-error ~11 to ~21 |
+| 7B tuned | pending | | | | | final eval to fill in |
+
+The gsm8k -1 rate tells the story cleanly: 1.5B tuned sits around 0.90, while the 7B base
+is 0.83 on gsm8k but drops to about 0.21-0.25 on olympiad and omnimath, meaning it
+actually attempts to localize on the harder problems.
+
+## What we take from this
+
+The honest headline is narrower than "small model beats big model," and that is fine. A
+small fine-tuned model can help on the easy side of the generator-verifier asymmetry, but
+only where the check is cheap for the model to run. For structural reasoning errors a
+1.5B model can contribute. For arithmetic it cannot, at least not without a calculator,
+and adding the calculator is what closes most of the gap. Capability (7B) and tools (code
+execution) push in the same direction, which is the direction GenPRM already pointed.
+
+On the project's own framing, the dataset really was the deliverable, but not the way we
+first assumed. The first dataset was large and clean and still taught the wrong thing,
+because the examples encoded justification instead of detection. Fixing what the examples
+taught mattered more than making more of them.
+
+We also spent more time on plumbing than expected. Getting QLoRA, the eval harness, and
+the Colab setup to behave took several rounds of debugging, and a few of our early numbers
+were held down by eval bugs rather than by the model (a repetition penalty that fought the
+verifier's own format, a token budget that cut long critiques before they finished, and a
+scale mix-up where our fractions were sitting next to a percentage). We mention this
+because it changes how much to trust any single run.
+
+## Evaluations
+
+We ran these:
+
+- ProcessBench, base versus tuned, on all four subsets. This is the main number and the
+  base-versus-tuned comparison the assignment asks for.
+- PRMBench, which injects errors of specific types. This is the robustness check, and it
+  is where we found that the model does better on structural errors than arithmetic ones.
+- A prediction-distribution readout (how often the model says -1, gives an index, or
+  fails to parse). This is a calibration check, and it is what exposed the "collapse to
+  all-correct" failure that a single F1 number hides.
+- A code-execution ablation, the same model with and without the Python tool. This
+  isolates the arithmetic-verification effect.
+
+Others that fit the assignment's rubric and are worth running:
+
+- Test-time scaling with majority voting (Maj@k). GenPRM's headline needs it. Our harness
+  supports it, but it only helps once the base verdicts are decent, so it is a later step.
+- The composition eval, where the verifier reranks a separate generator's samples and we
+  measure the lift in final-answer accuracy. This is the most direct "why does this
+  matter" test, since a verifier is only useful if it improves a downstream result. We
+  have the pieces but have not built the generator half yet.
+- Consistency under perturbation. Take a solution the model handles, rename variables or
+  reorder independent steps, and check that the verdict does not change. This targets the
+  consistency dimension of the rubric and the fragilities the brainlift lists.
+- A contamination-controlled held-out set. We already deduplicate training against the
+  eval sets, but a fresh set would make the numbers harder to argue with.
+
+## What we would do next
+
+The verifier is only half of the original plan. The other half is a generator, and the
+point of having both was to measure the asymmetry directly by having the verifier rerank
+the generator's samples. We have the code for this but have not run it.
+
+After that, the clear next steps are the full GenPRM recipe on the 7B, meaning code
+execution together with majority voting, and a held-out set to rule out contamination.
+
+## Artifacts
+
+- Datasets and model on Hugging Face: `42e/mathcompose-verifier` (data),
+  `42e/mathcompose-verifier-7b` (the tuned adapter), `42e/mathcompose` (code snapshot).
+- Eval outputs in `results/`, and the earlier detailed failure analysis in
+  `results/M1_verifier_findings.md`.