Skip to content

ZKGadgetEval variance run: no build-vs-LSP gap; range-check-8 is the one hard cell - #13

Merged
LucidSamuel merged 1 commit into
mainfrom
docs/variance-run
Jul 18, 2026
Merged

ZKGadgetEval variance run: no build-vs-LSP gap; range-check-8 is the one hard cell#13
LucidSamuel merged 1 commit into
mainfrom
docs/variance-run

Conversation

@LucidSamuel

Copy link
Copy Markdown
Owner

3-sample variance run (102 sessions, 17 gadgets × 2 modes × 3 samples, budget 5, claude-sonnet-5, 256 min):

Mode Pass rate Mean iters Wall
build 44/45 (98%) 1.07 84 min
lsp 45/45 (100%) 1.07 72 min

Negatives refused 12/12, zero soundness alarms.

Two findings, both recorded in benchmark/RESULTS.md:

  1. Run 1's "build beats LSP" did not replicate. LSP went 45/45 — including range-check-8, its only prior failure — and the wall-time gap reversed. Verdict: no measurable quality difference between feedback modes on this suite; choose on cost/latency. The run-1 claim is kept with a superseded note as a worked example of why single-sample comparisons aren't citable.
  2. Range-check-8 is the suite's one genuinely hard obligation — the sole failure in both runs (different modes each time), and the only cell with pass@1 < 1 (0.67; pass@2 = 1.0; Wilson 95% [0.21, 0.94]). Its 9-constraint bit-decomposition proof is the closest thing to a frontier short of lookup arguments.

Combined across both runs: 118/120 positive sessions proved, 16/16 false specs refused. Raw JSON committed as benchmark/variance-run-2026-07-17.json; README pointer updated.

…he one hard cell

102 sessions (17 gadgets x 2 modes x 3 samples, budget 5, claude-sonnet-5,
256 min): build 44/45, lsp 45/45, negatives refused 12/12, zero alarms.

The first run's 'build beats LSP' headline did not replicate — LSP went 45/45
(including range-check-8, its only prior failure) and the aggregate wall-time
gap reversed; mean iterations are identical at 1.07. Verdict recorded in
RESULTS.md: no measurable quality difference between feedback modes on this
suite; the run-1 claim is kept with a superseded note as a worked example of
why single-sample comparisons are not citable.

Real signal: range-check-8 is the sole failure in BOTH runs (different modes
each time) and the only cell with pass@1 < 1 (0.67, pass@2 = 1.0, Wilson 95%
[0.21, 0.94]) — the suite's one frontier obligation short of lookups.
@LucidSamuel
LucidSamuel merged commit b382088 into main Jul 18, 2026
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant