从验证失败到编码智能体的可复用指导
From Verification Failures to Reusable Guidance for Coding Agents
浏览论文内容
中文总结 AI 辅助
本文提出结合K框架与规范构建、证明修复及审计工具包，将验证失败诊断转化为可复用指导，在HumanEval上实现164/164成功率，并通过审计检测缺陷，推动编码智能体生成可验证正确性的程序。
中文摘要 AI 辅助
编码智能体需要确保程序满足规范，且规范准确捕捉了所请求的行为。我们研究专家对验证失败的诊断如何成为这项工作的可复用指导。我们的方法将K框架中的可执行语言定义与一组用于构建规范、修复证明和审计其充分性的程序相结合。在HumanEval（一个包含164个Python编程任务的基准）上进行的人工指导开发活动，在语义和工具包的支持下，通过两次针对性修复后的最终AI审计通过判定，实现了164/164的成功率。为了检验审计是否能检测出成功证明未解决的其他问题，我们构建了12对由作者审阅的干净包和有缺陷包。每个包都通过了其K证明，完成的审计识别出了所有缺陷并接受了所有干净包。随后，我们使用KleverBench测试了31个具有改变运算符含义的程序的规范和证明构建。与完整接受规则和同等长度的通用建议相比，在两种模型和预算设置下结果好坏参半，这激励了在资源限制内选择有用指导的进一步工作。经人工审阅的Optimism证明确立了在伦敦语义下、无界gas的声明输入范围内，六个操作的预期暂停回滚。我们报告了在实现提供可检查正确性论证的程序的智能体方面的进展、困难和经验教训。
英文摘要
Coding agents need to establish that a program satisfies a specification and that the specification captures the requested behavior. We study how expert diagnosis of verification failures can become reusable guidance for this work. Our approach combines executable language definitions in the K framework with a kit of procedures for constructing specifications, repairing proofs, and auditing their adequacy. A human-guided development campaign on HumanEval, a benchmark of 164 Python programming tasks, achieves a 164/164 success rate with the semantics and the kit, measured by final AI audit Pass verdicts after two targeted repairs. To examine whether auditing detects problems that successful proofs leave unresolved, we construct 12 author-reviewed pairs of clean and defective packages. Every package passes its K proofs, and completed audits identify all defects and accept all clean packages. We then use KleverBench to test specification and proof construction for 31 programs with changed operator meanings. Comparisons with complete acceptance rules and equally long generic advice yield mixed results across two model and budget settings, motivating further work on selecting useful guidance within resource limits. Human-reviewed Optimism proofs establish expected pause reverts for six operations within declared input bounds under London semantics with unbounded gas. We report progress, difficulties, and lessons toward agents that deliver programs with checkable correctness arguments.
发表机构
- University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
机构由 AI 辅助整理，请以论文原文为准。
