终极保证：形式化验证

AI模型价格对比 | AI工具导航 | ONNX模型库 | Vibe Coding教程 | PLC在线仿真器 | Tripo 3D | Meshy AI | ElevenLabs | KlingAI | ArtSpace | Phot.AI | InVideo

对于生活的大多数领域，答案似乎是否定的。例如，我们关于物理世界的所有知识都来自使用人类感官和科学仪器对其进行的观察。但人类感官是有缺陷的（即使你看到面前的东西，它可能只是视觉错觉）。即使最精确的科学仪器也有一些测量错误或捕获噪音的可能性，从而导致误差。每当从外部世界推断时，无论多么小，这些推断都可能基于完全错误的输入。而且即使你能以某种方式确保所有数据都是准确的，进行因果推断也是一个混乱且有些主观的过程。两位科学家可能拥有完全相同的信息，但仍然对信息的解释存在分歧。

人们可能希望通过退回到抽象逻辑和数学的世界来避免这些难题。在那里，你可以纯粹从公理进行推理，而不必从外部世界获取任何可能损坏的观察。因此，人们认为没有出错的余地。但事实真的如此吗？毫无疑问，逻辑和数学可以产生比任何其他科学分支更高的准确性，但即使它们也可能受到争议。

尽管现代数学家很少对证明是否有效存在分歧，但并非闻所未闻。例如，从2000年代开始，日本数学家望月新一开发了他所谓的跨宇宙泰希米勒理论，并用它证明了数论中一些长期存在的猜想。问题在于，全球数学界的大多数人都不相信望月，他的理论被望月的一小群追随者之外的所有人摒弃。直到今天，没有数学家能够明确证明或证伪该理论。

这是怎么可能的？数学应该是清晰明确的，不受人类任意判断的影响。数学陈述要么为真，要么为假。那么，为什么领先的数学家对此存在分歧呢？问题在于，即使是高级数学证明也大多用自然语言书写，而不是纯粹的逻辑或代码。但众所周知，自然语言是模糊的，可以有不同的解释。一个数学家认为明显的含义——如此明显以至于不需要证明——另一个数学家可能认为是需要冗长解释的无法容忍的逻辑跳跃。这个问题在数学的更高级阶段变得更加尖锐。随着理解一个领域所需的背景信息增加，能够阅读该领域证明并确定这些证明是否准确的人就会减少。如果只有少数数学家能理解特定领域正在写的内容，那么我们其他人就只能相信那些数学家正在准确诚实地工作。

有一种纯粹逻辑的语言可以用来代替自然语言，这样读者就可以立即判断一个论点是否为真，无论他们是否理解该论点，这将是很方便的。确实，这样的语言确实存在：它们被称为形式化验证语言。这些语言与其他编程语言的区别在于，它们都包含一个证明检查内核。当你运行内核来检查证明的有效性时，它总是会停止——这意味着它总是会验证（如果证明有效）或抛出错误（如果无效）。这不像Python，程序可能导致无限循环。除了上帝亲自降临地球告诉我们一个陈述是真的之外，像Lean这样的语言中的形式化证明是我们凡人能够接近绝对确定性的最接近的东西。

但即使这一声明也有一些注意事项：

首先，虽然"Lean中可证明的每个陈述都是真的"可能是一个真实的陈述，但反之则肯定不是。也就是说，"每个真实的陈述在Lean中都可证明"是一个错误的陈述。这是因为任何能够表达初等算术的一致形式系统都包含在该系统内无法证明或证伪的真实陈述。（这是哥德尔第一不完备性定理。）

其次，即使是形式化证明也不是纯粹的、100%的真实性保证。总是有一些可能性，无论多么小，形式化验证语言本身包含错误。也有可能，无论多么不可能，每台运行该语言的计算机同时出现故障并显示错误答案。没有机器，包括形式化语言，能够证明自身的一致性。（这是哥德尔第二不完备性定理。）所以虽然形式化证明可以使错误的可能性任意小，但它永远不能达到完全为零。

好吧，但抛开注意事项不谈，形式化证明仍然相当强大。它们可以将数学过程从"我相信这是真的，因为一位有信誉的数学家说这是真的"转变为"我相信这是真的，因为人类已知最强大的软件已验证这是真的"。那么问题就变成了：如果形式化证明如此伟大，那么我们为什么不一直使用它们？为什么数学家仍然主要用自然语言书写？

1、数学中形式化证明的简史

