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

• URL: http://arxiv.org/abs/2609.11076v1
• Date: Thu, 10 Sep 2026 04:32:43 GMT
• Title: SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work
• Abstract summary: SaltBench is a benchmark protocol for one question: How does a machine referee change the way a coding agent works?<n>In this study, the subject of the benchmark is a seat'', meaning an agent session in its standard harness.<n>We tested five systems components, all authored in Rust under a pinned Verus toolchain, with a withheld test suite as the referee for each.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• BenchShield: Formal Model-Backed Instrumentation for Reward Integrity in LLM-Agent Evaluation Infrastructure [47.61632934139226]
  LM-agent benchmarks increasingly function as interactive evaluation infrastructure.<n>This interactivity makes evaluations vulnerable to reward hacking.<n>This paper presents BenchShield, a model-backed instrumentation layer for reward integrity.
  arXiv  Detail & Related papers  (2026-09-10T03:10:58Z)
• More Rejective, Not More Discriminative: The Unit of Verification in Pre-Execution LLM Oversight [3.8564927363194754]
  Pre-execution oversight is core to trusted monitoring in AI control.<n>Existing designs take the unit as given; its effect on fallible monitors is unmeasured.<n>Our framework is the first controlled, pre-registered instrument for this choice and never reads catch alone.
  arXiv  Detail & Related papers  (2026-08-25T00:59:55Z)
• CatchBench: When Can an Agent Failure Be Caught? [6.230697997280125]
  CatchBench puts one auditor's question to three information states.<n>Prior benchmarks fix one of these states or vary the telemetry.<n>Each state admits different questions, so seven task contracts carry their own labels and metrics.
  arXiv  Detail & Related papers  (2026-08-24T05:09:41Z)
• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• Coding Agents as Test-Suite Auditors: Finding What Official Suites Miss While Approaching What They Catch [47.836680625916266]
  An off-the-shelf coding agent, serving as a test-suite auditor, both builds adversarial test suites to expose what official suites miss.<n>A certification chain determines whether each agent-flagged submission is genuinely buggy without relying on the official judge.<n>On post-cutoff Codeforces problems with no available official suites, the same test-building method leads all five reproduced baselines at every tested input budget.
  arXiv  Detail & Related papers  (2026-08-03T05:24:03Z)
• The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK [0.0]
  In a verifier-driven loop, AI agents wrote and verified bare-metal security software in Ada/SPARK spanning classical and post-quantum cryptography, TLS 1.3, IKEv2, X.509, and a Matrix client.<n>GNATprove discharged 49,280 proof obligations, established functional correctness for selected primitives, and proved the absence of run-time errors for the rest.<n>We report where each layer caught faults and draw the central lesson: what an agent can be trusted to establish is bounded by the strength of its feedback.
  arXiv  Detail & Related papers  (2026-07-15T20:09:05Z)
• Auto: The AGI Compiler [0.0]
  Auto is a compiler that records live agent behavior, measures which parts are secretly deterministic, extracts them into verified programs or distilled specialists, and emits cognition binaries.<n>We use "AGI compiler" in one narrow, testable sense: a system that autonomously converts novel experience into permanent, verified, near-free skill while measuring what it does not know.
  arXiv  Detail & Related papers  (2026-07-05T23:09:24Z)
• MoCA-Agent: A Market-of-Claims Code Agent for Financial and Numerical Reasoning [47.751319722749116]
  textscMOCA-Agent is a market-of-claims code agent that replaces free-form multi-agent debate with claim-level verification.<n>The system decomposes each question into typed atomic claims, asks specialist trader agents to buy or sell those claims, clears their orders into confidence-weighted accept/reject decisions.<n>A code-aware verifier then checks the program for execution, structural consistency, and common financial reasoning errors.
  arXiv  Detail & Related papers  (2026-06-10T00:45:39Z)
• Do Androids Dream of Breaking the Game? Systematically Auditing AI Agent Benchmarks with BenchJack [51.54835866517547]
  BenchJack is a system that drives coding agents to audit benchmarks and identify possible reward-hacking exploits.<n>We apply BenchJack to 10 popular agent benchmarks spanning software engineering, web navigation, desktop computing, and terminal operations.<n> BenchJack synthesizes reward-hacking exploits that achieve near-perfect scores on most of the benchmarks without solving a single task.
  arXiv  Detail & Related papers  (2026-05-12T19:22:45Z)
• Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon [0.0]
  ML kernels ship with an implicit contract about what it computes.<n>Recent empirical work has measured the gap across silicon platforms, but none of it specifies the contract being violated.<n>We present a specification language for kernel contracts.
  arXiv  Detail & Related papers  (2026-04-23T19:46:52Z)
• Malicious Agent Detection for Robust Multi-Agent Collaborative Perception [52.261231738242266]
  Multi-agent collaborative (MAC) perception is more vulnerable to adversarial attacks than single-agent perception. We propose Malicious Agent Detection (MADE), a reactive defense specific to MAC perception. We conduct comprehensive evaluations on a benchmark 3D dataset V2X-sim and a real-road dataset DAIR-V2X.
  arXiv  Detail & Related papers  (2023-10-18T11:36:42Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.