用统一框架组织语言模型智能体的轨迹证据与保障账本
Organising Trajectory Evidence for Language-Model Agent Assurance: Fragments, Methods, and the Residual
评估智能体时各种检查器各管一段、说不清组合效果，这篇论文用一套逻辑和保障账本把证据拼起来，还给了 τ²-bench 上 456 条轨迹的实测拆解。
这篇论文把规则检查器、支持检查器、前缀监视器、执行门等语言模型智能体评估方法放进同一个逻辑框架：需求写成两层逻辑公式，外层是有限轨迹时序逻辑，内层是描述记录上下文支持结构的逻辑。每种检查方法判定该语言的一个片段，返回精确、基于测试套件、风险界限或描述性四种类型之一。在 τ²-bench 电信域的 456 条轨迹上，基准 oracle 标记 231 条，叠加规则检查器、支持检查器和前缀监视器后联合标记数升至 391、401、407，剩余 49 条未标记轨迹与未满足义务构成残差，由保障账本统一登记。
Organising Trajectory Evidence for Language-Model Agent Assurance: Fragments, Methods, and the Residual
Methods for assessing language-model agents include rule checkers over logs, analyses of skill coverage and composition, support checkers, prefix monitors, execution gates, and rare-event estimators. Each observes a different part of a run and makes a claim of a different strength, and no common account says how these claims combine or what they leave unchecked. We give one, built from a logic, information fragments, and an assurance ledger. Requirements are formulas of a two-tier logic: an outer finite-trace temporal logic over recorded events, and an inner logic of standing over the argument structure that the agent's recorded context supports at a decision. A rule violation and an action taken on withdrawn support are thus formulas of one language. The information available to an assessor, to the agent, and to an execution gate defines fragments of that language; each checking method decides one fragment and returns a typed claim: exact, on a named test suite, a risk bound, or descriptive. The ledger merges the evidence and classifies every obligation as established, addressed but not established, or unaddressed. On 456 released $τ^2$-bench telecom trajectories, the benchmark oracle flags 231 runs; adding a rule checker, a support stand-in, and a prefix-monitor baseline raises the union to 391, 401, and 407, each contributing flags the others miss, and a gate makes one prohibition exact on a gated deployment. The 49 unflagged runs and the unmet or unaddressed obligations form the residual. Discovery makes unknown requirements explicit, and new or stronger checkers then reduce it.
