Show HN: zkGolf、形式検証済みサーキットの競争的最適化

ゼロ知識証明（ZKP）により、信頼できない証明者が、入力情報を検証者に明かすことなく、計算が正しく実行されたことを示すことができます。 しかし、何かを証明するためには、まず計算をサーキットとして表現する必要があります。これは、有限体上の多項式方程式（制約）のシステムです。 サーキットはZKPのアセンブリ言語であり、各制約は証明者（そして時には検証者）に時間的コストがかかるため、プロダクションサーキットは積極的に手作業で最適化されています。 ここ数ヶ月、私たちは形式仕様を記述し、LLMにサーキットを生成させるという実験を行ってきました。その実装が正しいことを証明できる限りにおいてです。これはSHA-256から始まりました。私たちはSHA-256圧縮のためにLeanで仕様を手書きし、次にLLMにR1CS算術化と大きなフィールドをターゲットとしたサーキットを書くように依頼しました。 Opus 4.7では数時間の作業と、正しい方向への軽い誘導で、モデルは妥当な実装を考案しました。その後、私たちはLLMに、サーキットのコスト指標（制約数）を下げることによって、サーキットを積極的に最適化するように依頼しました。最適化のアイデアを出し、それを実装し、新しいサーキットが健全性と完全性を満たしていることを証明するように依頼しただけで、すぐに非常に有望な結果が得られました。時には、健全でない最適化を考案することもありましたが、証明できなかったため、後退して正しいアプローチに戻りました。 その結果、SHA256圧縮における現在の人間による最適化された最先端技術を上回る（非決定的な）サーキットが生まれました。この経験から、私たちは「zk.golf」を創設しました。これは、最適化され、形式検証されたサーキットを作成し、ZKPの利用の敷居を下げ、その応用をより効率的にするためのオープンコンペティションです。 ぜひ参加して（https://zk.golf/llms.txt）、形式検証について学んでください。