zk.golf：电路的无畏协作优化

今天我们发布了 zk.golf，这是一个让人们在特定问题上创建最高效的 zk 电路的竞技平台。它融合了两个强大的理念：

• 借助 Clean，我们能够使用机器可验证的证明来认证电路的正确性。
• 借助前沿的 AI 模型，我们能够在几天内获得深度优化的电路及其配套证明。

我们称之为 zk 电路的无畏优化。

我们是如何走到这里的

过去几个月，我们一直在尝试让 LLM 编写电路，前提是它们能够证明自己的实现是正确的。最初从 SHA-256 开始：我们在 Lean 中手写了一个 SHA-256 压缩函数的规范，然后让 LLM 针对 R1CS 算术化和大域编写电路。Opus 4.7 花了几个晚上，并稍微往正确的方向引导了一下，但最终模型给出了一个合理的实现。

神奇之处在于，我们实际上不必检查电路是否正确。由于电路是用 Clean 实现的，Opus 4.7 同时提供了针对我们编写并信任的手写规范的可靠性证明和完备性证明。

过了一段时间，我们让 LLM 根据给定的成本指标积极优化电路。只需让它们提出优化思路、实现这些思路并证明新电路仍然满足可靠性和完备性，我们就立刻得到了非常有希望的结果。有时它会提出不可靠的优化，但由于无法证明这些优化，它会回溯并重新回到正确的方法上。

Lean 内核和 Clean 定理很高兴，我们也很高兴。

一种天然的不对称性

想一想 RSA 签名验证：该算法可以用几行代码写出来——它只是整数模幂运算，加上一些简单的填充检查。然而，实现此功能的电路往往极其复杂，主要在于大整数算术的实现方式以及使其高效的各种技巧。

在 zkSecurity，我们审查过许多这样的电路：对人类来说，跟踪不同组件之间的范围、假设和关系确实很难。但大多数时候，正确性推理是乏味且无趣的：它涉及简单的等式重写、范围分析，有时还有多项式求值推理。

这正是 LLM 非常擅长的证明类型：它们会乐于为我们处理无聊的边界分析和等式重写，而且由于它们无法欺骗定理证明器，我们可以信任它们完美地完成这项工作。这就是为什么形式化验证与 LLM 的结合异常强大，因为它们恰好互补：LLM 不可信，但非常愿意做任何数量的工作；另一方面，定理证明器可信，但要求大量的工作。结果是，之前需要数年的形式化工作，现在可以在几天内完成。

请给我正确的电路！

在 Clean 早期，我们有一个区别于其他 zk 形式化框架的标志性特征：我们希望在证明可靠性的同时也证明完备性。当时我们并未意识到，但这恰恰是允许不受信任的用户（尤其是 LLM）为我们编写和优化电路的特性。

如果我们要求 LLM 优化任何电路，并且只要求可靠性，输出会令人惊讶：它将是最廉价的不可满足的电路。在 R1CS 中，这可能只是一个只有一个线性约束的电路，强制常数 1 线等于零。这是因为不可满足的电路对于任何规范都是可靠的：证明者永远无法让验证者相信一个错误的声明，因为他们无法让验证者相信任何东西！

通过要求可靠性和完备性，我们正好从正确的相反方向确定了正确的电路。

编译器呢？

有人可能会说，我们已经有了自动电路优化的工具：它们叫做优化编译器。例如，Circom 编译器会执行许多有用的优化，如删除冗余变量和优化掉线性约束。

正如《软件开发的最终形态》所指出的那样，直接使用低级语言编写要强大得多：

• 我们能够消除对编译器正确性的信任假设，转而依赖约束满足这一微小的语义核心。
• 即使编译器经过形式化验证，我们也能够进行针对问题的特定优化。编译器只能进行通用优化，而在 zk 电路中，如果我们追求激进优化，这些通用优化往往是不够的。

从某种意义上说，LLM + 交互式定理证明器就是一个非常聪明且非常昂贵的优化编译器：将高级规范（例如验证 RSA 签名的简单程序）转换为复杂的低级描述（例如 zk 电路）。

规范，而非电路

我们越来越坚信，任何人都不应该再去看约束了：约束是编写 zk 电路的最底层，虽然它们精确描述了底层证明系统所做的断言，但它们并不是人类可审计的最佳语言。使用本文描述的方法，我们可以跳过对约束的审查，直接审查 Lean 规范。

当然，规范像所有代码一样可能存在错误，但审查规范要容易得多：规范不是优化实现，可以用最自然的方式来表达计算，例如使用任意精度整数进行模运算。这大大增强了我们对所编写和部署的电路的信心，同时也显著降低了入门门槛：从业者可以像用任何常规编程语言编写程序一样轻松地编写规范，然后让 LLM 使用 Clean 将其自信地转换为优化的电路实现。

什么是 zk.golf

到目前为止，本文只是一些随意的想法和观点。那么，我们到底构建了什么？

zk.golf 是一个平台，允许用户竞争为给定的“形式化接口”创建最高效的电路。电路的接口定义了电路的所有有趣属性，由以下部分组成：

• 输入和输出类型。
• 对输入的假设，这些假设需要在其他地方（例如由调用者）检查（有时称为前置条件）。
• 规范，即电路提供的保证（有时称为后置条件）。

对于每个挑战，我们都编写了一个形式化接口，我们相信它代表了有趣且现实世界的问题。用户可以提交任意电路，只要他们提供机器可检查的 Lean 证明，证明他们的电路满足该接口。我们使用 comparator 验证 Lean 证明。

由于 Clean 支持查表和高次约束，用户还需要证明他们的电路是 R1CS，并且提供电路的成本证明。两个成本指标是分配数量和约束数量。目前，我们根据分配和约束的总和对提交进行评分，并且我们以 BN254 素域为目标。

参与进来

如果你认为自己可以超越 zk 电路的当前水平，请访问 zk.golf，选择一个挑战并开始优化。我们还为 LLM 编写了一些指导，以便它们自主地为你执行优化和提交：只需创建一个 API 密钥，并将你的 agent 指向 llms.txt。即使你从未接触过形式化验证或 Clean，这也是一个非常简单的入门方式，可以看看一些简单但真实的规范/形式化验证示例。你只需引导你的 agent 使用正确的技术和工具，就可以优化电路。

我们将在未来几周内添加更多挑战，最终目标是提供一套高度优化、经过形式化验证的 zk 电路库，供整个社区使用。

我们期待在排行榜上看到各位！

zkSecurity 为密码学系统（包括零知识证明、MPC、FHE、共识协议等）提供审计、研究和开发服务。

• 原文链接： blog.zksecurity.xyz/post...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～