Answering my own thread, since I have now done the exercise.
First, thanks to @ksson — the tabulation was the answer on the cumulative product, and the other thread is closed so I could not say so there.
On the list above, the one I would now put first is honesty, and not for the reason I gave. I had it as a filter for how a pass was obtained — pragma Assume, SPARK_Mode Off, an empty postcondition. It is also a check on the tasks. Translating the set into SPARK turned up:
- four tasks whose postconditions are unsatisfiable — self-contradictory as written, so nothing could pass them and anything scored as “failing” them was right to;
- one permanently unprovable because of a preamble the solver is not allowed to edit — from outside, indistinguishable from a model failure;
- at least one needing a lemma the prover does not have — the cumulative-product task. Three models of very different sizes, handed the known-good invariant, all produced the correct algorithm and the correct bound, and gnatprove still refused.
None of that was visible while the suite was being run as scores. So, to answer my own “what would you add”: a benchmark must ship with a proof that each task is satisfiable. Otherwise part of what it measures is itself.
The third item is worth a paragraph, because it explains something in the published cross-language figures that reads as a result about languages. 8 of 9 frontier models solve that task in Dafny, 0 of 9 in Lean, 0 of 9 in Verus. Dafny’s integers are unbounded, so the obligation never arises. The task is not hard and the models were not failing at it — the bounded-integer translation made the difficulty, and the scores read it as a property of the models. Any cross-language benchmark has this problem, and I do not think it is usually separated out.
The method rule I took from it, which is cheap and I would recommend to anyone measuring this: when a task resists, hand the solver the known-good answer. Whatever refuses afterwards is not the solver.
On the 30B run I linked above — that 25/26 should be read with all of the above in mind. It is a real number under a fixed budget, and it is also a number from a task set I have since found defects in. I would rather say that than let it stand as a clean result.
@ksson mentioned the frontier-versus-open-weights gap in the other thread. A datapoint rather than a contradiction: everything in the two repositories I posted earlier this evening was emitted by a 27B open-weight model running locally.
That is not evidence the gap has closed — one package took three attempts, and the specifications are written by hand in prose first. It is evidence that a proof gate changes what the gap costs you, which is why “harness share: single shot against retry with prover feedback” is on the list above and I now think it is the most load-bearing line on it.
I can contribute the task set, the defects and the SPARK translations if anyone wants to build this properly.