@ryanlpeterman: Leonardo de Moura（@Leonard41111588）是 Lean 和 Z3 定理证明器的创造者。我与他讨论了 Lean 如何……

Leonardo de Moura (@Leonard41111588) 是 Lean 和 Z3 定理证明器的创造者。我与他讨论了 Lean 的工作原理,以及为什么 LLM 加上 Lean 将从根本上改变我们编写软件和做数学的方式。

本期内容:

• 形式验证和证明助手如何工作
• Lean 将如何影响手写数学和软件 • Lean 在近期数学突破中的作用
• 什么时候软件值得进行形式化

观看方式:

• YouTube - https://youtu.be/KzdYKeAqWhY • Spotify - https://open.spotify.com/episode/34dbrI4zjw94K2R4S43BI3?si=ZiaycTbmTG6xgr3Ofq51Dw… • Apple Podcasts - https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835… • Transcript - https://developing.dev/p/creator-of-lean-the-end-of-handwritten…

感谢本期节目的赞助商对我工作的支持:

• WorkOS:通过易于使用的 API 让你的应用达到企业就绪(Enterprise Ready),只需几行代码即可添加 SSO、SCIM、RBAC 等功能,快来 https://workos.com 看看吧

章节:

00:00 开场 00:28 形式验证如何工作 05:21 编写软件的新方式 13:15 证明助手 vs 编程语言 21:06 Lean 如何助力数学突破 32:03 什么时候值得对软件进行形式化 33:29 Lean 将如何影响手写数学 38:55 他创立的 Z3 定理证明器项目 45:44 他职业生涯中最具技术挑战性的工作 51:10 Lean 与其竞争对手 01:00:37 Lean 的未来 01:04:10 技术书籍推荐 01:06:15 给年轻时的自己的建议 01:07:10 结尾

TL;DR: Lean 的创造者 Leonardo de Moura 在访谈中解释了 Lean 如何作为编程语言与证明助手,将程序性质变成机器可检查的数学证明,并说明 AI 正在大幅降低形式验证的成本,让它从安全关键组件走向主流。

引言

在这一集对话中,Lean 与 Z3 定理证明器的创造者 Leonardo de Moura 讨论了 Lean 的工作原理,以及它将如何影响数学和软件验证的未来。话题从 Dijkstra 的名言开始,延伸到 AI 辅助证明、zlib 验证、seL4 的往事,以及 Lean 自身的内核设计。

什么是 Lean?

主持人引用 Dijkstra 的名言:“程序测试可以用来证明 bug 的存在,但永远不能证明它们的缺失。”他问 de Moura:Lean 和形式化证明是否可以证明 bug 不存在?

De Moura 给出的定义是:

Lean 是一种编程语言。你可以写代码,但也可以写证明。你可以对自己的代码进行推理。你可以为代码编写状态性质并证明它们。Lean 给你机器可检查的证明。你可以检查你的证明,并获得它们绝对正确的保证。你有很多检查器,独立的检查器。但你应该把 Lean 看作一个平台。你可以写代码,可以为代码编写性质,并证明它们。

他强调 Lean 是一个平台,而不只是一个单一工具。

如何用 Lean 验证真实软件?

当被问及“证明”如何与日常软件工程结合时,de Moura 区分了两种非常不同的用例。

直接用 Lean 写程序

Lean 本身是一种编程语言。如果你直接用 Lean 写程序,那么程序与数学定义之间的差别并不大,验证技术也很相似。

验证用其他语言写的程序

如果要验证用不同编程语言(如 Rust 或 C)编写的程序,主要有两种方法:

• 浅嵌入(shallow embedding):例如现有工具可以把 Rust 映射到 Lean 中,然后验证翻译后的 Lean 代码。
• 深嵌入(deep embedding):在 Lean 中编写 C 语言的语义,C 程序变成 Lean 中的数据结构对象,你可以对这种对象陈述性质并推理。

一个具体例子:数组越界

主持人希望有一个非常具体的例子,比如一个简单的 C 程序,证明它没有缓冲区溢出。

De Moura 用数组访问说明这个过程:

• 假设你有一个数组,在 C 中访问它。
• 你希望确保索引在边界内:如果数组有 10 个元素,你不会试图访问第 11 个元素。
• 你可以在 Lean 中写出数学陈述:“在程序中的这个点,i 的值将大于或等于零且小于 10。”
• 另一种理解方式是:如果你能用数学表达你关心的程序性质,你就可以用 Lean 验证它。

主持人总结为:C 源文件之上有一层等价的 Lean 证明,几乎像元数据一样逐行对应。de Moura 确认,Lean 会逐行检查。

证明的结构与模块化

人们会构建自动化流程来组织证明,例如使用 Hoare 三元组:

• 执行语句之前应该有一个数学事实为真(前置条件)
• 然后是语句本身
• 再然后是什么为真(后置条件)

de Moura 指出,复杂性是软件验证中的挑战。即使有了 AI,如果想扩展,证明仍然必须模块化,这类似于软件工程中必须写干净代码、易于编辑和推理。可以把证明看成“软件之上的第二层软件”。

AI 正在改变形式验证的游戏规则

De Moura 描述了一个可能的未来:你先精确地用数学写出你想要的行为,然后让 AI 合成代码,并证明合成出的代码满足你的规格说明。

请 AI 帮忙。AI 会一直努力,直到 Lean 证明说你没问题。

