Agent 编码的渐进式失控本地正确性 ≠ 全局架构对齐实例范围类媒体 vs 点类媒体Agent 视频编辑器的架构关系语义的重要性Agent 造成的实际破坏解决方案Lean 形式化验证为什么选择 Lean添加新关系模型强制执行的约束修复后的实现对齐工作流变革Spec Driven DevelopmentProse 规范与 Lean 模型的关系为什么 Agent 让这成为可能AI Agent 编码存在一个缺陷这个过程通常是这样的项目启动时你对应用的预期行为、交互方式、发展方向有清晰的想法你可能花费时间制定系统规格说明书spec与 LLM 反复沟通明确语义、边界、契约和功能集开始工作为 Agent 创建工作包可能拆分成更小的任务初期阶段运转良好Agent 表现优秀你让它们生成测试审查代码自己编写测试和实现细节。渐进式失控随着开发推进问题逐渐浮现遇到遗漏的边缘情况和设计不明确的地方你仍记得系统应该做什么调整计划让 Agent 修复一段时间内这看起来完全合理直到某个时刻你与 Agent 一起回顾工作时产生一种奇怪的感觉与实际实现脱节了。不一定是代码或架构糟糕也不一定是 Agent 做了明显的蠢事而是系统一直在演进——规格、边缘情况、实现、测试和假设都变了。即使每个单独步骤看起来合理你开始问自己我真的还知道系统应该做什么吗本地正确性 ≠ 全局架构对齐用拼图来可视化这个问题┌─────────────────────────────────────────────────────────┐ │ 系统架构可视化 │ ├─────────────────────────────────────────────────────────┤ │ 第1层局部正确性 │ │ 拼图碎片 - 有凸起tab和凹槽blank │ │ 形状完美契合 ✓ │ │ │ │ 第2层全局语义不变性 │ │ 印在拼图碎片上的电路网格图像 │ │ 拼图形状正确但图像被扭曲了 ✗ │ └─────────────────────────────────────────────────────────┘AI 的能力边界AI 非常擅长保持拼图碎片的形状局部正确性AI 在保持整体的非局部全局语义时会变得有创造力结果代码在结构上正确但在语义上变形。范围类媒体 vs 点类媒体以一个 Agent 视频编辑器为例需求是不仅操作时间线还要能推理大型媒体库Agent 需要工具在海量视频、音频、图片、字幕、文档中查找相关内容不仅检索整个文件还要能检索文件内的特定部分这需要亚媒体精度的检索能力。架构系统由四个高层组件构成两个尤为关键组件职责Searcher搜索器使用特征化结果解决语义查询Featurizer特征化器将可能达到 TB 级别的媒体库转换为可处理的形式区分媒体类型系统必须区分两类媒体┌─────────────────────────────────────────────────────────┐ │ range-like media范围类媒体 │ ├─────────────────────────────────────────────────────────┤ │ 存在时间范围从 T0 到 T1 │ │ 示例视频片段、音频片段、ASR语音识别段落 │ │ 特性有明确的开始和结束时间 │ └─────────────────────────────────────────────────────────┘ ┌─────────────────────────────────────────────────────────┐ │ point-like media点类媒体 │ ├─────────────────────────────────────────────────────────┤ │ 只有位置或标识没有持续时间 │ │ 示例图片、静态帧、代表性帧 │ │ 特性可能关联某个时刻但本身不是持续存在的 │ └─────────────────────────────────────────────────────────┘当需要关联这两类媒体时概念完全不同关系类型描述示例Interval Overlap区间重叠两个区间是否有交集视频片段 A 是否与 ASR 段落 B 重叠Point-in-Interval点在区间内点是否落在区间内这个视觉帧时刻是否在这个 ASR 段落内这个区别在英语中很小但在架构上很重要Agent 造成的实际破坏一个测试在 Searcher 组件中失败Agent 修复了这个失败的测试因为测试有时可以用多种方式解释Agent 通过合并架构需要保持的区分来修复Agent 优化的是模块的局部形状——修复了可见的失败破坏的本质Agent 没有保持的架构不变量修复前 Point-like temporal information图片的时间点 ≠ Range-like temporal information视频片段的时间范围 修复后× Point-like temporal information Range-like temporal information 两者被模糊合并为什么这很危险两个问题确实存在语义区分需要保持这些差异会随时间复合可能导致代码混乱和后续扩展困难Diff 看起来并不疯狂外向行为在局部是正确的测试通过了但现在可能混淆图片的点类时间信息和视频的范围类时间信息不是外部可见的问题但下一个需要扩展、改进或修改这个模块的 Agent 可能会看到那段修复的代码突然推断出可以在这里应用那个约束问题的本质: 一个合理的局部更改慢慢削弱系统的语义含义。解决方案Lean 形式化验证为什么选择 LeanProse 规范的问题不强迫你决定概念实际意味着什么无法强制执行下游约束可以变得悄悄过时——你可以更改实现、测试和架构而 Prose 规范仍然坐在那里看起来有意义但不再是系统的准确表示Lean 的优势允许拥有编译后的系统形式化模型可以将 Lean 添加到测试管道的步骤中要求 Agent 在架构更改时触碰它当 Agent 无意中尝试对模块进行局部有效但破坏全局架构的更改时这会成为形式化模型中的编译错误Lean 模型示例在示例中模型已经有了时间重叠关系用于普通的区间对区间情况-- 区间对区间的时间重叠 def TemporalOverlap (a b : MediaItem) : Prop : a.hasInterval ∧ b.hasInterval ∧ intervalsOverlap a.interval b.interval但真正的问题是不同的关系时间点落在时间区间内。添加新关系-- 点在区间内的关系Point-in-Interval -- 这与区间重叠不同是一个独立的关系 def TemporalPointInInterval (p i : MediaItem) : Prop : -- 定义何时这个关系是良构的well-formed -- 左边的项必须有 temporal point右边的项必须是 temporal interval (p.isPointLike ∧ i.isRangeLike ∧ contains (getPoint p) (getInterval i)) ∨ (i.isPointLike ∧ p.isRangeLike ∧ contains (getPoint i) (getInterval p))模型强制执行的约束-- 良构性规则 -- 对于同一个媒体项时间点必须包含在 T0 到 T1 的区间内 theorem temporal_point_in_interval_well_formed (p i : MediaItem) (h : TemporalPointInInterval p i) : // 验证时间点确实在区间内 pointWithinIntervalBounds p.time i.start i.end修复后的实现对齐// Rust 实现中正确的关系构造implMediaItem{fnrelates_to(self,other:MediaItem)-bool{// 首先检查是否都是区间Interval Overlapifself.is_interval()other.is_interval(){returntemporal_overlap(self,other);}// 如果不适用回退到独立的点和区间关系// Point-in-Interval点和区间的关系if(self.is_point()other.is_interval())||(self.is_interval()other.is_point()){returnpoint_within_interval(self,other);}// 任何其他组合都不是这个关系false}}验证结果最终代码不只是测试通过 ✓ Temporal Overlap interval to interval区间对区间 ✓ Temporal Point-in-Interval point to interval点对区间 ✓ 这些是不同的关系有不同的良构性规则工作流变革Spec Driven Development为什么 Agent 改变了开发传统编码前维护形式化规范伴随实现非常难以为继不是因为想法不好而是维护成本是真实的维护实现、编写新代码、更改旧代码、添加新测试本身已经是一整个工作量尝试在常规工作负载旁边保持模型更新只在正确性和安全性有硬性要求的特定组件上做过Agent 介入后┌─────────────────────────────────────────────────────────┐ │ 新的工作关系 │ ├─────────────────────────────────────────────────────────┤ │ 我开发者 │ │ ↓ │ │ 专注于确保模型正确 │ │ 专注于压缩的参考点 │ │ - 有哪些概念 │ │ - 有哪些法则 │ │ - 架构应该保持哪些区分 │ │ ↓ │ │ Agent │ │ ↓ │ │ 帮助将这些更改传播到实现中 │ └─────────────────────────────────────────────────────────┘传统方式Spec-Driven 方式实现是真相所在合同是真相所在在 Agent 之外需要在脑中维护所有实现细节不断回到更小、更密集的预期构建表示实现细节始终相关实现细节相关次数减少Agent 不是我想让系统真相存在的地方。真相应该存在于 Agent 之外的合同中。Agent 帮助我保持实现与那个合同对齐。Prose 规范与 Lean 模型的关系┌─────────────────────────────────────────────────────────┐ │ 规范层级 │ ├──────────────────────┬──────────────────────────────────┤ │ Prose 规范 │ Lean 模型 │ ├──────────────────────┼──────────────────────────────────┤ │ 探索系统的最佳场所 │ 强制系统的重要部分变得足够精确 │ │ 允许模糊和迭代 │ 以至于可以失败 │ │ 不编译 │ 编译 │ │ 可以悄悄过时 │ 编译失败时暴露问题 │ └──────────────────────┴──────────────────────────────────┘理解Lean 不替换 Prose它是正交的。Prose 规范是探索系统的地方Lean 模型是强制系统精确到可以编译的地方验证流程的实际应用测试告诉你存在不匹配。Agent 让不匹配消失了。形式化模型告诉你那个消失是否合法。流程┌─────────────────────────────────────────────────────────┐ │ Spec-Driven Agent Workflow │ ├─────────────────────────────────────────────────────────┤ │ │ │ 1. 编写 Prose 规范探索 │ │ ↓ │ │ 2. 识别关键概念和区分 │ │ ↓ │ │ 3. 在 Lean 中形式化强制精确 │ │ ↓ │ │ 4. Agent 根据形式化规范修改实现 │ │ ↓ │ │ 5. 如果编译失败 → 架构不变量被破坏 │ │ 如果编译成功 → 继续 │ │ ↓ │ │ 6. 实现与规范对齐 ✓ │ │ │ └─────────────────────────────────────────────────────────┘总结Agent 编码的风险局部正确 ≠ 全局对齐每个模块通过测试但整体架构语义可能已变形渐变式破坏Agent 做合理的局部更改慢慢削弱系统含义不可见的熵增差异随时间复合可能成为意外架构的一部分形式化验证的作用强制精确迫使你决定概念实际意味着什么编译时检查架构不变量被破坏时成为编译错误可验证的真相来源系统真相存在于 Agent 之外的合同中Spec-Driven Development 的价值分离关注点开发者专注模型Agent 传播实现减少认知负担不需要在脑中维护所有实现细节保持架构意识即使系统不断增长也不失去与系统的联系为什么 Agent 让这成为可能方面传统方式Agent Lean维护成本高难以持续低Agent 传播更改注意力分配分散在实现各处集中在模型正确性真相位置实现形式化规范建议识别架构关键区分找出系统必须保持的不变量如 point-like vs range-like使用形式化模型表达将关键概念和关系在 Lean 中形式化集成到 CI/CD将 Lean 模型编译作为构建步骤作为 Agent 的约束要求 Agent 在修改时遵守形式化规范保持模型简洁模型应该直接和简单不应该复杂