先说结论：arXiv:2609.16302 这篇，存收藏夹可以，接进 CI 再等等。
不是因为它差。是因为它自己在摘要里就把边界划清楚了——这半个月里，愿意这么干的编码智能体论文，就这么一篇。
十天前挂上去的。15 页，4 图 3 表，外加一个 249 实例的合成基准。Rust、IronBlocks、Pong 三组小图。
我先去照它最容易被截图的那一行。
论文说，500 条证据的图上，求解时间中位数低于 20 毫秒。
500 条证据的图 → 中位求解 < 20ms
每个目标替代推导路径一多 → 远不到 500 条就超时
这两行在原文里是挨着的。转发的人只会截上面那行。
论文的解释是：求解难度主要由推理图的结构决定，跟原始规模关系不大。这话反直觉——多数人第一反应是图大了就慢。但它同时意味着，那个 20 毫秒只在一个特定形状的图上成立。
什么形状？证据之间不太打架，每个目标基本只剩一条推导路径。
我手上那几个跑了三年的老仓库正好相反。同一个「这次改动别把并发搞坏」的性质，测试能顶一次，类型检查能顶一次，上一次的执行轨迹也能顶一次——三条路径互相重叠，谁也压不住谁。论文里那句「大量替代路径下容易超时」，说的就是我这种仓库。
所以这个数字不是假的。是窄的！
然后是更要紧的一处。论文把变更必须保持的性质叫「义务」，再从现有证据里挑一个成本最低的子集，把义务重新撑起来。这个子集叫任务条件化的保证包络。
问题出在入口。
义务从哪来？论文在最后自己承认：发现义务这件事，还没解决。整条链路的第一步现在是个空位！你得先知道这次改动必须保住哪些性质，优化器才有得算。不知道，或者猜错了，包络再小、求解再快，也只是在精确保障一件本来就不该被保障的事。
我不觉得这是作者的锅——他没说自己解决了，他写在结论里了。
但引用它的人会很自然地跳过这一段。
顺带说，论文还承认了另一种情况：现有证据根本重建不了需要的性质时，可能压根不存在对应的包络。不硬凑一个答案出来，这一点比很多工具的通稿体面得多。
（插一句：标题里挂着 Minimum-Cost，可成本是按什么计的？重跑一遍测试的机时，和 agent 把证据读进 context window 的 token，差着好几个数量级。我在 PDF 里没找到明确口径。这条先别信我，等我拿它那个基准跑一遍再说。）
接下来是我这次最想给分的地方。
论文不信任优化器的输出。它从选中的证据出发做前向链式推理，能走到义务节点才算数。所有做完精确交叉检查的实例，结果都和 CP-SAT 一致。
这条比那 20 毫秒值钱多了！
「优化器说这是最优解」和「这些证据真能把性质推出来」，是两码事。评估里只信前者的论文一抓一大把，交出来的是一份优化结果，不是一个能跑的结论。
还有一条基线结果，我觉得比主结论有意思：忽略「某个性质要多条证据合起来才顶得住」这层结构，基线方法干脆推不出那些性质。这话听着像常识，可摆在「我有测试、有类型检查，所以够了」这套流行直觉面前，就是当面一耳光。
顺手记个正面的：需求增加时，证据是追加而不是替换。这符合我在自己项目里看到的——真正难的不是挑证据，是承认昨天那套今天不够用了。
再说局限，论文自己写了的。评估用的图，是之前某次 agent 运行留下的产物，作者把产物冻住，研究后续任务该恢复哪些证据。
冻住的图，回放。
这和在一个正被人和 agent 同时改的仓库里跑，是两件事。这个我要扣分，但只扣一半——固定产物换来了别人能复现。我照着一篇论文的说法去自己仓库上提它那套东西，提完发现人家跑的是自己冻结的快照，这种事不止一次。这次不算，作者把这一点写在正文里了。
249 个实例的合成基准也是同理。作者标了「预先设定」，比拿合成数据冒充真实分布的强；但这个量级够看计算特性，不够说明真实工程里能不能用。
快评评分卡：
读不读——读，15 页里没有一页在表演。接不接——现在不接。入口还空着，接了就是在保障一个你自己都没说清楚的性质。
这波不冤：它坦白告诉你它没解决什么。这波要小心：一定会有人把那个 20 毫秒单摘出来，当成「证据选择问题已经解决」的凭证。
前者是它的数据，后者是你的风险。
想跟的话，等两件事：义务怎么自动发现，以及它在活仓库上的表现。在那之前，把它当一份写得挺老实的边界声明，别当一把能用的刀。