意图形式化：AI代理时代可靠编程的重大挑战
Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
当 AI 可以写代码，谁来确保它真正做了你想要的事？微软研究院 Shuvendu Lahiri 论证核心挑战是意图形式化——将模糊的人类意图转化为可检查的正式规约。从测试到 DSL 的四层谱系，TiCoder 的交互式实践，以及自动化度量揭示人类评审遗漏的缺陷——这篇立场论文定义了 AI × 形式方法 × HCI 的研究议程。
TL;DR — AI 现在可以写代码，但谁来检查它是否真正做了你想要的事情？本文论证核心挑战是 意图形式化（intent formalization）——将模糊的人类意图自动转化为精确的、可检查的规约。关键转变是：从"验证技术不够强"转向"没有规约可供验证"。
一、问题的本质：Vibe Coding 时代的意图鸿沟
当 Andrej Karpathy 在 2025 年初提出 "Vibe Coding" 这个词汇时，他精准地捕捉到了 AI 编程范式的本质转变：开发者用自然语言描述需求，AI 自动生成代码，人从"作者"变成了"监督者"——甚至有时候只是代码的被动"消费者"。
但一个根本性的问题始终悬而未决：生成的代码真的符合用户的意图吗？
论文用一个看似简单却极具启发性的例子揭示了这个问题。当用户说"给定一个整数列表，去重"，他们真正想要的是什么？
- 理解 A：保留每个元素的一个副本 →
[1,2,3,2,4]→[1,2,3,4] - 理解 B：删除所有重复出现的元素，只保留唯一的 →
[1,2,3,2,4]→[1,3,4]
人类开发者通过领域知识和对话来解决这种歧义；LLM 仅仅依赖训练数据的统计模式——这导致代码"看起来正确"，却可能悄然偏离用户的实际意图。以下代码对理解 B 而言就是错误的，但它编译通过、看起来合理：
# Listing 1: 看起来正确但实际不符合"删去所有有重复的数字"的意图
def remove_duplicates(numbers):
return list(dict.fromkeys(numbers))
# remove_duplicates([1,2,3,2,4]) → [1,2,3,4] ✓ 对理解 A 正确，✗ 对理解 B 错误而一个形式化的后置条件能精确消除歧义：
# Listing 2: 捕获"删去所有有重复的元素"意图的后置条件
assert all(numbers.count(x) == 1 for x in result)
assert all(x in result for x in numbers if numbers.count(x) == 1)作者指出 AI 从两个维度放大了这个意图鸿沟：
- 规模化而无审查（Scale without scrutiny）：AI 生成代码的速度超过了人类审查的速度。传统保障——代码审查、手动测试——跟不上代码产出的步伐。
- 合理性而非正确性（Plausibility without correctness）：LLM 生成的代码构造上就是合理的——看起来正确、能编译、通常通过测试——但不是构造上正确的。微妙错误隐藏在表面流畅性背后，使 AI 生成的 bug 比手写的更难发现。
核心洞察：AI 生成的代码是"合理构造"的，但不是"正确构造"的。意图鸿沟——用户意图与程序行为之间的语义距离——才是可靠性的真正瓶颈。
1.1 为什么是现在？
在 Codex 时代（2021），AI 编码还只是自动补全助手：建议单行或小代码块，开发者保留完全控制。但今天，agentic coding 工具（GitHub Copilot coding agent、Claude Code 等）自主地规划、编写、测试和调试整个功能。
这一转变有三个使意图形式化变得关键的后果：
- 人类审查正在被绕过：当开发者以最少或不审查接受 AI 生成代码时，形式规约成为检查生成代码匹配用户意图的唯一可扩展机制。
- 攻击面已爆炸性增长：AI 生成代码以前所未有的规模进入生产——包括安全关键和安全敏感系统。一个规约缺口可能有巨大后果。
- 技术已就绪：驱动 vibe coding 的 LLM 也可以生成规约。验证基础设施（SMT 求解器、证明助手、类型系统）经过数十年已成熟。首次可以实现闭环：生成代码、生成规约、并相互验证——全部在 AI 辅助工作流中。
二、核心命题：意图形式化
作者提出了一个关键的方向转变：与其问"AI 能写出代码吗？"，不如问"AI 能帮助我们明确代码应该做什么——并验证它确实做到了吗？"
意图形式化（Intent Formalization） 被定义为：将非正式用户意图自动翻译为一组形式化的、可检查的程序规约。
四层规范谱系
这个转换过程提供了从轻量级到严格验证的完整谱系：
| 层级 | 形式 | 代表工具 | 验证方式 | 适用场景 |
|---|---|---|---|---|
| 测试 | I/O 样例 | TiCoder, nl2postcond | 动态执行 | 快速验证、持续集成 |
| 代码契约 | 断言/前置/后置条件 | ClassInvGen | 运行时检查 | 防御性编程 |
| 逻辑契约 | Dafny/Verus/F* 规范 | Auto-Verus, VeriStruct | 静态形式验证 | 高可靠性系统 |
| 领域特定语言 | 完整规范 | 3DGen, EverParse | 验证合成 | 协议解析、关键基础设施 |
关键洞见：这些层级不是互斥的，而是互补的。测试可以验证后置条件，后置条件可以引导不变量发现，不变量可以支撑完整的形式化证明。最重要的是，前两层（测试和代码契约）是语言无关且可立即部署的——不需要切换到验证感知语言。
这里有两个重要的概念区分：
- 意图形式化 ≠ 自动形式化（autoformalization）。自动形式化追求将完整自然语言规约翻译为形式逻辑，追求完全保真度；意图形式化提供成本有效的谱系——从消除 NL 提示中最容易产生歧义的属性开始，到从中自动合成正确代码的 DSL。
- 意图形式化补充而非替代规约驱动开发。GitHub Spec Kit 等工具围绕自然语言需求结构化 AI 编码，但这些规约仍然是非正式的、不可检查的。意图形式化通过产生形式的、可检查的规约来弥合这一鸿沟。
2.1 规约与验证的区别
必须区分规约和验证。规约描述代码应该做什么；验证检查代码确实做到了。
- 测试：对有限多个输入验证规约。轻量级且广泛适用，但通过所有测试不保证对未见输入的正确性。
- 运行时检查：在生产中对每次执行验证规约。后置条件和断言在运行时评估，提供比离线测试更强的覆盖，但仅在错误被触发时检测。
- 证明：对所有可能输入验证规约。由 SMT 求解器或证明助手生成，提供数学保证，但需要更丰富的规约和更复杂的自动化。
意图形式化聚焦于规约侧。当今的关键瓶颈是缺少可供验证的形式规约——验证技术本身继续进步，但规约是前提，没有它们验证工具闲置。意图形式化提供权衡谱系：即使在可能歧义点的针对性规约也作为成本有效的护栏。
三、关键瓶颈：如何验证规范本身
论文提出了意图形式化中最棘手的问题：规范本身的验证。代码可以通过测试来验证，但规范的"正确性"却无法通过测试来确认——因为除了用户之外，没有规约正确性的独立预言机。用户意图只存在于用户脑海中。
这一节的内容是论文中最具原创性的贡献之一。
3.1 LLM 可以生成有意义的规约
这不是推测。多条独立研究线提供了具体证据：
- 在 Defects4J 基准（数百个大型 Java 项目中的真实 bug）上，LLM 生成的后置条件捕获了每八个真实 bug 中的一个，包括经典 Daikon 不变量检测器遗漏的 bug。GPT-4 生成的规约在健全性和完整性上显著高于 GPT-3.5 或 CodeLlama，表明规约质量随模型能力缩放。
- ClassInvGen 为 C++ 数据结构合成类不变量——一个精心选择的类不变量可以替代数百个函数级规约。
- VeriStruct 进一步扩展到 Verus 中的整个数据结构模块，验证了包括链表、哈希映射和 B 树在内的 11 个模块中的几乎所有函数。
这些结果确立了：LLM 可以产生编码真实语义理解的规约，不仅仅是语法模式。
3.2 如何衡量规约质量
一个前置问题立刻浮现：我们如何衡量生成的规约是否足够好？
作者倡导基于两个属性的自动化指标：
- 健全性（Soundness）：规约与正确行为一致——不拒绝有效实现。
- 完备性（Completeness）：规约具有辨别力——拒绝错误实现。
两种属性通过仅使用测试（输入/输出对）来操作化，不需要代码本身：规约 S 关于测试套件 T 是健全的，如果 S 在每个测试上被满足；规约 S 关于 T 是完整的，如果它能够检测到输出变异后的错误。
一个令人深思的例子：专家评审标记为"强"的 Dafny 规范，其完备性检验却发现了缺陷：
// Listing 3: 专家评审标记为"强"的 Dafny 规范——但自动化完备性度量揭示它不完整
ensures forall x :: x in result ==> (InArray(a, x) && InArray(b, x))
ensures forall i,j :: 0<=i<j<|result| ==> result[i] != result[j]这表示 result 中每个元素出现在两个输入中，且结果无重复——是健全的，但不完整的。自动化符号测试发现 ==>（蕴含）应为 <==>（双向蕴含）：没有双向蕴含，空列表平凡地满足规约。
修正版：
// Listing 4: 修正后的规范，使用双向蕴含
ensures forall x :: x in result <==> (InArray(a, x) && InArray(b, x))在整个评估中，自动指标发现了 3 个错误标注和 2 个由复制粘贴错误引入的不一致规约——全部被人类评审遗漏。
你不能改进你无法衡量的东西。自动化指标对于扩展意图形式化至关重要。
这些指标还启用下游证明自动化。Auto-Verus 系统使用健全性和完整性指标过滤 LLM 生成的 Rust/Verus 程序规约和证明，通过自演化循环引导高质量训练数据，证明准确率比 GPT-4o 零样本高 3.6 倍。
3.3 TiCoder：交互式意图形式化
TiCoder 系统在代码生成期间交互式地使用意图形式化。
TiCoder 不是接受 LLM 产生的任何代码，而是生成优先考虑歧义点的候选测试——不同代码候选产生不同输出的输入——并要求用户将每个分类为"是"、"否"或"未定义"。批准的测试通过代码执行修剪不正确候选。
TiCoder 交互示例——提示："找出两个列表的共同元素。"
生成测试：
common([1,2,3],[2,3,4]) == [2,3]— 用户：是common([1,2,2],[2,2,3]) == [2,2]— 用户：否通过拒绝测试 2，用户明确歧义：结果应该是集合，不是多重集。TiCoder 据此剪枝保留重复元素的候选。
一项涉及 15 名专业开发者的对照研究发现：
- 使用 TiCoder 后，正确评估 AI 生成代码的频率约为不使用时的两倍（p < 0.001）
- 认知负荷显著降低（p = 0.007）
- 批准的测试持久化为回归测试
- 大多数参与者偏好 TiCoder
这体现了按需付费哲学：TiCoder 从谱系成本有效端开始，针对最可能暴露 LLM 解释偏离用户意图的测试。少量意图形式化——批准几个测试——在正确性上产生显著回报。
3.4 端到端验证管线：3DGen
在谱系远端，3DGen 系统展示了 DSL 级别的意图形式化，规约足够完整以自动生成代码。
3DGen 使用多 agent AI 架构将非正式 RFC 文本翻译为 3D 领域特定语言中的形式规约，符号测试生成提供迭代精化的反馈。验证的 3D 规约通过 EverParse 编译为可证明正确的、内存安全的 C 或 Rust 二进制解析器——规约就是程序，由验证合成中介。
它已为 20 种标准网络协议格式（DNS、TLS 扩展、QUIC）产生验证解析器——展示了从非正式文本通过 DSL 到可证明正确的可部署代码的完整谱系潜力。
四、研究前沿：七个开放挑战
早期研究在基准问题上展示了潜力，但也揭示了离通用解决方案有多远。七个开放问题定义了研究前沿，横跨 AI 能力、形式方法基础设施、人机交互设计和软件工程实践。
4.1 从基准测试到真实系统
当前结果针对自包含的算法函数。真实世界软件有副作用、可变状态、并发和复杂依赖。异步事件处理器或 ML 管道的"后置条件"意味着什么？需要真实世界意图形式化的基准、指标和规约习语。
4.2 变更意图与组合性
实践中多数开发是修改现有代码而非从头编写。意图形式化必须捕捉"应该改变什么"并与现有规约组合。密切相关的是代码翻译——如将遗留 C 代码迁移到 Rust。SpecTra 等早期工作表明从源代码生成中间非正式规约并用其指导翻译显著改善正确性。
4.3 成本有效的澄清优先级
对从业者而言，规约的价值由它能防止多少 bug 衡量。需要按预期影响排名规约的指标。TiCoder 通过生成多样代码候选并针对候选不一致的输入生成测试迈出第一步——但这需要采样合理实现空间，对大代码块变得昂贵。
4.4 规范验证的自动化度量
由于除用户外没有规约正确性的独立预言机，进展需要整合多个互补信号：测试和变异分析作为自动化代理、针对性用户反馈、跨不同制品（代码、文档字符串、形式注释）的交叉检查。
4.5 丰富逻辑与量词
验证感知语言使用量词、递归谓词和幽灵变量。LLM 在这些构造上表现欠佳，现有验证器在展开复杂具体测试输入的递归谓词方面有根本限制，使自动化健全性和完整性评估困难。
4.6 人机交互规范设计
TiCoder 的批准/拒绝循环在基准问题上显著提升了正确性，但真实世界的规范需要更丰富的交互：自然语言解释形式属性、置信度校准建议、规范模板——这是一个很大程度上尚未探索的 HCI 设计空间。
4.7 集成到开发者工作流
意图形式化必须自然融入现代开发者工作流：从 issue 创建（规约在代码编写前捕获预期行为），到代码审查（规约为审查者暴露意图），到 CI/CD 管线（agentic 工作流持续发现和验证规约以应对演化需求）。在 vibe coding 时代，当人类可能永远不检查代码时，规约成为人类意图和机器行为之间的主要接口——使这种集成不仅是理想的，而且是必不可少的。
五、相关工作
意图形式化借鉴并扩展了多个已确立领域：
- 规约挖掘（Specification mining）：经典工具如 Daikon 从执行轨迹推断不变量，但无法捕获超越观察行为的用户意图；LLM 驱动的规约生成通过推理预期语义超越此限制。
- LLM 驱动代码生成：HumanEval 等基准通过 pass@k 评估代码正确性但不评估规约质量；意图形式化将评估目标从"代码通过测试吗？"转向"规约捕获意图吗？"
- 形式验证：SMT 求解器、证明助手和验证感知语言（Dafny、Verus）提供检查规约的成熟基础设施但无法生成它们——意图形式化提供缺失的输入。
- LLM 用于验证：近期利用 LLM 进行程序验证和 Dafny 规约合成的工作主要聚焦于使给定程序的验证成功，而非捕获尚不存在代码的用户意图。
六、结论与启示
这篇论文提出了一个核心论断：AI 生成代码的时代已经到来，但可靠 AI 生成代码的时代尚未到来。意图形式化——使人类意图明确化、可检查、可执行——是弥合这一差距的有前景的方向。
作者呼吁社区将意图形式化视为一等优先级：需要专用基准、AI/PL/形式方法/HCI 研究者之间的跨学科协作，以及持续投资。
意图鸿沟是瓶颈；弥合它将决定 AI 让软件更可靠还是仅仅更丰富。
对系统设计者的启示
- 多层次规范策略：不要追求一刀切的验证方案，根据可靠性需求采用不同层级的规范——从针对性测试护栏到完整 DSL 合成
- 人机协作优于完全自动化：TiCoder 的成功表明，将用户纳入规范验证闭环能显著提升正确性，而交互应最小化且高回报
- 度量驱动：自动化规范质量度量（健全性/完备性）是规模化意图形式化的关键前提——你不能改进你无法衡量的东西
对 AI Agent 开发者的启示
- 从代码生成转向规范生成：AI 的能力不仅在于写代码，更在于帮助明确"代码应该做什么"
- 歧义点的主动识别：系统应该识别可能产生不同实现的输入点，并主动寻求澄清——像 TiCoder 那样生成针对歧义点的测试
- 验证基础设施的整合：形式验证工具不应是事后补丁，而应成为开发工作流的有机组成部分
论文信息
- 标题：Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
- 作者：Shuvendu K. Lahiri (Microsoft Research)
- 发表：arXiv:2603.17150v1, March 2026
- 相关项目：TiCoder, Auto-Verus, 3DGen, VeriStruct, ClassInvGen
- 所呈现材料基于 FSE 2024、FMCAD 2024、IEEE TSE 2024、ICSE 2025、ICLR 2025、SAIV 2025 和 TACAS 2026 发表的工作