Making a small model write OCaml

Every method we tried to lift Qwen3 4B/8B on LiveCodeBench-multilingual OCaml, ranked by what it bought: 150 held-out problems, 16 samples at t=0.6, pass@1 against the hidden tests, paired bootstrap on every delta. The winning recipe is a stack (distil, GRPO, thinking, best-of-16 by the printed tests) reaching 0.5686 from 0.0733; the 4B follows to within 3.5 points. The verified self-loop lifts the best single sample to 0.3808, and feeding its pools back in at k=50 reaches 0.4059 single-sample and 0.6067 with the test filter. Sonnet 5 one-shots 0.8867 of the same problems.

The stack, stage by stage

Bar is pass@1; the tick is the oracle, the best any picker could do from those same 16 samples. Thinking and best-of-16 are inference-only, so the untrained model gets them too.

Both trained and untrained end within 3 to 7 points of their own oracle: the distance between 0.5686 and 0.4859 is training raising the pool, not the picker improving.

What "distil" means here, precisely

No larger model is involved: the teacher is the same 8B with thinking enabled (0.2545 against 0.0733), and its rollouts become targets with the reasoning trace stripped. The only filter is the type-checker (1,854 of 2,392 kept); filtering harder toward correctness is monotonically worse (0.2263 > 0.2125 > 0.2017). LoRA rank 32, saturating at 2 epochs.

What each family bought

Best arm per method, same base model and eval.

The self-distillation loop: the filter decides whether it compounds or collapses

Each round: k=8 thinking rollouts of the 300 training problems from the previous checkpoint, filter, strip the traces, train a fresh LoRA on the base model; eval thinking, k=16, held-out 150. Every cell is the same measurement: pass@1 on the held-out 150 in thinking mode, estimated from 16 samples per problem. In the charts, solid lines are pass@1 and dashed lines are oracle@16 from the same rollouts (the share of problems where any of the 16 samples passes); the verified line is drawn wider, so on the shared trunk through round 2, where the two chains are the same run, both colors stay visible. The columns differ only in the filter applied to the TRAINING data between rounds: compile keeps every rollout that type-checks; verified keeps only rollouts that pass their own training problem's tests (the train split's suite, never the eval set) and accumulates kept pools across rounds. The chains are identical through round 2 and diverge at round 3. Starting points: untrained 8B 0.2485 (re-measured on the full 150 in the k=50 re-eval), untrained 4B 0.0842; the 4B's round-1 adapter (239 rows) scores 0.2550, so the loop's first and smallest round does most of the lifting.

The compile-filter loop collapses and its own pool hides it: both sizes peak at round 2 and fall, the 4B by 9x the ±0.006 noise floor, while pool pass keeps rising (0.3654 to 0.4029 on the 8B). Verification turns collapse into compounding: keep only rollouts that pass their own training problem's tests, accumulate the pools, and the chain rises to 0.3808. Accumulation alone is not the fix (0.3246), and this was bet against in writing: purity loses to compile-filtering in one-shot distillation, but it is the only filter that resists distribution narrowing.

More data: MBPP-X transfers in only one direction

Matched A/B, both arms a fresh LoRA on base Qwen3-8B, same hyperparameters, pools generated by the same checkpoint; arm B adds Ag-MBPP-X rows to the LCB training set.

The MBPP-X gain is decisive (+0.0618, CI [+0.024, +0.101]); the LCB gain (+0.0092, P=0.723) is indistinguishable from the seed-noise row. Transfer runs one way only, and mixing 52% out-of-domain rows costs nothing on LCB. ±0.006 is the seed-noise floor for single-run adapter comparisons here.

The current best recipe: verified self-loop pools, k=50, broader data

A fresh LoRA on the base model per size, trained on k=50 thinking rollouts drawn from the round-3 verified self-loop checkpoints over both training sets (LCB-train 300 and MBPP-X-train 264), pass-filtered. Evaluated on the same 150 held-out problems at k=50.

Both campaign records, and the pool improved as much as the picker: oracle@50 reaches 0.6933 against 0.6733 for the previous best 8B pool. The nothink rows move the other way (0.1964 and 0.1557 against 0.2246 and 0.1733 for the original distillation): training on verified thinking rollouts buys thinking accuracy and costs direct-answer accuracy.

RL from the base model does not work here

Six levers, each its own trained arm against the same 0.0975 reference.

The graded reward is the informative failure: it lifted gradient-carrying rollout groups from 38% to 95% and still moved only +0.009, not significant. Starvation was real but not binding; the base model's own success rate is.

The prompt is worth as much as the training

Five lines of prompt buy what the RL buys (0.0975 either way), and they stack: sheet + 16 samples + test filter reaches 0.2841 with no training. It hurts the strongest distilled checkpoints (−0.020 to −0.033), so: on for base and RL-band models, off for distilled ones.

Sampling and selecting, against the oracle

The filter uses only tests printed in the problem statement and recovers 92 to 97% of oracle on every arm. It only re-ranks what the sampler produced, so it cannot replace training.

What changes at k=50: the pool is not saturated

The two best thinking arms resampled at 50 per problem, same 150 problems. Everything else on this page stays at k=16; this is the only table where two ks meet.

pass@1 is stable (0.3596 at k=50 against 0.3546 at k=16), so the k=16 rows are not undersampled; the pool keeps growing (oracle +7 points on both arms); and the filter converts part of it, best-of-50 reaching 0.6000. No sample passed the hidden suite while failing the public tests, so the ceiling is set entirely by plausible-but-wrong programs.

