I have been running a small local model against a set of program-verification tasks — the model writes the code, a prover decides whether it holds. Nothing leaves the machine. Model local, prover local, no API key anywhere.
I found something last night that I would rather not have found.
I ran the same model, same settings, same 58 tasks, four times. It scored 30, 31, 32 and 34. Range of four, on a set of 58. Two things I had written up that morning as findings were inside that range, so I withdrew them.
Then it got worse. A later series of six runs, same tasks, same model, gave 26, 26, 26, 26, 28 and 29. Tight, but nowhere near the first four. In between I had fixed some packaging bugs and the machine was busy with other things. I have not worked out which of those did it, so I am not going to tell you the two series are comparable. That is roughly the state of my confidence in any single number at the moment.
Which means most published numbers on these benchmarks — including the ones I was comparing myself against — are single runs. One draw. A sample reported as a measurement. The frontier results I looked at have zero repair attempts and one shot per task.
The ask. I cannot fix this alone. Repeats are the fix and they are boring and they need hardware. If anyone has an idle GPU and an hour, I would like help collecting draws — same tasks, different machines, different quantisations. It runs entirely locally. There is nothing to sign up to and nothing phones home. You would get your own numbers out of it as well as contributing to a real one.
It is here: GitHub - tonygair/proofbench · GitHub
You need ollama with a code model pulled, gnatprove via Alire, and Go to build the harness. About 1,500 lines. The only HTTP call in it goes to 127.0.0.1 — grep for it, there are three occurrences and they are all that one call.
What I would want back is dull: the score, the model, the quantisation, the hardware, and the run log. Nothing else.
Why I think it is worth the trouble. Software that arrives with a proof you can check yourself is, to my mind, mostly the kind worth making. Not because proofs are elegant — because it is the only version where you do not have to trust the person who sent it to you. Everything else asks you to take a vendor’s word. This crowd seems less inclined to do that than most, which is why I am asking here.
The other thing that came out of it is the argument for repeats. Reading every specification line by line, four of the 58 tasks turned out to be unsatisfiable as written — no implementation can satisfy them, and they had been scoring as model failures for everyone who ran the set. A fifth needs a lemma the prover does not have, so a correct implementation still fails. Six unproved tasks, and only one of them was actually about the model.
The wider thing, since it is all quite new. Everyone is measuring these models against something. My experience over the last day is that the measuring kit is the least reliable part of the setup, and I include my own in that.
In one day I found: a benchmark with unsatisfiable specifications in it; a task that could never pass because an obligation sat in a section the solver is not allowed to edit; a model recorded as failing for two months that turned out to be producing exactly the right answer while the prover refused for want of an identity it does not know; and my own harness running a model at settings its own documentation forbids, which I had written up correctly that same morning and then applied to the wrong program.
My own checks were no better. One reported everything fine while pointed at the wrong file. Another flagged 50 of 58 tasks as broken, then 1 of 58, both times wrong. I only caught the first because a task I knew worked was in the list.
None of that is a complaint about anyone. It is what a young field looks like from the inside. But it does mean I trust a number a great deal less than I did on Monday, and it is why I would rather have four boring repeats from four strangers’ machines than another clever result from my own.
Happy to answer anything, and happy to be told I have this wrong.