几个世纪以来，数学家一直梦想着让他们的领域更加严谨。例如，在17世纪，戈特弗里德·威廉·莱布尼茨提出了characteristica universalis（通用特征）的概念，这是一种通用符号语言，与calculus ratiocinator（推理演算）配对，这是一种机械化程序，用于立即筛选在characteristica universalis中做出的陈述并确定其准确性。第一个在构建此类系统方面取得重大进展的数学家是戈特洛布·弗雷格，他的Begriffsschrift最初于1879年出版。但弗雷格最初的公式有一些严重的错误。最重要的是：弗雷格声称每个正式定义的集合都必须存在，但我们可以正式定义"不包含自身的集合"的集合。由于无法说明此集合是否包含自身，我们有一个矛盾。（这是罗素悖论。）

弗雷格的Begriffsschrift被击败之后，世界领先的数学家（伯特兰·罗素、阿尔弗雷德·诺思·怀特海德、朱塞佩·皮亚诺、大卫·希尔伯特和L.E.J.布劳威尔等）之间进行了数十年的辩论，讨论如何构建元数学领域。他们试图回答这样的问题：什么是数学陈述，我们如何才能知道它是否为真？什么是集合，我们如何判断两个集合是否相等？我们应该依赖什么起始公理来推导其余的数学？而且，对于本文的目的最重要的是：在书写逻辑陈述时，什么是合适的语言？正是在这个时代，我们得到了许多至今仍在使用的最著名的数学符号，如"∈"表示集合成员关系，"∃"表示"存在"，"∀"表示"对于所有"。

到1930年代末，这些元数学辩论大多得到了解决，从而为数学和计算机科学提供了坚实的理论基础。尽管如此，形式化数学证明从理论可能性到数学家经常做的事情又花了数十年时间。20世纪中叶的计算机仍然庞大、笨重、昂贵且容易出错，因此，除了领先研究团队中少数非常有远见的数学家之外，几乎没有理由使用基于计算机的形式化证明而不是更传统的自然语言证明。

计算机用于形式化证明的首次记录使用来自1956年的兰德公司团队，他们使用"逻辑理论家"计算机程序证明了罗素的《数学原理》第二章中前52个定理中的38个。大约在同一时间，几位数学家汇聚在柯里-霍华德对应上，该对应建立了计算机程序和数学证明之间的联系。到1960年代末，荷兰组合数学家尼古拉斯·戈弗特·德布鲁因利用这种对应关系创建了他自己的程序Automath。Automath可以被认为是第一个真正的现代证明助手；它能够形式化整本教科书的结果。1984年，受Automath启发，法国数学家蒂埃里·科昂和热拉尔·于埃开发了构造演算。这个高度表达的形式系统构成了Coq形式化证明语言（最近重命名为Rocq）的理论基础，该语言至今仍是最广泛使用的定理证明器之一。自1980年代以来，世界各地的数学家团队已经创建了数十种不同的形式化证明语言和助手，每种都对应于略微不同的证明风格和计算需求。

然而，值得注意的是，这些形式化证明绝大多数用于验证人类数学家已知的结果，而不是从头开始发现新结果。直到今天，大多数数学家并不经常使用形式化证明，绝大多数新的数学研究都是用自然语言而不是形式化符号语言发表的。（在这里说句题外话：我最近完成了我的本科数学学位，在我大学的数学系，完全没有教授形式化证明技术。我关于形式化证明的所有知识都来自自学，我可能比我的教授更擅长写基于Lean的证明。）

为什么？如果我们知道形式化证明比自然语言证明在逻辑上更严谨、更不容易出错，为什么领先的数学家仍然使用后者而不是前者？部分原因很简单，是惯性和传统主义，加上不愿意经历用形式化语言书写所需的陡峭学习曲线。但还有更深层次的因素在起作用。有两个因素特别使形式化证明在数学界相对不受欢迎/未被充分利用：

首先，计算机的工作方式与人类思维非常不同，这意味着计算机可读的证明通常对人类来说是不可读的。计算机每秒可以处理数百、数千甚至数百万个案例，而人类工作非常缓慢，并且在给定时间只能在脑海中保存相对较少的案例。因此，对机器来说直观的证明可能对人类来说完全不透明。以阿佩尔和哈肯著名的1976年四色定理证明为例。该定理指出，任何地图都可以用四种或更少的颜色填充，使得没有两个相邻的形状共享相同的颜色。

