Show HN: zkGolf – 正式验证电路的竞争性优化

零知识证明（ZKPs）允许不受信任的证明者向验证者证明计算已正确执行，而无需透露输入信息。 然而，要证明任何内容，首先需要将计算表示为电路：有限域上的多项式方程（约束）系统。 电路是零知识证明的汇编语言，每个约束都会消耗证明者（有时也包括验证者）的时间，因此生产级电路会进行大量手动优化。<p>在过去的几个月里，我们一直在尝试编写形式化规范，并让大型语言模型（LLMs）生成电路：只要它们能够证明其实现是正确的。 我们从 SHA-256 开始：我们手动用 Lean 编写了 SHA-256 压缩的规范，然后要求 LLMs 编写电路，目标为 R1CS 算术化和大域。<p>Opus 4.7 花了几个小时的工作，并进行了一些轻微的引导，但最终模型提出了一个合理的实现。然后我们要求 LLM 积极优化电路，通过降低电路的成本指标（约束数量）。仅仅通过要求它提出优化想法、实现它们并证明新电路仍然满足可靠性和完备性，我们立即得到了非常有希望的结果。有时，它会提出不合理的优化，但由于无法证明它们，它就会回溯并重新回到正确的方法上。<p>结果是一个（非确定性）电路，击败了当前人工优化的 SHA256 压缩的最先进水平。这一经历促使我们创建了“zk.golf”，这是一个开放竞赛，旨在生成经过优化的、正式验证的电路，以降低使用零知识证明的门槛，并使其应用更高效。<p>快来参与（<a href="https:&#x2F;&#x2F;zk.golf&#x2F;llms.txt" rel="nofollow">https:&#x2F;&#x2F;zk.golf&#x2F;llms.txt</a>）并了解形式化验证吧。