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
I have a set of tasks lying around that would do for a start, and one public run of a 30B model on the vericoding tasks: SPARK on the vericoding benchmark — what a 30B model did, and did not, do — The Dark Factory
Does anything like this exist already? What would you add or strike?