A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
本文提出了一条健全且经内核验证的验证流水线，该流水线集成了 Rust 到 Lean 的提取工具、形式化密码学库以及人工智能证明器，成功为以太坊基金会 zkEVM 项目中的生产级 Rust 密码学代码生成了机器验证的正确性证明。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你拥有一家高风险工厂，专门为一座庞大、无形的金库（零知识虚拟机）制造数字密钥。如果这家工厂中哪怕有一个微小的齿轮略微弯曲，整个金库的安全性就会受到破坏，而无人会在为时已晚之前察觉。
多年来，检查这些齿轮就像聘请一支专家机械师团队，手工检查每一颗螺栓。这种方法既缓慢又昂贵，并且依赖于机械师不会遗漏任何细节。
本文描述了一条全新的自动化装配线，它能完成三件事：
- 翻译：将工厂的蓝图（用一种名为 Rust 的复杂语言编写）转化为一种通用的数学语言（Lean 4），使计算机能够完美理解。
- 提供：一个完美的、预先写好的“黄金标准”，说明机器应当如何运作（使用名为 ArkLib 和 CompPoly 的库）。
- 聘请一位超级智能的 AI 助手（名为 Aleph 和 Aristotle），将翻译后的蓝图与黄金标准进行比对，并撰写证明它们匹配的证明。
以下是该流程的运作方式，使用简单的类比说明：
1. 翻译器（从 Rust 到 Lean）
工厂的蓝图是用 Rust 编写的，这是一种工程师们喜爱用于构建快速、安全软件的语言。然而，“数学法官”（Lean 4 系统）不懂 Rust；它们只讲纯粹的数学。
本文使用名为 Aeneas 和 Hax 的工具作为翻译器。它们将 Rust 代码转换为“纯函数式”数学。
- 类比：想象将一份用厨师行话（Rust）写成的食谱，翻译成严格、逐步的化学公式（Lean）。翻译器还为每一步添加了“安全标签”。如果某一步可能失败（例如除以零或原料耗尽），翻译会清晰地标记出来，以便数学检查能够识别。
2. 黄金标准（规范）
除非你定义了什么是“正常工作”，否则无法证明机器是否有效。
- 类比：将 ArkLib 和 CompPoly 视为密码学的“官方规则手册”。它们包含了诸如“折叠纸张”（FRI 折叠）或“检查默克尔树”等事物在数学上应如何表现的完美、抽象定义。
- 目标是证明翻译后的 Rust 代码（工厂机器）所做的正是规则手册规定它应该做的，不多也不少。
3. AI 证明撰写者（“大脑”）
这是最令人兴奋的部分。一旦代码被翻译且规则手册准备就绪，你就需要撰写证明它们匹配的证明。传统上，这需要人类数学家来撰写证明，这就像解决一个巨大而复杂的拼图。
本文引入了 AI 证明器（Aleph 和 Aristotle）来承担繁重的工作。
- 类比：想象 AI 是一位不知疲倦、速度极快的侦探。你给它翻译后的蓝图和规则手册，它说：“我看到了联系！这是证明。”
- 关键安全检查：AI 不仅仅是声称它是正确的；它用 Lean Kernel（终极法官）能够阅读的语言撰写证明。Kernel 会检查 AI 逻辑的每一步。如果 AI 猜错了，Kernel 就会拒绝它。因此，AI 可以发挥创造力，但不能作弊。
他们实际做了什么
该团队将这一流程应用于 以太坊基金会 项目中使用的现实世界密码学代码（具体为 Plonky3 和 RISC Zero）。
- 成功之处：他们成功证明了代码的特定部分（例如计算如何折叠数据或检查树是否正确包含）在数学上是完美的。
- AI 的角色：在一个涉及名为
compute_log_arity_for_round的函数的具体示例中，AI（Aleph）自动撰写了两个复杂的证明，这些证明此前一直处于停滞状态（标记为"sorry"，意为“我们知道这是真的，但尚未证明”）。 - 人类的角色：AI 非常擅长处理逻辑谜题、“如果 - 那么”场景和基础数学。然而，它仍然需要人类来：
- 设计整体策略（即“规则手册”）。
- 处理复杂的循环（例如在重复序列中寻找正确的模式）。
- 修复翻译错误，即当 Rust 代码过于棘手以至于翻译器无法处理时。
小插曲（工程差距）
本文承认，这条装配线尚未完美。
- 版本不匹配：翻译器、规则手册和 AI 都使用数学语言中略有不同的“方言”。团队必须协调，使所有人使用同一版本。
- 翻译限制：一些复杂的 Rust 功能（如泛型类型或外部库）很难被翻译器转换。团队不得不将某些代码重写为更简单的“模型”，以便翻译器能够理解。
核心结论
本文并不声称 AI 已经取代了人类工程师。相反，它展示了一个 流程，其中：
- 人类翻译代码并设定目标。
- AI 充当强大的助手，撰写繁琐的逻辑证明。
- 严格的计算机法官（Kernel）验证一切以确保安全。
其结果是一个运作的系统，它将生产级的密码学代码转化为机器检查的、数学上保证的证明，使这座“无形金库”变得更加安全。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。