AI 中文总结
研究生产型大语言模型智能体框架控制原语执行差距，用无模型差分探针发现漏洞及差距，提出SOUNDGATE修复，能强制执行多种属性，端到端阻止违规，释放合法效果。
AI 中文摘要
生产型大语言模型智能体框架公开了控制原语，如人工参与审批门、运行取消和执行超时，其名称和文档暗示了屏障语义。但研究表明，在测试的六个广泛使用的开源框架中，这种隐含契约都不成立。无模型差分探针发现了常见的漏洞，如审批门暂停自身分支时，兄弟分支的效果仍在执行。还发现了其他三个差距。为修复这些差距，提出了SOUNDGATE，它能强制执行多种属性，在六个框架上能端到端阻止所有检测到的违规行为，同时释放合法效果。
英文摘要
Production LLM-agent frameworks ship control primitives -- human-in-the-loop approval gates, run cancellation, and execution timeouts -- whose names and documentation imply barrier semantics: while a run is paused, cancelled, or timed out, no gated side effect executes. This contract holds on none of six widely used open-source frameworks. Model-free differential probes isolate a recurring sibling leak -- an approval gate suspends its own branch while a sibling's effect executes during the pause, defeating rejection -- in every framework shipping a pre-execution gate (five of six, four execution models, two language runtimes), and confirm replay double-execution, cancellation orphans, and timeout zombies. The hazard is reachable: frontier models emit the leak-triggering plan shape at rates up to 14%, and live models driving unmodified frameworks leak 215 of 1,200 runs (P(leak | emitted)=1.00); on naturalistic tau-bench episodes models serialize writes -- the everyday gap is latent -- while injection induces it deterministically and a 13-incident public corpus corroborates the replay and cancellation failures. We repair the gaps with SOUNDGATE, an environment-external Rust gate through which every side effect must be admitted, enforcing hold-until-decided, reject-cancels, dedup-on-replay, and fence-on-cancel under a stated complete-mediation contract, discharged for network egress by two kernel-enforced routes. The admission core is mechanically verified (Verus; TLA+/TLC to 7.5e7 states; TLAPS; Loom on the deployed Rust) and bridged to code by differential conformance over 1.2e7 operations with zero divergences. Under that contract SOUNDGATE blocks every measured violation on all six frameworks while releasing legitimate effects: gated tau-bench episodes complete with zero refusals at ~1 ms per write, and durable admission sustains ~12k admissions per second.
Comments32 pages, 3 figures, 11 tables. Code: pip install soundgate (PyPI)
