LLM 正在让形式化软件验证在更大规模上变得可行

LLM、形式化验证与能力边界

• 多条评论将 Anthropic 的结果与“凸包”想法联系起来：LLM 在人类数学实践范围内做插值，但可能难以发明根本新的抽象。
• 有人认为，LLM 擅长艰难地推演大量已知风格的证明，但如果没有更好的抽象和推理策略，就会碰到复杂性墙。
• 也有人反驳说，在更难任务上进行强化学习可能会涌现出更好的证明策略，因此这个边界并不清楚地固定。

证明风格、抽象与复杂性

• 由 agent 生成的证明被描述得极其冗长，会展开每一个底层执行细节。
• 这也映射到 LLM 写代码和测试的方式：脆弱、具体、重复、模块化较弱。
• 多人指出，要扩展验证规模，需要类似人类的证明工程：模块化抽象、可复用引理，以及更好的推理原则。
• 也有人乐观地认为，对良好证明结构的训练，可能会改善通用编码质量，尤其是在强类型函数式和类似 Rust 的生态中。

到底验证了什么？规格、模型与局限

• 强调“形式化验证”总是意味着“相对于某个形式化规格/模型”，而这未必与真实意图或真实硬件一致。
• 担心 LLM 会生成空洞或规格写错的定理，但它们仍能通过检查器，从而带来错误的信心。
• 有人强调经典限制（停机问题、Rice 定理），也有人指出这些并不妨碍对特定、非任意程序证明有用性质。
• 区分了验证（代码符合规格）与确认/校验（规格符合真实世界需求），并指出后者更难。

工作流、工具与抽象层级

• 一些实践者报告称，使用 LLM 配合 Lean/Rocq、ESBMC、Alloy、Verus 等取得了成功，尤其是在等价性证明方面（例如 C→Rust 重写、优化与参考实现的对比）。
• 验证编译后的二进制或 LLVM IR 被认为很强大，但也很“残酷”，需要大量机器生成的证明项；而这正是 LLM 规模化擅长的地方。
• 也有人认为，与完整规格相比，等价于“黄金参考实现”更易处理，也更适合遗留系统（例如 COBOL、Postgres C）。

声明式未来 vs 命令式现实

• 一派预测会转向确定性的声明式语言，配备丰富的类型/效应系统和内建可验证性，使形式化证明成为默认。
• 怀疑者则认为，一种足够灵活且高性能的声明式语言，最终要么会变成事实上的命令式语言，要么会重新遭遇“足够聪明的编译器”问题。
• 讨论还涉及 DSL、嵌入式声明式片段（SQL、LINQ、Inform7）以及分布式系统语义。

测试、模糊测试、安全与采用

• 许多人认为，当下主要的实际收益是：证明模糊测试性质对所有输入都成立（不崩溃、往返一致、代数律成立），其保证比单独 fuzzing 更强。
• 对这到底算不算“真正的”形式化验证，还是只是加强版测试，存在争论；但大多数人同意，这对安全性和稳健性仍是实质性提升。
• 有人对降低使用 Alloy、TLA+ 以及安全关键或高保证领域中的形式化方法门槛感到兴奋；也有人预测，除了“偏执”小众场景外，采用会有限。

社会经济与工作流担忧

• 一些开发者形容 LLM 既赋能又打击士气：一方面更快实验、更多验证；另一方面工艺感流失，并担心职业稳定性。
• 有人担心，行业会把 LLM 带来的“验证红利”用于追求更快速度和更粗糙的系统，而不是更高的保证。
• 一个反复出现的主题是：LLM 会放大既有倾向——草率团队会产出更多草率内容；谨慎团队则可以推进到过去因成本过高而无法实现的验证。