Split out from my cumulative-product thread, where ksson said there is not much public.
I know ACATS for compilers and spark-by-example as a teaching corpus. I have not found anything that plays the part a benchmark plays elsewhere: a fixed set of specs, a fixed prover budget, a number out.
If we built one, I would want it to measure:
capability: proof-gated pass rate per task, not compile rate
energy: joules per proven task from a meter, inference and prover time separately
cost of a pass: candidates tried, wall seconds, tokens, money, for failures too
honesty: whether a pass used pragma Assume, SPARK_Mode Off or an empty postcondition. Those are not passes
contamination: fitted tasks against held-out ones
prover budget as a constant: level, timeout, provers
harness share: single shot against retry with prover feedback
reproducibility: pinned GNAT, SPARK and solver versions, and someone else getting the same numbers
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.