Kim Morrison 与 zlib

这个未来在六个月前听起来像科幻小说,但实际已经发生。De Moura 的同事 Kim Morrison 在几个月前启动了一个项目:

• zlib 是一个用 C 写的压缩库。
• Kim 给 AI 创建了一个非常复杂的提示词:“我要你把它翻译成 Lean,确保 Lean 版本通过 zlib 的测试套件,然后我要你证明,如果你压缩数据再解压缩,你会得到原始数据。”
• 这是一条非常强的性质。结果大约一周后,他们成功完成了整件事。
• 现在他们只是在继续要求优化代码,但不能破坏证明——必须继续证明所有你关心的性质。

De Moura 说,“压缩和解压缩后得到原始数据”对压缩引擎来说是一个非常重要的性质,这现在“很丰富”“超现实”。

规格说明 vs 全面测试套件

主持人提到,行业里很多人用非常全面的测试套件加上 AI 做惊人的重写,因为这样对重写准确性更有信心。De Moura 同意规格说明甚至比全面测试套件更好:

有了测试套件,你能证明 bug 的存在,但不能证明它们的缺失。好的测试套件差不多是,你可能会说:“嗯,这里可能没有 bug 吧”,但你可能有一个真正的极端情况,你的测试套件没有覆盖到。但是有了证明,你覆盖了所有可能的情况。

这也与基于属性的测试联系起来。基于属性的测试很流行:人们写出希望确保为真的性质,但靠测试来检查。而现在“我们可以证明它们,然后你可以说:‘看,没必要再测试了。我证明了。’”

写规格说明有多难?

主持人问:与创建合理测试套件相比,制定合理规格说明要多花多少功夫?

De Moura 回答,差异很大,但有很多场景下规格说明并不难获得:

• 很多时候,人们开始开发软件时并不确切知道规格是什么,但性质通常在你心里是很清楚的。
• 低效的程序可以给你提供规格说明。通常写一个低效程序比写一个超级高效、有很多聪明技巧的程序容易得多。
• 你可以用非常朴素的方式写“这是我想要的”,然后让 AI 生成高效版本并优化,再证明它与你低效的版本等价。

他说:“我不是说规格说明总是很容易想出来,但性质方面,开发者通常对他们关心的性质有很好的想法。一个低效程序本身就是一种规格,你可以把它看作规格说明。形式验证技术是对测试的补充。”

为什么过去形式验证代价如此高昂?

主持人提到 Jane Street 更大力投资形式验证,以及 seL4——一个完全形式验证过的微内核。

De Moura 认为 seL4 是一个重要里程碑,但那是 AI 之前完成的项目,完全手动验证,成本非常昂贵。AWS 使用形式验证已经十年,但只用于超级安全关键的组件,因为成本高。“有了 AI,这改变了游戏规则。”

最痛苦的不是规格,而是证明维护

De Moura 说,必须想出规格说明不是最痛苦的部分。

最痛苦的部分是必须手动开发证明——如果你以前必须这么做的话——以及当你改变代码时维护证明。

他描述了这样的场景:有人抱怨改了程序后测试套件里有一堆失败,必须一个一个修复。对于证明也是同样的过程——你必须修复证明。而且有时候你已经不记得这个证明背后的故事是什么。这很麻烦。

但 AI 在写形式证明、维护形式证明方面极其擅长。De Moura 举了一个例子:

昨天我在改东西。我想出于技术原因修改一些证明,我甚至不知道那些证明是关于什么的。是别人写的。然后我说:“听着,我想让你把这些证明改写为不使用这个特性,因为我要改它,我不想破坏库。”瞬间就搞定了。它给我生成了新的证明。

这非常关键,因为否则维护证明的工作量会让形式验证难以主流化。

几乎就像如果你的程序花费 x 时间,过去做形式验证需要 10 倍时间。那很正常。但想象如果你的程序一直在变化,这是很常见的事情,现在你还得不断维护证明。这是很多工作。但 AI 为我们消除了这种痛苦。

Lean 作为编程语言

主持人注意到 Lean 被称为“证明助手”,但 de Moura 也说它是编程语言。主持人问:证明助手通常同时是编程语言和证明助手吗?

De Moura 回答:有些,尤其是那些基于依赖类型理论的,它们既是编程语言也是证明助手。在 Lean 中,你可以写定义,就像数学中定义概念一样,但有些定义可以是程序。Lean 是一种函数式编程语言,接近 Haskell,但还支持证明。

Lean 本身用 Lean 实现

Lean 的第一个大用例是 Lean 自己。

• 很多工具是用 Lean 实现的,例如名为 Vers 的文档编写系统。
• 构建系统叫 Lake(类似 Lean 的 make),也是用 Lean 实现的。
• 在 AWS,有一个用于 AI 加速器的编译器,是五十万行 Lean,主要选择 Lean 作为这个项目的编程语言。

De Moura 说,在这种情况下,证明就像副产品:“你可以得到证明,并在设计中发现问题的好处。”

证明助手的工具链是什么样?

大多数人熟悉编程语言和它们的工具链。主持人问:一个证明助手需要哪些主要组件?

De Moura 说,工具方面并没有太大不同。比如 Lake 就像是 Lean 的 Cargo。你会以同样的方式打开 VS Code,得到所有智能提示。

一个很大的区别是 Lean 中的 **信息视图(