SpecGuard 用 Lean 证书在编码 Agent 执行前证明任务冲突
SpecGuard: Proving a Task Is Broken Before the Agent Cheats
AI 导读
SpecGuard 在编码 Agent 运行前检测任务描述与测试之间的冲突，并用 Lean 4 生成机器可检查的冲突证书。方法上，SpecAgent 在不接触测试的情况下从任务描述和代码库生成可执行规范，TestAgent 独立形式化测试要求，Certifier 构建语义连接器并尝试证明不存在同时满足两者的实现。在冲突版 SWE-bench 任务上，SpecGuard 最多检测出 72.8% 的冲突、正式证明 51.1%；GPT-5.6 Sol 的冲突漏报率为 8.1%，而 LLM 评委基线为 39.8%。同时提供原始与损坏两版测试时，检测率提升 17 至 25 个百分点，Sol 的证明率升至 67.0%。作者对 60 份形式化的人工审计显示 52 份忠实，失败分析表明主要瓶颈是独立生成表示之间的语义对齐，而非 Lean 证明检查本身。
推荐理由
论文把任务描述与测试分别形式化，用 Lean 证书在 Agent 执行前证明二者不可同时满足，为奖励作弊提供了可独立复核的前置检查思路。