从验证失败到编码Agent的可重用指南

编码Agent需要确定程序满足规范并且该规范捕获所请求的行为。我们研究验证失败的专家诊断如何成为这项工作的可重用指南。我们的方法将 K 框架中的可执行语言定义与用于构建规范、修复证明和审核其充分性的过程套件相结合。 HumanEval（164 个 Python 编程任务的基准）上的人工引导开发活动在语义和套件上实现了 164/164 的成功率（通过两次有针对性的修复后最终 AI 审核通过判定来衡量）。为了检查审计是否检测到成功证明未解决的问题，我们构建了 12 对经过作者审查的干净包和有缺陷的包。每个包裹都通过了 K 证明，完成的审核识别出所有缺陷并接受所有干净的包裹。然后，我们使用 KleverBench 测试 31 个更改了运算符含义的程序的规范和证明结构。与完整的接受规则和同样长的通用建议进行比较，会在两种模型和预算设置中产生混合结果，从而推动在资源限制内选择有用指导的进一步工作。经过人工审查的乐观证明为伦敦语义下声明的输入范围内的六项操作建立了预期的暂停恢复，并具有无限的气体。我们向那些提供具有可检查正确性参数的程序的Agent报告进展、困难和教训。