AI 中文总结
SaltBench提出一种裁判门控协议，通过隔离代理并测量方法效应，发现指定并验证代码的方法在五个Rust组件上成本更高，溢价有界且随规模增大。
AI 中文摘要
SaltBench是一个基准测试协议，旨在回答一个问题：机器裁判如何改变编码代理的工作方式？机器裁判——如证明内核、程序验证器或保留的测试套件——决定代理工作的价值，而代理无法与之争辩。在此，我们报告了一种协议，该协议使裁判的效应可测量，且其答案事后无法被叙述：每个结果都在代理自身工具链之外决定；代理与网络、参考解决方案及测试装置本身隔离，且隔离通过尝试在每次评分运行前突破它的探针进行测试，因此隔离是被观察到的而非假设的；每次运行都通过带有预测注册的日期冻结授权；预算停止是暂停，而非失败。在本研究中，基准测试的对象是一个“席位”，即标准测试装置中的代理会话。我们测试了五个系统组件，全部在固定的Verus工具链下用Rust编写，并为每个组件使用保留的测试套件作为裁判。测试了四个臂：一个普通代理；一个被指示创建规范并对照规范验证代码的代理，采用方法的简化呈现，如注册所示；以及两个预先提供规范的臂，在日期修正案下扩展到$k=4$，其中注册的符号检验未得出裁决（4中3，$p = 0.3125$，每个溢价均低于可解析下限）。我们发现，被指示进行规范和验证的臂在所有五个组件上成本更高，且差距具有实际意义：在这五个组件中，无论对声明集合的哪种解读，溢价均未超过$2.8879\times$，而三个最便宜的低于$1.4\times$。该界限是此总体的属性，而非对更大总体的承诺：溢价在最小组件上接近$1$，并随规模增大而上升。我们发布了完整记录。
英文摘要
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.
