一个代码模型收到 bug 报告，很快给出补丁。代码能够编译，现有测试也全部通过，reviewer 看了一眼，觉得改法十分自然。两周后，一个测试集中没有覆盖的输入再次触发故障：补丁只是绕过了样例，并没有修复真正的错误。
这个故事并不说明大模型不会写代码。恰恰相反，它说明生成一段“看起来正确”的程序已经很容易，而判断它对所有相关输入是否满足要求仍然很难。模型可以提出候选实现、测试、断言甚至证明；最终的可靠性却取决于这些产物能否被执行、分析或机器检查。
前五篇建立了从程序状态到静态分析器的完整路线。最后一篇不再重复每个公式，而是讨论它们在 AI 辅助开发中的新位置：大模型适合承担哪些开放式工作，形式化方法能提供什么保证，两者结合时又应把信任边界画在哪里。
文章会先区分“生成一个合理候选”与“证明某个性质成立”，再考察 LLM 如何与静态分析、符号执行和程序修复组合。讨论的重心始终是两个问题：一套混合系统的最终结论由谁验证，这个结论又受哪些规格、语义模型和工具范围约束。
一、两种不同的“理解程序”
代码大模型从大量自然语言与程序中学习统计规律，因此很擅长补全代码、解释意图、迁移常见 API 用法和生成候选修复。面对一个陌生函数，它往往能迅速给出“这段代码大概在做什么”，也能利用注释、命名和周围模块推断业务含义。
传统程序分析走的是另一条路线。研究者先定义程序语义、状态空间与检查性质，再让算法按照明确规则传播信息。例如，空指针分析会规定：
- 哪些值属于
Null、NonNull或Unknown； - 每条语句怎样改变这些值；
- 分支与函数调用怎样传播状态；
- 什么时候可以报告或排除空指针错误。
两种方法的优势并不重合。大模型善于处理不完整描述和开放式搜索，形式化分析善于在给定模型内进行可复查的系统推理。
但从上下文生成流畅答案，并不等于提供了语义保证。假设模型看到：
1
2
int *p;
*p = 10;
它很可能指出未初始化指针风险，但这段回答本身没有说明它检查了哪些路径、采用了什么内存模型，也没有提供一份可以由独立检查器验证的证据。即使每次都生成相同答案，也不等于结论已经被证明。
反过来，大模型完全可以参与证明：它可以生成循环不变量、SMT 约束或 proof assistant 的证明项。关键区别不在于“内容是否由 AI 写出”，而在于最终结果是否交给了一个具有明确语义的检查器。
LLM 输出通常应被视为 candidate；测试结果、反例、求解器结论或机器检查通过的证明，才构成相应范围内的 evidence。
形式化方法也不是无限保证。形式化工具的结论总是相对于某个规格和模型。例如，证明函数满足错误的规格，并不能让软件满足真实需求；忽略反射、原生库或并发行为的模型，也不能覆盖这些未建模部分。
因此，“形式化验证过”之后仍要追问：验证了什么性质，采用什么程序语义，环境假设是什么，哪些模块不在范围内。形式化方法的价值不是宣称绝对正确，而是把结论和前提都写得足够清楚，使其能够复查。
二、组合方式一：让 LLM 补充分析器缺少的知识
一个污点分析器知道数据怎样沿赋值和调用传播，却未必知道某个第三方 API 是 source、sanitizer 还是 sink。一个错误处理分析器能够追踪返回值，却可能缺少“这个函数用哪个返回值表示失败”的规格。人工维护这些规则既昂贵，又容易落后于代码变化。
LLM 可以根据函数名、文档、调用方式和邻近代码提出候选规则，静态分析器再把这些规则放回全程序的数据流中验证和使用。这样，模型负责处理含糊的上下文，分析器负责稳定地传播结果。
一个具体例子来自 Chapman、Rubio-González 与 Thakur 的工作：他们将静态分析中间结果放入提示，再把 LLM 推断的 error specification 送回分析器。研究对象不是泛泛的“理解代码”，而是一个明确任务：推断 C 函数用哪些返回值表示错误，并据此发现错误处理缺陷。论文报告了在其实验对象上的 recall 与 F1 改进，也专门分析了模型非确定性带来的影响。详见论文 Interleaving static analysis and LLM prompting with applications to error specification inference。
这个例子的重要之处在于分工：LLM 没有取代程序分析，而是在分析器缺少规格时提供候选知识；候选知识的效果仍然通过明确的分析任务和 benchmark 衡量。
这里能否维持 soundness，取决于 LLM 输出被怎样使用。如果 LLM 只负责排列 alarm 优先级，最坏结果可能是开发者先看错了报告；如果系统直接删除模型认为“不重要”的路径，就可能破坏原分析的覆盖保证。类似地，把模型生成的 transfer rule 当作可信规则，会把模型错误带进整个求解过程。
较稳妥的设计包括：保留原 sound 分析作为回退路径；让模型只增加候选而不删除行为；或者要求生成结果通过类型检查、测试、静态约束或人工审核后再进入可信规则库。是否维持 soundness，不由“用了 LLM”或“用了静态分析”决定，而由数据流和信任边界决定。
三、组合方式二：让 LLM 搜索，让工具检查
3.1 自动程序修复中的候选—验证循环
传统自动程序修复需要在巨大的补丁空间中搜索。大模型可以利用代码上下文快速提出更像人类修改的候选 patch，于是流程变成：
1
2
3
4
5
6
7
错误报告与上下文
↓
LLM 生成候选补丁
↓
编译、测试、静态分析或形式化验证
↓
接受、拒绝，或把反例反馈给下一轮
这是一种常见的 neuro-symbolic 分工：生成模型缩小搜索空间，确定性工具负责检查可执行条件或逻辑条件。2025 年的一项跨语言实证研究在六个 benchmark 上分析了大量 LLM 生成补丁，也发现模型选择与提示方式都会明显影响修复表现；可参见 Empirical Evaluation of Large Language Models in Automated Program Repair。
不过，通过测试并不等于补丁正确。测试只覆盖有限输入，一个 patch 可能通过硬编码、绕过分支或删除功能来迎合测试集，这就是 test-suite overfitting。因而“tests passed”只证明这些测试没有观察到失败，不能自动推出程序满足完整规格。
如果有形式化规格，可以进一步使用符号执行、model checking 或 deductive verification 检查补丁；如果没有，就需要补充测试、静态检查、代码审查和运行时监控。验证强度应与软件风险匹配，而不是把所有项目都送进同一种最昂贵的证明流程。
3.2 不变量和证明也可以先生成再检查
循环不变量、函数契约和证明策略往往很难自动发现，却相对容易由验证器检查。LLM 可以根据代码提出候选不变量，SMT solver 或 proof assistant 再验证候选是否满足初始化、保持和退出条件。
例如，LaM4Inv 把 LLM 生成与 bounded model checking 结合，用反例反馈改进循环不变量。这里真正可信的不是模型“觉得不变量合理”，而是候选经过形式化条件检查。相关方法见 LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference。
四、组合方式三：用模型帮助探索复杂路径
符号执行用符号变量代表输入，并沿路径累积约束：
\[x=a, \qquad PC=a>0.\]到达目标位置后，SMT solver 判断路径约束是否可满足，并在可能时给出具体输入。问题在于每个分支都可能复制状态，循环还会产生无界路径，导致 path explosion。
LLM 可以根据代码语义为路径排序、生成摘要、猜测循环不变量或建议更可能触发错误的输入。这些启发式可能提高有限预算内的发现效率，但如果系统永久剪掉未探索路径，就不能继续声称“所有路径都已覆盖”。
“更像在推理”的输出仍要接受执行检验。2025 年 ICML 的一项研究让多种模型处理编译器 IR，并测试 CFG 重建、反编译、摘要和执行推理。模型能够识别部分语法与高层结构，但在指令级执行、控制流和循环上更困难。它提醒我们：生成一段合理的程序说明，与逐步跟踪低层语义并不是同一项能力。参见 Can Large Language Models Understand Intermediate Representations in Compilers?。
因此，模型给出的路径判断最好通过解释器、编译器 IR 工具、符号执行器或测试运行来落地。能执行的证据通常比另一段自然语言自评更有价值。
五、怎样设计可信的混合分析系统？
一套混合系统至少包含三类组件：
1
2
3
4
5
6
7
8
9
程序、规格与上下文
│
┌─────────┴─────────┐
│ │
LLM 候选生成 程序分析与执行工具
│ │
└─────────┬─────────┘
│
可检查的结果与证据
设计时应明确哪些输出会影响最终结论。模型生成一段解释和模型生成一条“可信 transfer rule”的风险不同；模型建议优先检查某条路径和模型授权系统忽略其余路径的风险也不同。
一种实用原则是把开放式生成限制在可验证接口之外：让 LLM 提议，让较小、语义明确的组件裁决。例如：
| LLM 提议 | 检查组件 | 能得到的证据 |
|---|---|---|
| 候选补丁 | 编译器、测试、静态分析器 | 编译结果、测试轨迹、alarm 变化 |
| 路径输入 | 程序执行器、fuzzer | 可复现的崩溃或覆盖信息 |
| 循环不变量 | SMT solver、验证器 | 验证成功或反例 |
| API 规格 | 类型检查、数据流分析、人工审核 | 一致性检查与分析指标 |
| 证明项 | proof assistant kernel | 机器检查通过的证明 |
检查器本身不必完美，但它的语义、失败模式和覆盖范围应比自然语言判断更清晰。
信任边界还必须覆盖失败情况。可信系统不仅要给出“通过”或“失败”，还应保留路径、约束、反例、测试日志、模型假设和未支持特性。这样，开发者才能判断是候选本身错误、规格不完整，还是分析工具无法覆盖当前语言特性。
对于高风险场景，还应避免让模型在证据不足时静默降级。例如，验证器超时与验证成功不是同一状态，缺少库模型与确认安全也不是同一结论。
六、阅读 LLM + Program Analysis 论文的五个问题
面对一篇混合方法论文，可以按下面的顺序检查：
- 任务是什么？ 是生成补丁、排序 alarm、推断规格，还是证明性质？
- LLM 产生什么？ 自然语言判断、候选程序、抽象规则，还是可检查证明？
- 谁作最终决定？ 模型、测试、求解器、静态分析器还是人工？
- 失败会怎样？ 是多报、漏报、超时，还是退回原有分析？
- 实验测量了什么？ pass rate、真实正确性、recall、false positive、运行成本，还是 soundness？
同一个“LLM 提升了分析效果”的标题，可能对应完全不同的可靠性含义。把这五个问题回答清楚，通常就能看出论文真正的技术贡献。
进一步阅读。 如果想了解这个交叉方向的整体版图，可以先阅读 A Contemporary Survey of Large Language Model Assisted Program Analysis。它按静态、动态与混合程序分析整理相关工作。随后可根据兴趣选择本文链接的错误规格推断、自动修复、循环不变量或编译器 IR 研究，不必一次读完所有方向。
对于形式化基础，站内的 Easy Foundations for Programming Languages 系列继续讨论程序语言理论；Software Foundations 则适合系统学习程序语义与机器辅助证明。
七、回到这个系列：六篇文章连成了什么？
六篇文章逐步回答了六个问题：
| 篇目 | 核心问题 |
|---|---|
| 第一篇 | 集合、映射和语义符号怎样翻译成程序概念？ |
| 第二篇 | 代码怎样变成 CFG，状态怎样随执行迁移？ |
| 第三篇 | 状态太多时，怎样用抽象域保留关键性质？ |
| 第四篇 | Transfer function、join 和 worklist 怎样求得不动点？ |
| 第五篇 | 分析器怎样在 soundness、precision 与规模之间取舍？ |
| 第六篇 | LLM 参与开发后，候选与可验证结论怎样分工？ |
这条路线最终形成一种阅读方法：先找论文定义了哪些对象，再看对象之间如何转换，然后确认合并与收敛规则，最后检查结论的范围和假设。无论方法使用经典静态分析还是大模型，这套问题都仍然有效。
八、结语：从“看不懂公式”到“知道为何可信”
8.1 回到第一篇的那行公式
这个系列开始于一个很普通的时刻：读论文时，一行公式突然出现在眼前，每个符号似乎都认识，合在一起却不知道该从哪里读起。
六篇文章走下来，我们没有学完一整套高深数学，而是逐渐建立了一种阅读程序的方法。看到集合和映射时，我们开始寻找论文定义了哪些对象；看到 CFG 时，我们知道作者正在描述程序可能走向哪里；看到程序状态和 transfer function 时，我们开始追踪一条语句如何改变信息；看到 lattice、join 和 fixed point 时，我们能够理解分析器怎样合并路径，并在循环中得到稳定结果。
到了最后，我们面对的不再只是一行公式，而是一套关于程序的完整论证：
\[\text{程序如何表示} \longrightarrow \text{信息如何抽象} \longrightarrow \text{状态如何传播} \longrightarrow \text{结论为何成立}.\]8.2 形式化训练的是一种提问方式
形式化真正训练的，并不是计算能力，而是把含糊的问题问得足够准确：
- 我们正在讨论什么对象？
- 哪些行为被模型覆盖？
- 哪些细节在抽象中被舍弃？
- 分析结果提供了什么保证？
- 这个保证又依赖哪些前提？
这些问题在大模型时代反而更加重要。模型可以迅速生成代码、补丁、测试和解释，但“看起来合理”与“值得相信”之间仍有一段距离。测试、静态分析、求解器和机器检查证明的作用，就是让这段距离变得可见、可检查，也可以被质疑。
回头再看第一篇中的公式：
\[\sigma:X\rightarrow V.\]它现在应该不再像一道需要求解的数学题。你会自然地读出：“程序状态把每个变量映射到一个值。”更重要的是，你还会继续追问：这些值是具体的还是抽象的？状态怎样更新？不同路径如何合并？最终结论覆盖了哪些程序行为？
当这些问题开始自然地出现在脑海中，这个系列真正想建立的阅读方式就已经形成了。
最终值得带走的判断标准，也由此变得清楚。大模型扩大了软件工程的搜索与生成能力，形式化方法则让一部分结论能够被精确定义和独立检查。二者并不是“谁取代谁”的关系。更有用的问题是：
哪些步骤允许试错和猜测，哪些步骤必须给出可复现、可检查的证据？
当你能够为一套系统画出这条边界，就不仅是在读公式，也是在判断一项软件工程研究究竟提供了怎样的保证。
形式化的终点，不是让软件脱离人的判断，而是让我们面对越来越复杂的程序、分析器与 AI 系统时，仍然能够清楚地回答：
我为什么可以相信这个结论？