Source-linked AI summary
SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work
Jason Hickey
TL;DR
SaltBench asks how machine referees change coding-agent work while preventing agents or experimenters from narrating outcomes afterward. It preregisters isolated, machine-checked comparisons and finds that specification-and-verification instructions cost more across five systems components, within this population’s observed bounds.
Problem
SaltBench addresses the need to measure machine-referee effects without relying on agents’ self-reports or post hoc experimenter interpretations.
Method
The protocol uses isolated seats, externally decided referee outcomes, pre-registered comparisons, and four arms varying specification-and-verification instructions and specification provenance.
Results
The specification-and-verification arm cost more on all five components, while no premium exceeded 2.8879× and the three cheapest were below 1.4×.
Takeaways & Limitations
The observed cost premium is specific to this five-component population, with premiums near 1 on the smallest components and rising with size.
Takeaways & Limitations
The registered k = 4 sign test reached no verdict, and the design provides no correctness verdict for scored cells or causal join between cost and correctness.
Abstract
from arXiv · showhide
SaltBench is a benchmark protocol for one question: How does a machine referee change the way a coding agent works? A machine referee --- a proof kernel, a program verifier, or a withheld test suite --- decides what an agent's work is worth, and the agent cannot argue with it. Here we report a protocol that makes the referee's effect measurable and whose answers cannot be narrated afterwards: every outcome is decided outside the agent's own toolchain; the agent is walled off from the network, the reference solutions and the harness itself, and the wall is tested by probes that try to breach it before any scored run, so the isolation is observed rather than assumed; every run is authorized by a dated freeze with its predictions registered; and a budget stop is a halt, never a failure. In this study, the subject of the benchmark is a ``seat'', meaning an agent session in its standard harness. We tested five systems components, all authored in Rust under a pinned Verus toolchain, with a withheld test suite as the referee for each. Four arms are tested: a plain agent; an agent that is also instructed to create a specification and verify the code against it, in a reduced rendering of the method, as registered; and two arms where the specification is provided a priori, extended under a dated amendment to $k=4$, where the registered sign test reached no verdict (3 of 4, $p = 0.3125$, every premium below the resolvable floor). We found that the arm instructed to specify and verify cost more on all five components, and by a practical margin: across these five components no premium exceeded $2.8879\times$ under either reading of the declared set, and the three cheapest sat below $1.4\times$. That bound is a property of this population and not a promise about larger ones: the premium runs near $1$ on the smallest components and rises with size. We publish the complete record.
1 Introduction
SaltBench addresses the unreliability of agent self-reports by fixing machine-refereed outcomes and comparisons before runs. It reports a seat-level benchmark measurement and a registered, reduced rendering of the Salt method.
- Motivation and protocol: SaltBench fixes outcomes through an external machine referee and fixes comparisons before runs, preventing post-hoc narration of results.The protocol uses a proof kernel, program verifier, or withheld test suite outside the agent’s toolchain, with pre-registered populations, arms, predictions, adverse outcomes, and freeze commits.
- Contribution: The paper measures a working seat end to end rather than treating the model alone as the experimental subject.The reported experiment combines the agent session, harness, and workspace in the benchmark subject.
- Scope: The study claims a protocol, a seat-as-subject design, an authored population, and the cost reading returned by the run, but no treatment effect on referee acceptance.The paper explicitly reserves population-magnitude claims for later tests and records the scope of its current claims.
- Method: The tested Salt arm is a registered, reduced rendering of the method that a single sealed agent can carry.The rendering was limited to the solo-executable portion of the formal mathematics workflow before the first call.
2 The seat-as-subject experiment
The experiment treats the agent session, harness, and workspace as the subject and compares method instructions across an authored five-component Rust population. Its four-arm design separates writing a specification from verifying against one supplied a priori.
- Seat-as-subject experiment: The benchmark measures method cost on a working seat, using referee-decidable tasks and an authored population rather than relying on agent accounts or drawn tasks.The seat comprises a coding agent, harness, and workspace; the benchmark reports per-cell prices and separately reports a later correctness pass.
- Design: The four arms cross method instruction with specification source: plain or specification-and-verification, each with an agent-written or a priori specification.The a priori pair isolates verification cost from specification-writing cost; a placebo controls prompt length but is outside the four arms.
- Substrate: All arms use Rust under the same pinned Verus toolchain, so the intended comparison changes method instruction rather than programming language.A Lean arm would change language and method together and is therefore not part of this paper.
- Task forms: The measured task form is greenfield, while brownfield repair and specification-change forms are authored or planned rather than run.The run-status vocabulary distinguishes landed runs, amendment-authorized registrations, authored designs, and plans.
- Population and referee: The population contains five authored, frozen Rust systems components, and the withheld suites were measured against authored mutants before any cell ran.The passages identify the five-component authored population and report 44 of 44 mutants killed, while cautioning that this is a ceiling rather than a strength measure.
- Specification amendment: The specification amendment derived admissible sections uniformly from withheld reference solutions, with reproduction and interface-closure rules fixed before editing.The same extraction tool was required to reproduce the existing LZW section byte-identically, and named proof functions contributed contracts with bodies elided.
3 The protocol, as exercised on v3
The exercised protocol scores work with a referee outside the agent’s workspace, measured isolation, pre-registered readings, and explicit halt handling. Its instrument record also documents sandbox and grading failures that constrain interpretation.
- Referee and scoring: Each episode is scored by a checker the agent cannot see or reach, with solved status fixed by the referee rather than the agent.The Rust population uses withheld suites run by the harness outside the workspace, although the reported cost cells were scored without invoking the referee.
- Referee variants: Earlier referee implementations include Lean kernel replay, Verus acceptance with text and AST checks, and a hidden-suite SWE-bench scorer later abandoned after stage 0.These referees appear as related protocol substrates rather than interchangeable guarantees.
- Measured fence: Isolation is layered and empirically probed, but the harness file-reading tool remained outside the subprocess sandbox in every scored episode.The record retains subprocess sandboxing, an empty network allowlist, shell hooks, ground-truth checks, and auditing, while noting that tool permissions were not path-fenced.
- Registration: The protocol’s freeze commit authorizes the population, byte-pinned arms, checker, constants, predictions, adverse outcomes, and stop rules before model calls.Later changes require dated amendments with their own predictions, and corrections are appended rather than silently edited.
- Reading rules: The registered reading uses pre-specified count or null-derived thresholds, while predictions are scored in their registered direction and budget caps are recorded as halts rather than failures.A token stop at four times the governing regime’s p90 leaves the episode unresolved for the rate; the grader writes HALT for token or wall stops.
- Grader behavior: The Verus treatment’s helper-lemma behavior exposed grader gates that rejected some prompt-invited helper placements and enforced additional unstated use rules.The repair changed the prompt to make it a consumer of the grader’s restrictions.
4 The v3 reading: a registered cost premium on all five problems, and a post-hoc correctness pass that did not separate the arms
The registered cost reading found that the dieted specify-and-verify treatment cost more than the plain arm on all five problems, while the post-hoc correctness pass did not separate the arms. The evidence supports a sign result, not a population cost multiplier, and budget stops must be treated separately from correctness failures.
- 4 The v3 reading: The declared set was scored under continuity and run-only readings, and both preserved the five-of-five sign despite differing magnitudes.Reading B removes three borrowed smoke cells; the sign remains unchanged, while several per-problem premiums move.
- 4 The v3 reading: The largest observed premium was 2.8879×, but three of five premiums fell below the 2.0072× resolvable floor.The reported premiums are observations at n = 3, not population magnitudes or interval estimates.
- 4 The v3 reading: Five of five treatment premiums exceeded parity under both readings, yielding one-sided p = 0.0312.The sign test was registered before execution; the two readings agree on the headline sign.
- 4.1 A post-hoc correctness pass: The post-hoc correctness pass did not separate the arms, and its pass rates are biased upward because every budget-capped cell was a treatment cell.Budget stops are not correctness failures; all three capped treatment cells passed completely when their suites were run.
5 The instrument findings, as results
The instrument findings show that benchmark infrastructure can distort, censor, or misstate results unless gates, controls, and stop rules are treated as measurement components. Several failures changed the protocol or exposed limits on what the recorded data could support.
- A censored cap returns the cap, so budgets must use uncensored data or raise the cap until censoring is negligible.Recording the intermediate state does not by itself recover an uncensored estimate under a verifier.
- The benchmark found that a blind agent can pass while spending 11–16 times more than a sighted episode, because it cannot reach its referee.The episode driver was changed to refuse runs where the fence and workspace intersect.
- Fence validation must probe every bound tool, because sandboxing subprocesses did not fence the agent’s own file-reading tool.A useful audit must distinguish denied calls, absent files, and served reads; otherwise it can report false escapes.
- Scoreboards require companion statements about population structure because arithmetic alone hides missing correctness verdicts and cross-root cell reuse.The paper also identifies condition-key errors that can pool arms without producing obvious numerical errors.
- A control arm that fails as predicted is not evidence for the treatment, and the placebo’s unresolved results were explicitly barred from supporting it.The placebo cost $193.42 and remained unresolved on all five problems.
- A budget cap can create arm-correlated sampling bias by removing the treatment’s slowest cells before later correctness analyses.The treatment reached the cap while controls did not, leaving fewer and easier treatment cells in the surviving sample.
6 The reads that shaped the design
The earlier reads closed several seemingly available evaluation routes and motivated SaltBench’s referee-gated, authored, cost-focused design. They found contamination, shared failures, oracle defects, and censoring effects that made capability comparisons unsafe or incomplete.
- SWE-bench was abandoned after contamination was found, because resolved tasks included upstream-fix text and the substrate was saturated at that tier.The treatment arms were not run on this substrate.
- On the registered U15, both S2-Lean arms proved 8 of 15 tasks, with identical paired outcomes despite different token costs on shared successes and failures.The treatment used 15.79M versus 20.76M tokens on jointly proved problems, but 35.62M versus 29.92M on jointly failed problems; the paper reports this as a paired observation, not an effect.
- At Opus, both content arms moved to 10 of 15 with no discordant paired outcomes, leaving the treatment contrast indistinguishable.A differential re-check found a complete kernel-checked proof with and without a refused line, so the treatment’s 11-of-15 reading is diagnostic rather than a resolved contrast.
- Blind triage classified 30 of 31 failed stage-B cells, with 17 human-loose, 5 agent-wrong, and 8 proof-hard cases.Eight failing problems each carried one label, indicating that the arms failed for the same problem-specific reasons; many false obligations arose from guarded versus total specifications.
- The reference specification for Problem 18 contradicts the benchmark’s own test, and the checker can certify all 15 tasks when the theorem is replaced by True or discharged by an axiom.These findings expose a benchmark-oracle failure rather than a treatment effect.
- The hard-band read passed 9 of 10 scorable tasks, but cap shoulder effects make that count a lower bound on the ceiling.Two episodes reached the 40-call cap, and another episode that had no discharged obligations at 40 calls contained a complete proof at call 79 after the cap was raised.
7 The treatment question, open
The treatment question remains open: the systems run measures a cost difference, not an effect on referee acceptance. The paper therefore separates the reported price reading from registered follow-up work needed for a capability comparison.
- The treatment cost more on all five systems problems, but the record does not show that it changes what the referee accepts.The post-hoc correctness pass over surviving cells did not separate the arms, and the paper explicitly distinguishes price from capability.
- A 120-call episode passed cleanly after the identical 40-call episode reported no discharged obligations, showing that the lower cap was binding on that task.The planned 40-call hard-band read was cancelled because it would return a censored result.
- The repaired CLEVER variant changes the benchmark from specification isomorphism to implication-with-witness and is registered as a variant rather than a correction.It excludes Problem 18 and reruns the seven problems both arms failed.
- A capability comparison on the systems population requires separate registered work because four gaps prevented the current cost reading from being comparable across the population.The amendment reached k = 4 rather than the intended k = 5, and the full method rendering was refused by the current cost cap.
- The S2-Lean failure surface is itself a benchmark finding: four remaining stage-C oracles are permissive where their tests never look, and the taxonomy lacks a contradictory-reference-specification class.The reproduction scripts are released for benchmark authors, while the disclosure is treated as a separate act.
8 Reproducibility
SaltBench is designed for reproducibility through pinned inputs, tools, prompts, checkers, drivers, seeds, and images, with the authored systems population frozen by dated cell identifiers. The release separates re-derived task sources from run records and documents redistribution and licensing.
- Every evaluated component is pinned through hashes covering sources, toolchains, prompts, arms, checkers, drivers, limits, seeds, and rebuilt views.The episode script refuses to run when a view or checker hash does not match its recorded pin.
- The authored systems population is frozen in a dated export, with scored cells declared by identifier and prices read from each cell’s meter file.The client is selected by an absolute versioned path rather than shell-path resolution.
- Task populations are rebuilt from pinned sources, while redistributed materials are limited to the items listed in PROVENANCE.md.Run records and S2 episode archives are maintained as a separate released data asset.
- The code is released under Apache-2.0 and the data and documents under CC BY 4.0.The paper also records the agent and the versions of the governing provider documents used for publication.
A S2-Lean U15, per problem
The S2-Lean U15 records stage-B outcomes for problems across two systems, with pass/fail patterns and call-cap diagnostics shown per problem. The accompanying key identifies the systems, stage, cap, and one screen-refused cell with a later complete proof.
- A S2-Lean U15, per problem: The per-problem matrix reports pass/fail outcomes for S and O across the listed U15 problems.The supplied table lists six outcomes per problem, while the key identifies S as claude-sonnet-5 and O as claude-opus-5.
- A S2-Lean U15, per problem: S denotes claude-sonnet-5, O denotes claude-opus-5, and all entries are stage-B results under a 100-call cap.
- A S2-Lean U15, per problem: One cell marked † was refused by the pragma screen, but a registered re-check found a complete proof.The key identifies this as diagnostic 11 of 15.
B The stage-B failure triage
The stage-B failure triage assigns labels from the specification texts and proof alone, separating human-loose specifications, agent-wrong specifications, and proof-hard obligations. Across 30 triageable cells, human-loose cases are most common.
- B The stage-B failure triage: The triage labels were assigned blindly from the two specification texts and the proof, without tier, arm, class, or termination information.This procedure was used for every failed stage-B cell in the record.
- B The stage-B failure triage: The labels were treated as properties of problems rather than arms, because the failing problems carried the same single label across arms.
- B The stage-B failure triage: 17 of 30 triageable cells were human-loose, compared with 5 agent-wrong and 8 proof-hard cells.One screen-refused cell was excluded from these totals.
C The S2-Rust hard band
The S2-Rust hard band contains upper-tercile tasks selected by reference-proof wall time. In a 13-task draw, 9 episodes passed, but the capped count is explicitly a lower bound because one failure was cap-censored.
- C The S2-Rust hard band: The band comprises the upper tercile of 180 live tasks, with 60 tasks ranked at least 120 by reference-proof wall time.It contains 42 Anvil-Advanced and 18 NRKernel tasks.
- C The S2-Rust hard band: 9 of 10 episodes passed under the sequential stop, while 1 reached VERIFY_FAIL at the cap.The failed episode ended at 40 of 40 calls one obligation short, so the observed pass count is a lower bound for the band at this cap.
- C The S2-Rust hard band: The 9 passing episodes reached a first clean referee run after a median of 2 referee calls, with p90 equal to 9.Uncensored passing call counts ranged from 23 to 39 against the 40-call cap, and one pass landed exactly at 40.
D The systems matrix, per cell
The systems matrix reports per-cell metered subscription prices and premiums under two declared readings of the set. Reading B removes three borrowed smoke cells, while four unmetered or malformed cost records are excluded from every reading.
- D The systems matrix, per cell: The scoreboard reports premiums, while the underlying per-cell US-dollar prices allow readers to recover the medians.Each price is read from that cell’s harvested METER.txt.
- D The systems matrix, per cell: Reading A includes every printed row, whereas Reading B removes three underlined borrowed smoke cells.Three conditions therefore use n = 4 under Reading A and n = 3 under Reading B; the remaining conditions use n = 3 under both.
- D The systems matrix, per cell: At n = 4, the median is the mean of the middle pair rather than any individual cell price.
- D The systems matrix, per cell: Four matrix-root cells were excluded from every reading because their cost lines did not begin with a bare price.The scorer refused them rather than defaulting their prices to zero.