論文の概要: SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work

• arxiv url: http://arxiv.org/abs/2609.11076v1
• Date: Thu, 10 Sep 2026 04:32:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-11 23:53:35.211881
• Title: SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work
• Title（参考訳）: SaltBench: 機械学習ソフトウェア作業におけるメソッド効果測定のための参照ゲートプロトコル
• Abstract要約: SaltBenchは1つの質問に対するベンチマークプロトコルである。 マシンレフェリーは、コーディングエージェントの動作方法をどのように変えますか? 本研究では,ベンチマークの対象がシート'であり,標準ハーネスにおけるエージェントセッションを意味する。 私たちは5つのシステムコンポーネントをテストしました。いずれもRustで記述されたVerusツールチェーンの下で,それぞれがレフェリーとして使用可能なテストスイートを使用しています。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: SaltBenchは1つの質問に対するベンチマークプロトコルである。 マシンレフェリーは、コーディングエージェントの動作方法をどのように変えますか? マシンレフェリー -- 証明カーネル、プログラム検証器、あるいは非保持テストスイート -- は、エージェントの作業の価値を決定する。 エージェントは、ネットワーク、参照ソリューション、ハーネス自体から切り離され、壁は、スコアランの前にそれを破ろうとするプローブによってテストされるので、推測されるよりもむしろ分離が観察される。すべての実行は、日付付きフリーズによって、その予測が登録された状態で承認され、予算が停止されることは決してありません。 本研究では,ベンチマークの主題が ‘seat'' であり,標準ハーネスにおけるエージェントセッションを意味する。 私たちは5つのシステムコンポーネントをテストしました。いずれもRustで記述されたVerusツールチェーンの下で,それぞれがレフェリーとして使用可能なテストスイートを使用しています。 4つの腕がテストされる: プレーンエージェント、そして、登録されたメソッドのレンダリングを減らして、仕様の作成とそれに対するコード検証を指示されるエージェント、および仕様が提供された2つの腕は、日付付き修正により$k=4$に拡張され、登録されたサインテストは、解決可能なフロアの下のすべてのプレミアムである4,$p = 0.3125$の判定値に達しない。 これらの5つのコンポーネントのうち、プレミアムが2.8879\times$を超えないこと、そして最も安い3つは1.4\times$を下回ること。 プレミアムは最小のコンポーネントで1ドル近い価格で動き、サイズが大きくなる。 私たちはその完全な記録を公表する。

関連論文リスト

• BenchShield: Formal Model-Backed Instrumentation for Reward Integrity in LLM-Agent Evaluation Infrastructure [47.61632934139226]
  LMエージェントベンチマークは、ますますインタラクティブな評価基盤として機能する。 この対話性は、評価を報酬ハッキングに脆弱にする。 本稿では、報酬整合性のためのモデル支援インスツルメンテーション層であるBenchShieldについて述べる。
  論文  参考訳（メタデータ） (2026-09-10T03:10:58Z)
• More Rejective, Not More Discriminative: The Unit of Verification in Pre-Execution LLM Oversight [3.8564927363194754]
  事前実行監視は、AI制御における信頼できる監視のコアとなる。 既存の設計ではユニットが与えられており、フェールブルモニターに対する効果は計り知れない。 私たちのフレームワークは、この選択のために制御され、事前登録された最初の楽器であり、キャッチのみを読み取ることはありません。
  論文  参考訳（メタデータ） (2026-08-25T00:59:55Z)
• CatchBench: When Can an Agent Failure Be Caught? [6.230697997280125]
  CatchBenchは、監査人の質問を3つの情報状態に分類する。 以前のベンチマークでは、これらの状態の1つを修正したり、テレメトリを変更したりする。 各州は異なる質問を認めており、7つのタスク契約は独自のラベルとメトリクスを持っている。
  論文  参考訳（メタデータ） (2026-08-24T05:09:41Z)
• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。 Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。 ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
  論文  参考訳（メタデータ） (2026-08-13T17:41:27Z)