为了证明这一点，他们首先使用计算机程序证明每个地图都可以简化为数千种可能配置之一。然后，他们使用同一个计算机程序证明数千种配置中没有一种是有效的反例。该证明在发表时非常有争议。没有人否认计算机的结果是准确的，但许多数学家觉得这是作弊。他们认为，数学的部分之美在于建立直觉和寻找优雅的规则来解释我们的世界，而不是由机器重复检查数千个案例。如今，大多数数学家已经接受四色定理是有效的，但他们仍然更喜欢在可能的情况下用自然语言证明而不是形式化证明。如果研究论文的目标是与其他人交流思想，那么用其他人实际上可以阅读的自然语言书写该论文是有意义的。

形式化证明相对少见的第二个原因是它们比自然语言证明更难写、更乏味。如果你曾经尝试过像我一样手工写形式化证明，你会很快意识到需要多少额外的工作。例如，像"(x + 2) - 2 = x"这样的陈述对人类来说似乎是显而易见的，如此明显以至于不需要证明。但对于形式化证明机器来说，没有陈述可以在没有证明的情况下被断言，所以形式化证明编写者必须花费大量时间验证平凡的结果。

这就是人工智能影响最大的地方。人类数学家不再需要手动筛选数千个公理和定理来寻找他们想要的结果。相反，你可以将你的陈述插入AI模型，它将在验证语言中搜索所有已知结果的库，以找到并应用与你的证明最相关的定理。通过人工智能，形式化验证已知结果的过程可以从几乎不可能变为几乎微不足道。

尽管最初并非为AI设计，但名为Lean的证明助手由于其易于AI集成，在形式化证明社区中变得非常受欢迎。使用Lean而不是竞争对手证明助手的主要好处是它的"mathlib"定理库，AI代理可以轻松搜索。而且，正如AI可以帮助推进形式化证明的状态一样，形式化证明也可以帮助推进AI的状态。用形式化语言编写的数学定理已被证明是现代AI系统的宝贵数据源，因为与大多数人类生成的数据不同，我们确切知道这些定理是准确的。这解释了为什么谷歌的AlphaProof模型（主要在Lean仓库上训练）能够在2024年国际数学奥林匹克竞赛中获得银牌。

早期的LLM浪潮，从2017年到2024年左右，适度增加了形式化证明的使用。但直到最近，AI聊天机器人在形式化证明方面仍然非常有限，因为它们仍然太容易产生幻觉，上下文窗口太短，并且容易陷入无成效的研究方向。但过去2年该领域发生了真正的革命。随着Claude Code等现代AI代理的出现，形式化证明现在广泛可及，甚至对像我这样的业余自学者也是如此。陶哲轩，当今最著名和最受尊敬的数学家，已成为使用AI辅助形式化证明进行数学研究的积极倡导者。过去一年，新的数学发现速度惊人增长，通常以形式化方式书写。至少12个开放的埃尔德什猜想已被AI解决；就在本月，一个OpenAI模型能够证伪他关于单位距离问题的最著名猜想之一。

形式化证明的下一个前沿似乎是自动形式化：是否有办法获取任意的自然语言证明，并自动将其转换为严格的形式化证明？已经有几家公司和研究小组以实现这一目标为宗旨而出现，到目前为止结果令人鼓舞。例如，问题陈述的自动形式化接近成为已解决的问题：早在2024年，研究人员就能够创建一个模型，在测试问题陈述的形式化方面准确率超过93%。（形式化问题陈述比形式化整个证明更容易，但它仍然令人印象深刻。）我们可能很快就会进入一个前所未有的时代，所有数学知识都经过形式化验证。

2、从形式化证明到形式化验证

你可能想知道这有什么关系。当然，我们现在可以更准确地验证数学结果，但这如何应用于现实世界？

形式化证明很重要，因为不仅仅数学定理可以被形式化验证：理论上，我们可以形式化验证任何硬件或软件，以证明它具有我们想要的属性。这对安全具有重大影响，无论是在私人还是政府层面。传统的非形式化程序测试方法依赖于人工审查、经验结果和模糊测试（向软件抛出大量可能的输入，看看其中是否导致错误）的组合。问题在于人工审查容易出错，即使软件通过了所有测试，这仍然不是准确性的完全保证。正如荷兰计算机科学家艾兹格·迪科斯彻所说，"程序测试可用于显示错误的存在，但永远不能显示它们的不存在！"

相比之下，形式化验证可以两者兼顾。举一个简化的例子：假设你正在运行一个网站，你需要编写一个软件程序，只有在用户输入正确密码时才允许他们进入帐户。那么理论上，你可以打开形式化验证引擎，输入你的代码，然后输入语句"用户的帐户页面将打开当且仅当用户输入正确的密码。"如果引擎编译通过，那么你将确定你的软件具有你想要的属性。否则，你将知道存在潜在错误。

