SpecGuard：在Agent执行前证明任务存在奖励作弊漏洞

摘要

随着自主编码Agent的部署越来越多，任务中意外或敌对注入的错误指定导致Agent危险行为的风险至关重要。先前的研究表明，承担此类任务的Agent很少会标记冲突，而是作弊、编辑测试或硬编码预期输出，而作弊所采取的操作可能会造成真正的损害，例如删除安全防御以使测试通过损坏。目前尚不清楚在Agent采取行动之前是否可以通过独立可验证的证据来确定此类冲突。我们推出 SpecGuard，它可以检测并正式证明任务意图和测试之间的这些冲突。仅给出任务描述和代码库，SpecGuard 将预期行为自动形式化为 Lean 4 规范。这些测试是独立形式化的，精益内核会检查是否有任何实现可以满足这两种形式化，并在无法满足时生成机器检查的证书。在冲突的 SWE 基准任务中，SpecGuard 检测到高达 72.8% 的冲突，并正式认证高达 51.1%，冲突漏失率比基于模型的判断低近五倍。 SpecGuard 提供执行前安全检查，在观察到任何Agent行为之前，通过任务级冲突的正式认证来识别奖励黑客机会。我们的代码可在 https://github.com/prmbiy/specguard。获取

SpecGuard：在Agent执行前证明任务存在奖励作弊漏洞：论文原图 — 图 3：SpecGuard 概述。 SpecAgent 根据描述和代码库生成可执行的正式规范，而无需访问测试。 TestAgent 正式化测试要求。验证者构造一个语义连接器并尝试生成经过内核检查的分歧证书。