• Coding Agents as Test-Suite Auditors: Finding What Official Suites Miss While Approaching What They Catch [47.836680625916266]
  テストスイート監査官として機能する市販のコーディングエージェントは、どちらも、公式スイートが見逃すものを公開するために、敵対的なテストスイートを構築します。 認証チェーンは、各エージェントフラッグされた申請が、公式の裁判官に頼らずに、真にバグだらけであるか否かを判定する。 Codeforceは、利用可能なオフィシャルスイートを持たない問題に対して、同じテストビルディングメソッドを使用して、テストされた入力予算毎に5つの再生ベースラインを導出する。
  論文  参考訳（メタデータ） (2026-08-03T05:24:03Z)
• The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK [0.0]
  検証者主導のループにおいて、AIエージェントは古典的および後量子暗号、TLS 1.3、IKEv2、X.509、マトリックスクライアントにまたがるAda/SPARKのベアメタルセキュリティソフトウェアを書いて検証した。 GNATproveは49,280の証明義務を解除し、選択されたプリミティブに対して機能的正当性を確立し、残りのプリミティブに対して実行時のエラーがないことを証明した。 それぞれのレイヤが障害をキャッチし,中心的な教訓を引き出す方法を報告します。エージェントが確立するために信頼できるものは,そのフィードバックの強さに縛られているのです。
  論文  参考訳（メタデータ） (2026-07-15T20:09:05Z)
• Auto: The AGI Compiler [0.0]
  Autoは、ライブエージェントの振る舞いを記録し、どの部分が秘密に決定論的かを測定し、それを検証プログラムや蒸留専門家に抽出し、認識バイナリを出力するコンパイラである。 我々は,「AGIコンパイラ」を狭義で実証可能な意味で使用し,新規体験を,未知の知識を計測しながら,永続的で検証された,ほぼ自由なスキルに自律的に変換するシステムを開発した。
  論文  参考訳（メタデータ） (2026-07-05T23:09:24Z)
• MoCA-Agent: A Market-of-Claims Code Agent for Financial and Numerical Reasoning [47.751319722749116]
  textscMOCA-Agentは、フリーフォームのマルチエージェントの議論をクレームレベルの検証に置き換える、有望なコードエージェントである。 このシステムは、各質問をタイプされた原子的クレームに分解し、専門家のトレーダーにそれらのクレームの売買を依頼し、信頼度の高い受け入れ/拒絶決定へと命令をクリアする。 コード認識検証器は、実行、構造整合性、一般的な金銭的推論エラーのプログラムをチェックする。
  論文  参考訳（メタデータ） (2026-06-10T00:45:39Z)
• Do Androids Dream of Breaking the Game? Systematically Auditing AI Agent Benchmarks with BenchJack [51.54835866517547]
  BenchJackは、コーディングエージェントがベンチマークを監査し、報酬をハックする可能性のあるエクスプロイトを識別するシステムである。 BenchJackを、ソフトウェアエンジニアリング、Webナビゲーション、デスクトップコンピューティング、端末操作にまたがる10の人気のあるエージェントベンチマークに適用する。 BenchJackは、単一のタスクを解決することなく、ほとんどのベンチマークでほぼ完璧なスコアを達成する報奨ハックのエクスプロイトを合成する。
  論文  参考訳（メタデータ） (2026-05-12T19:22:45Z)
• Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon [0.0]
  MLカーネルは、その計算に関する暗黙の契約で出荷される。 最近の実証研究はシリコンプラットフォーム間のギャップを測定しているが、いずれも契約に違反していることを明記していない。 カーネル契約のための仕様言語を提案する。
  論文  参考訳（メタデータ） (2026-04-23T19:46:52Z)
• Malicious Agent Detection for Robust Multi-Agent Collaborative Perception [52.261231738242266]
  多エージェント協調(MAC)知覚は、単エージェント認識よりも敵攻撃に対して脆弱である。 MAC知覚に特異的な反応防御であるMADE(Malicious Agent Detection)を提案する。 我々は、ベンチマーク3DデータセットV2X-simとリアルタイムデータセットDAIR-V2Xで包括的な評価を行う。
  論文  参考訳（メタデータ） (2023-10-18T11:36:42Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。