Errors by difficulty and failure type

Every sample of every stage, labelled with difficulty and one mutually-exclusive failure reason; compiling-but-failing samples were re-executed against the hidden suite.

What the failures are

Absolute = share of all 16 samples (comparable across stages); relative = share of that stage's failures only.

Training relocates errors more than it removes them: distillation collapses syntax from 33% to 5% of samples and the mass reappears as wrong answers (6.5→24.8%) and timeouts (2.0→10.2%). Thinking converts wrong answers into passes (25.6→10.8%) and pays in truncation (2.2→11.0%), a budget artifact and the clearest remaining lever. The dominant crashes are stdin parsing, the teacher's Scanf pathology at runtime.

Selecting without running anything: the correctness probe

Without a toolchain or sandbox, can a classifier read the model's own activations and pick the right sample? One teacher-forced prefill, mean-pooled hidden states from one layer, logistic regression; baselines are the compile gate and an off-the-shelf LM judge.

Does it discriminate?

The drop from 0.84 pooled to 0.66 within-problem is the whole story: most of what the probe knows is which problem is hard, and only within-problem ranking matters to a selector. An MLP head buys +0.073 AUROC while changing not one selected sample.

The selection ladder

Does the probe know anything the tests do not? On the distilled checkpoint, yes: +0.0156 over the public filter (CI [+0.0036, +0.0303]), closing 70% of the gap to oracle. On the untrained model it moves nothing.

Negative results, and what to distrust

• Probes do not transfer across checkpoints: the base-8B probe on the distilled generator is below chance (0.2200 vs 0.2246 random). One probe per checkpoint.
• Thinking mode degrades it: within-problem AUROC 0.584, CI [0.501, 0.668], barely above chance (55-problem self-split).
• Within-problem AUROC rests on few problems: 37 of 150 (8B), 11 (4B); CIs are wide.
• The ladder is not budget-matched against training: it answers "what to do with 16 samples", not "probe vs fine-tuning".
• The judge baseline is a transfer measurement (adapters trained on LiveCodeBench-Python).

Pipeline and reproduction: experiments/ocaml_clf/ (dataset build, sharded activation extraction, probe training, ladders), reusing the LCB probe tooling unchanged.

The ceiling: Sonnet 5 on the same problems

One reply per problem, no retries, no feedback, no tools: a sandboxed subagent with every tool denied, verified by a live probe; compilation and grading stay on our side. The prompt is byte-identical to the content the Qwen3 arms are evaluated with.

0.8867 in one sample, against 0.4059 for our best single-sample arm: the headroom is capability, not prompt or selection. Sonnet type-checks 96.7% of programs, so the syntax battle that consumes the small models does not exist for it; its 18 failures are almost all semantic.

Replicating the Agnostics paper

Their reported OCaml numbers and ours under their protocol: their prompt, their sampling, their comparator, 20 samples at t=0.2.

Their 8B baseline is the anomaly, not their pipeline: their 4B baseline lands where ours does, and we exhausted the request side. Their headline 8B 0 to 7 is measured against a baseline our replication puts at 4.4. Their 4B gain does not reproduce under LoRA on any axis; full fine-tuning on 8xH100 is the one untested lever. The effect size itself replicates, +6.5 against their +7.

What did not work

• A bigger teacher. The 14B uses Scanf.scanf "%d" in 70% of samples (8B: 11%), collapsing correct-given-compiles from 0.62 to 0.43.
• Full fine-tuning over LoRA. No gain, twice.
• Importance weighting (IGUANA): loses to a hard compile filter by 0.028; deleting the weights is a null, so coverage, not the estimator, was the constraint.
• Training only on correct answers: worse than compile-filtered at matched volume.
• Reasoning traces as targets, and tool-use training: highest usable rate of any arm, no more correct.
• Sequence-sum GRPO loss: diverged at every setting by suppressing EOS; per-token normalization is required, not cosmetic.
• More training. Distillation saturates at 2 epochs.
• Fine-tuning instead of thinking. The distilled nothink model (0.2145) stays below the untrained model with thinking on (0.2545).
• SMC weighting variants. The centered arm collapsed; rank-selection rescued nothing.

Protocol

• 150 held-out LiveCodeBench-multilingual OCaml problems, split by question-id hash, never trained on; 16 samples each at t=0.6. Rows marked 111 probs come from a public rollout dump intersecting our split on 111 of 150: comparable in paired contrasts only.
• pass@1 is the expected pass of one sample, graded by the agnostics exact comparator against the hidden suite.
• Every delta is a paired bootstrap over shared problems, 10,000 resamples; significant means the 95% interval excludes zero.
• Public tests are only those whose input appears verbatim in the problem statement; the hidden suite is never used for selection.
• k=50 thinking cells ran as five 30-problem shards and were merged; the merge refuses unless the shards agree on every decoding parameter and their problem sets are disjoint and complete. A preliminary k=8/16 pass predicted every cell within noise.
• Self-loop rounds retrain a fresh LoRA on the base model each round, so capability differences between rounds are carried entirely by the data. The verified filter uses the hidden tests of training problems only.
• Sonnet rows are one reply per problem from a tool-denied subagent, graded by the same comparator; the full split has 154 problems, of which the standard eval covers 150, and both numbers are reported.