【Show HN】ZK回路最適化の革命児「ZkGolf」が登場！LLM×形式検証で最強の証明を生成せよ

ゼロ知識証明（ZKP）は、入力データを検証者に明かすことなく、計算が正しく実行されたことを証明できる強力な技術です。しかし、証明を行うには計算を「回路（有限体上の多項式制約のシステム）」として表現しなければなりません。この回路はZKにおけるアセンブリ言語のようなもので、制約が増えるごとにプルーバー（証明者）やベリファイア（検証者）に多大な負荷がかかるため、現場では手作業による過酷な最適化が行われてきました。私たちはここ数ヶ月、LLMを活用して「形式仕様から回路を生成する」という実験を行ってきました。LLMが実装の正当性を自ら証明できるのであれば、回路作成を自動化できるはずだと考えたのです。まずはSHA-256から着手しました。LeanでSHA-256圧縮の形式仕様を記述し、R1CS算術化と大きなフィールドをターゲットとして、LLMに回路を書かせることに成功しました。Claude 3 Opusは、多少の誘導こそ必要だったものの、数時間で実用的な実装を完成させました。さらに、制約数をコスト指標として回路を徹底的に最適化するよう指示したところ、驚くべき結果が得られました。LLMは最適化のアイデアを出し、実装し、それが健全性と完全性を満たしているか証明するプロセスを繰り返しました。誤った最適化を提案しても、証明が通らないと自ら軌道修正する姿には驚かされました。最終的に、人手による最高峰の最適化を凌駕する（非決定的な）SHA-256回路を生成できたのです。この成功体験から、最適化された検証済み回路を競い合い、ZKPの利用ハードルを下げて効率化を追求するオープンコンペティション「zk.golf」を立ち上げました。ぜひ皆さんも参加して、形式検証の奥深い世界を体験してください。詳細はこちら：https://zk.golf/llms.txt

一番乗りを目指して投稿してるよ。素晴らしいプロジェクトだね！