当 AI 写代码时，谁负责证明它正确？
AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
当代码生成变得轻而易举，验证其正确性却成了新的瓶颈。AWS 的 Leo de Moura 作为 Lean 语言创始人，在对话中探讨了 AI 如何推动形式化验证的普及。从自动形式化（autoformalization）到验证 Rust 代码，AI 不仅能将数学定理或任意语言编写的程序转化为 Lean 模型，还能辅助发现深层漏洞。然而，机器检查的 Lean 证明虽能消除“信任我”式的代码依赖，但模型是否忠实于原代码仍需人工把关。随着 Mathlib 库在 AI 助力下规模激增，软件工程正从单纯写代码转向定义规格与证明，未来或许人人都是验证者。
形式化验证不仅能解决人与人之间的信任瓶颈，更能解决人与 AI 之间的信任瓶颈。
HN 评论区
25- chamomeal
大家对属性测试（property based testing）怎么看？我设置了一些属性测试，感觉它几乎就像形式化验证一样。
我知道这两者并不完全相同，但属性测试能捕捉到各种极其离谱的 bug，这些是我根本想不到的检查点。涉及状态的东西、跨服务的东西。我对属性测试唯一的抱怨一直是设置过程太繁琐，但大语言模型（LLM）解决了这个问题。
最近好像没怎么看到关于属性测试的讨论，但在大语言模型时代，它的投入产出比极高。
- wbeckler
我觉得终极组合是 Lean 4/TLA+/等等，加上 AI，再加上确定性生成器。对于大型系统，形式化方法的断言需要压缩到人类可理解的大小。当断言用于确认模型及其附带代码生成器的准确性时，这种情况就会发生。生成器可以生成所生成代码的证明，而人类只需要确保生成器能够可证明地生成正确的大规模断言。
这就是形式化方法如何约束大型系统中的 AI。
我们在 Open Markets Initiative 正在做这件事，我们生成了数百万行的 Lean 4、TLA+ 和 Rocq 代码，以确保我们的开源电子交易协议代码准确无误。我们原本没预料到，但 Lean 证明器确实识别出了一些错误的步骤。
- PandaRider
> ... 但我们预计，在未来几个月乃至几年里，人们会将更多精力集中在规范、模型以及你希望软件具备的属性上。
有人有学习形式化验证建模的资源推荐吗？（不一定要用 Lean）