迄今为止，形式化验证在现实世界中应用的最重要示例可能是亚马逊。自2011年以来，亚马逊网络服务使用形式化方法来验证其内部软件系统。正如公司报告所述，"形式化方法在AWS取得了巨大成功，帮助我们防止微妙但严重的错误到达生产环境，这些错误我们不会通过任何其他技术发现。它们帮助我们设计了复杂算法的激进优化，而没有牺牲质量。"

在需要绝对确定性的国防等关键领域，没有替代品可以让软件经过形式化验证。因此，美国国家安全界对这项技术产生了浓厚兴趣：

DARPA弹性软件系统研讨会的重播，于2025年6月17日在弗吉尼亚州阿灵顿举行，现在可以在该机构的YouTube页面上观看。

该活动召集了来自国防部（DOD）、国防工业、美国政府、盟国、学术界和形式化方法开发者的300多名参与者。它标志着推进DARPA催化广泛采用形式化方法目标的关键时刻，这些数学上严格的技术可以显著提高软件系统的安全性和可靠性。

"在DARPA，我们全力以赴，要求高风险/高回报的研究，目标是提供关键的抵消，使国家安全格局朝着有利于我们的方向发展，"DARPA副主任Rob McHenry说。"我们投资组合中有很多很棒的赌注，但我相信弹性软件系统计划最有可能成为DARPA十年的影响力。"[...]

"我们的目标是翻转你们每个人头脑中的一位，"McHenry说。"接受网络漏洞风险已经不再是可以接受的了。我们知道如何做得更好。我们都必须做得更好。今天是网络漏洞时代的最后一天。"

直到最近，像这样的声明会被认为是荒谬的、天方夜谭式的理想主义。前AI时代的形式化验证如此缓慢、昂贵和乏味，以至于即使在纯数学家之中也很少见。对于大多数公司或政府机构来说，形式化验证所有软件完全是不切实际的。但现在，AI为我们提供了部署完全针对漏洞进行验证的软件的机会。

而且，与许多其他网络能力的增强不同，形式化验证不对称地有利于防御者。这是因为，一旦一个软件或硬件经过形式化验证，它就是为使用该系统的每个人验证的。对数学陈述的真假有更多确定性意味着有更多工具可供善用者使用，而更少的混乱可能被恶意利用者利用。

当然，我们应该注意局限性。形式化验证中的一个显著问题是规约问题：自然语言版本的陈述和该陈述的技术版本之间可能存在差异。用自然语言陈述的主张可能是模糊的或不清楚的，甚至是对于做出陈述的人。可能发生的情况是，形式化验证引擎"证明"了一个主张，但它实际证明的主张与说话者意图的主张微妙地不同。因此，使用形式化验证的组织可能意外地验证了错误的主张，从而陷入虚假的安全感。有些陈述本质上是主观的，使得客观规约不可能。例如，如果你想验证AI模型永远不会伤害无辜的人的主张，你需要找到某种方式来严格指定你所说的"伤害"、"无辜"和"人"的意思。即使在所有数学都经过形式化验证的世界中，规约问题仍然需要大量工作才能正确完成。

此外，软件只是集成安全系统的众多方面之一。即使拥有完全安全的软件，攻击者仍然可以入侵易受攻击的硬件，或者对易受攻击的人类操作员进行网络钓鱼攻击。

然而，即使有限制，这些技术仍然可以完成很多工作。政策制定者和慈善家应该利用AI辅助形式化方法提供的前所未有的机会，大力投资形式化验证我们的软件和硬件系统。

3、形式化验证的慈善方法

我不是第一个提出雄心勃勃的议程来促进形式化验证研究的人。去年，数学家帕特里克·沙夫托为进步研究所撰写了一篇名为《无限项目》的提案：

无限项目是一个1.125亿美元的拨款竞赛，在数学研究所之间进行。该项目利用AI翻译和计算机编程的进步，在五年内形式化整个数学领域，为任何人自动产生和验证数学证明创建基础设施。

具体来说，沙夫托写道，该项目将：

建立形式化和自然语言数学库。 自然数学陈述必须由人类专家手动翻译成能够进行形式化验证的计算机程序（如Lean）中的等效陈述。手动翻译对于促进AI系统在数学中的训练以及确保与人类数学实践的联系是必要的。这可以通过专家以分散的方式实现，由牵头研究所组织的中央协调委员会协调。

进一步生成形式化数学。 AI辅助将很重要，因此模型可以加速数学的形式化，并将形式化数学反向翻译成自然语言数学。正确性可以通过计算机程序的形式化验证来确保。这将极大地加速数学的形式化和用于训练AI代理的高质量数据。

