自主编码智能体的保证包络：软件变更的最小成本证据
Assurance Envelopes for Autonomous Coding Agents: Minimum-Cost Evidence for Software Change
浏览论文内容
中文总结 AI 辅助
本研究提出任务条件保证包络，通过最小成本证据子集重新确立软件变更所需属性，利用类型化推理图和闭包验证，实验表明结构决定求解难度。
中文摘要 AI 辅助
当编码智能体回到现有软件时，它会继承先前工程工作的证据：测试、类型检查、证明、静态分析和痕迹。重新加载所有证据是浪费的，但丢弃变更所依赖的证据可能会使所需属性得不到支持。给定变更必须保留的属性（即其义务），我们询问可用证据的哪个最小成本子集能重新确立这些属性，并将这样的子集称为任务条件保证包络。证据及其组合规则形成一个类型化推理图；当从所选证据进行前向链接达到义务时，义务即被满足，我们通过该闭包验证每个选择，而不是信任优化器。我们评估中来自软件派生的图来自先前AI编码智能体运行的保留结果；我们冻结这些工件，并询问对于后续任务应恢复哪些累积证据。来自Rust、IronBlocks和Pong结果的小图表明，最小包络取决于任务；当当前证据无法重新确立所需属性时，可能不存在包络；某些属性需要多个证据共同作用；扩展需求会增加证据而非替换证据。一个包含249个实例的预设合成基准描述了计算特性：丢弃“多个证据共同作用”结构的基线必然无法重新推导它们；每个完成的精确交叉检查都与CP-SAT优化器一致；在500证据图中，中位求解时间保持在20毫秒以下，但每个目标具有多种替代推导的图在远小于此规模时超时，因此是结构而非原始规模驱动难度。贡献是将既有优化方法有限地应用于为软件变更选择保证上下文；发现义务和下游智能体收益仍是开放问题。
英文摘要
When a coding agent returns to existing software, it inherits evidence from earlier engineering work: tests, type checks, proofs, static analyses, and traces. Reloading all of it is wasteful, but dropping a piece the change depends on can leave a required property unsupported. Given the properties a change must preserve, its obligations, we ask which least-cost subset of the available evidence re-establishes them, and we call such a subset a task-conditioned assurance envelope. Evidence and the rules that combine it form a typed inference graph; an obligation is met when forward chaining from the selected evidence reaches it, and we validate every selection by that closure rather than by trusting the optimizer. The software-derived graphs in our evaluation come from preserved outcomes of prior AI coding-agent runs; we freeze those artifacts and ask which accumulated evidence should be restored for a later task. Small graphs from Rust, IronBlocks, and Pong outcomes show that the minimum envelope depends on the task, that none may exist when current evidence cannot re-establish a required property, that some properties need several pieces of evidence together, and that expanding the requirements adds evidence rather than replacing it. A prespecified synthetic benchmark of 249 instances characterizes computation: a baseline that discards the 'several pieces together' structure necessarily fails to re-derive them; every completed exact cross-check agreed with the CP-SAT optimizer; and median solve time stayed below 20 ms at 500-evidence graphs, except that graphs with many alternative derivations per target timed out at far smaller sizes, so structure, not raw size, drives difficulty. The contribution is a bounded application of established optimization to selecting assurance context for a software change; discovering the obligations and downstream agent benefit remain open.
发表机构
- SmartInfer AI（SmartInfer人工智能公司）
机构由 AI 辅助整理，请以论文原文为准。
