Metraipolis › archive › dc_4c8564f1044a

SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work — arXiv:2609.11076

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.11076
License (as archived): CC0-1.0
Archived: 2026-10-16T05:57:33.416Z
SHA-256 of the archived text: e55cc2dcaae63a214eb97ecb90db367dbca4642d9c5ae222c58846fd56c65594
Stable URL of this page: https://metraipolis.com/documento/dc_4c8564f1044a

How to cite

SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work — arXiv:2609.11076 — arXiv (en), https://arxiv.org/abs/2609.11076 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_4c8564f1044a (Metraipolis archive dc_4c8564f1044a, sha256 e55cc2dcaae63a214eb97ecb90db367dbca4642d9c5ae222c58846fd56c65594)

BibTeX

@misc{dc4c8564f1044a,
  title = {SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work — arXiv:2609.11076},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.11076},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_4c8564f1044a; sha256 e55cc2dcaae63a214eb97ecb90db367dbca4642d9c5ae222c58846fd56c65594},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.11076. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

SaltBench asks how a machine referee (a proof kernel, program verifier or withheld test suite) changes how a coding agent works. Outcomes are decided outside the agent's toolchain; a wall probed before any scored run isolates the agent from the network, reference solutions and harness; a dated freeze of predictions authorizes each run; a budget stop is a halt, never a failure. Five Rust systems components on a pinned Verus toolchain are each refereed by a withheld test suite. The arms: plain; salt-diet, also instructed to specify and verify its code (a registered reduced rendering of the method); and two arms handed the specification a priori, where the registered sign test at k=4 reached no verdict (3 of 4, p = 0.3125). salt-diet cost more on all five components, by a practical margin: no premium exceeded 2.8879x under either reading of the declared set and the three cheapest sat below 1.4x, a bound of this population and not a promise about larger ones: the premium is near 1 on the smallest components and rises with size. Versions 2 and 3 add the complete pilot matrix: 200 conditions over four models, 181 with a result of record, 16 inexpressible and 3 declared unreached at the cost cap, costed in tokens, dollars and wall time, with no verdict on the arms. Version 3 adds a correctness reading, declared post hoc and registered after every verdict it reads existed and many had been read by its author: 447 cells pass the withheld suite, 40 fail, 10 are censored at a registered budget, 4 are unscorable and 42 are read by condition. salt-diet's pass-rate interval lies wholly below plain's on 8 greenfield and 5 brownfield rows and wholly above it on 2 greenfield rows. It is descriptive, over three cells of record per condition, with no test, and says nothing about whether the method makes code more or less correct. The full record is public.

Tema degli esploratori: calcolo e infrastrutture (retro-catalogo arXiv: annunci del 2026-09-11 in cs.SE).
Categorie arXiv: Software Engineering (cs.SE) ; Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2609.11076 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-16T05:45:13.292Z dalla pagina https://arxiv.org/catchup/cs.SE/2026-09-11?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).