有界循环：智能体执行框架的预运行花费上限、终止性证明与完成性验证
Bounded Loops: Pre-Run Spend Bounds, Proved Termination, and Verified Completion for Agent Harnesses
浏览论文内容
中文总结 AI 辅助
针对智能体执行框架缺乏强制终止与预算保证的问题，提出有界循环图模型，通过独立门控与修复机制证明终止性、防偏离与防超支，并构建检测工具在69个循环中发现47个空洞门控，贡献在于检测装置本身。
中文摘要 AI 辅助
在主流智能体框架中，当智能体自身的输出表明其已完成时，一个步骤即告结束。持久化执行平台对重试次数和时间设置上限，但其检查器通常与工作代码位于同一代码库中：这是一种依赖部署方自觉遵守的纪律，而非执行框架强制执行的属性。\n我们阐明了智能体执行框架必须保证的性质，对其加以证明，并构建了用于度量执行框架是否兑现该保证的检测工具。有界循环由三部分组成：一个工作器、一个工作器无法写入的独立门控，以及一个声明的预算；有界循环图通过修复关系将这些组件组合起来，使得下游失败可以重新运行已完成的上一节点。由此产生三项保证。其一，它必然结束：在全局而非逐节点的修复预算下，终止性在修复机制下成立，且最坏情况下的尝试总数具有闭式表达式。其二，它不会偏离：在仅追加的哈希链式账本中，没有节点能在未获得门控裁决的情况下达到完成状态，这一点可从控制流得到证明，因为修复机制不留下可沿之归纳的拓扑顺序。其三，它不会超支：预算上限在单次尝试内部强制执行，而非在尝试之间强制执行。\n门控通过两层保留的变异体语料库进行度量。我们刻画了两类可能使看似合理的检查放行任意内容的门控类别：空洞性——因被检查对象缺失而得到满足，以及自我证明——由被检查主体自身提供用于检查的值。在包含69个循环的目录中，该工具在已发布并经审查的代码中发现了47个空洞门控。针对修复后的门控，该工具在209个破坏性变异体上报告零误接受（α≤1.8%，Wilson 95%置信区间）；该数字反映的是饱和而非质量：冻结门控并应用一组全新的操作符族，在已耗尽的语料库报告零误接受的场景下，恢复出23.3%的误接受率。误接受率属于特定门控；本研究的贡献在于这套检测装置本身，而非我们给出的具体数字。引擎、目录和语料库均以Apache-2.0许可证发布。
英文摘要
In mainstream agent frameworks, a step ends when the agent's own output says it has finished. Durable-execution platforms bound retries and time, but their checker conventionally lives in the same codebase as the work: a discipline the deployment is trusted to keep, not a property the harness enforces. We state what an agent harness must guarantee, prove it, and build the instrument that measures whether a harness delivers it. A bounded loop is a worker, an independent gate the worker cannot write to, and a declared budget; a bounded-loop graph composes them with a repair relation that lets a downstream failure re-run a finished upstream node. Three guarantees follow. It finishes: termination holds under repair, with the worst-case attempt total in closed form, if the repair budget is global not per node. It does not drift: no node reaches DONE without a gate verdict in an append-only hash-chained ledger, proved from control flow, since repair leaves no topological order to induct along. It does not overspend: the ceiling is enforced inside an attempt, not between attempts. Gates are measured against a two-tier held-out mutant corpus. We characterise two classes that let a sound-looking check pass anything: vacuity, satisfied by the absence of the thing checked, and self-attestation, where the subject supplies the value the check is applied to. On a 69-loop catalogue the instrument found 47 vacuous gates in shipped, reviewed code. Against the repaired gates it reports no false accepts over 209 destroying mutants ($α\le 1.8\%$, Wilson 95%); that figure is saturation, not quality: freezing the gates and applying a fresh operator family recovers a 23.3% false-accept rate where the exhausted corpus reported none. A rate belongs to a specific gate; the apparatus, not our number, is the contribution. Engine, catalogue and corpus are Apache-2.0.
发表机构
- Qualixar（Qualixar公司）
机构由 AI 辅助整理，请以论文原文为准。
