当前位置：首页 > news >正文

Agent 如何悄悄破坏架构？Lean + Rust 形式化验证指南

news 2026/6/25 21:36:20

Agent 编码的渐进式失控
本地正确性 ≠ 全局架构对齐
实例：范围类媒体 vs 点类媒体
- Agent 视频编辑器的架构
- 关系语义的重要性
Agent 造成的实际破坏
解决方案：Lean 形式化验证
- 为什么选择 Lean
- 添加新关系
- 模型强制执行的约束
- 修复后的实现对齐
工作流变革：Spec Driven Development
Prose 规范与 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 形式化验证

为什么选择 Lean

Prose 规范的问题：
- 不强迫你决定概念实际意味着什么
- 无法强制执行下游约束
- 可以变得悄悄过时——你可以更改实现、测试和架构，而 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 Overlap）ifself.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. 实现与规范对齐 ✓ │ │ │ └─────────────────────────────────────────────────────────┘