开发数学增强AI代理。 以数学为中心的AI代理将在形式化和自然语言数学库上进行训练，以自动生成新的数学。关键挑战在于数学不仅要是真的，还要引入有助于解决其他数学问题的有用概念。引入新的、有用的概念的能力对于扩大数学在各个领域的可访问性和有用性尤为重要。

展示对科学、技术和社会的影响。 将开发演示来说明数学和AI的变革性影响。科学流程（如生物学中的实验室工作）和计算机程序等技术对象的形式化将作为更广泛数学基础潜力的演示。将开发教程材料和外展计划，以促进教育和在整个经济和社会中的广泛采用。

沙夫托认为，仅靠私人产业不足以完成如此规模的项目。虽然一些私人机构可能有动力为自己运行狭隘的形式化验证程序（如上面提到的AWS案例），但数学知识通常是一种公共利益，其好处广泛分散。此外，沙夫托认为，这种倡议需要社会、学术界和行业之间只有政府才能实现的协调水平。

虽然我希望看到美国政府支持的无限项目来促进形式化验证，但我怀疑这样的政府项目会很快发生。本届政府已经削减了现有国家科学基金会项目的资金，因此我怀疑它会愿意支持像这样更雄心勃勃的科学项目。这意味着联邦资助的无限项目最早不太可能在2029年之前发生。我不想等那么久，幸运的是，我认为我们不必等。

尽管美国政府可能不愿意支持无限项目，但私人产业和慈善事业可能愿意。AI界最近一直在热议即将到来的"美国慈善事业的第三波浪潮"：如果AI真的即将像科技界认为的那样创造大量利润，那么一群AI高管和工程师突然会有大量现金，在许多情况下比他们知道如何使用的还要多。已经有一些基于硅谷的资助者，如Coefficient Giving，报告说他们手头的钱比他们想要花的令人兴奋的项目还要多。一个可以轻松吸引和吸收新富科技慈善家资金的项目就是促进形式化验证的项目。

我的提议很简单：慈善家应该支付由AI代理协助的人类数学家团队，来形式化验证数学和计算机科学中的现有结果。专注于可能产生最积极外部性但不服务于任何直接市场功能的结果。如果形式化证明最终产生了新的定理/引理，应该支付数学家将这些新定理翻译回自然语言。如果沙夫托的提议是现实的——即仅需1.125亿美元的预算，我们就可以雇佣足够的研究人员在五年内形式化整个数学领域——那么它完全在足够有动力的慈善家的能力范围内。真的：如果你是亿万富翁或超级富豪，你现在就可以让这件事发生。

我支持的另一种方法是使用基于市场的机制，如赏金系统。慈善家可以为他们想要形式化验证的数学领域、特定定理或特定软件设置赏金。第一个能够形式化验证（或形式化证伪）该领域/结果的人或团体将获得赏金。

这种基于慈善的系统有几个好处：通过不依赖政府资助，我们可以立即开始，避免不得不依赖华盛顿政策制定者的突发奇想。政府和学术界的研究可能相当缓慢；它可能无法与AI进步的速度相匹配，这在网络安全和硬件安全等时间敏感领域尤其相关。相比之下，赏金系统可以为公众利益释放硅谷的速度和效率。

慈善/私人主导的无限项目所缺乏的是沙夫托原始、政府主导提案中的那种协调或中央自上而下的结构。我将此视为一个特性，而不是一个错误。数学作为一个整体，特别是形式化证明社区，在分散和自下而上的情况下运作得非常出色。世界上许多最先进的、使用最广泛的开源库都是由成千上万的无偿志愿者建立和维护的，除了增加人类知识和改进世界软件的愿望之外，没有任何共同的隶属关系。我不相信政府参与对于让数学家相互协调是必要的。

4、结束语

形式化验证在数学界已经讨论了近100年，但只是现在，随着人工智能的最新进展，形式化验证才变得可以大规模实施。我们有可能在未来五年内形式化整个数学领域。

这也正是时候，因为对它的需求从未如此之大。每天，AI都在创造网络安全和物理安全的新风险，无论是AI代理对恶意人类行为者的赋能、AI模型权重对破坏或盗窃的脆弱性，还是AI模型本身的不一致。我不指望形式化验证能够单独解决所有或大部分这些问题。但它是防御者工具包中的另一个工具，与其他安全技术一起，有可能大幅提高AI安全。

我敦促政策制定者和慈善家投资这一研究方向。需求从未如此紧迫，潜在收益从未如此巨大。

原文链接: The Ultimate Guarantee: Formal Verification

汇智网翻译整理，转载请标明出处