Show HN: zkGolf – Competitive optimization of formally verified circuits
zk.golfZero-Knowledge Proofs (ZKPs) let an untrusted proved show that computation was executed correctly without revealing the inputs to the verifier. However to prove anything, the computation first has to be expressed as a circuit: a system of polynomial equations (constraints) over a finite field. Circuits are the assembly language of zk and every constraint costs prover (and sometimes verifier) time, so production circuits are aggressively hand-optimized.
Over the last months, we have been experimenting with writing formal specifications instead and letting LLMs produce the circuits: as long as they could prove that their implementation was correct. It started with SHA-256: we hand wrote a specification in Lean for SHA-256 compression, and then we asked LLMs to write the circuit, targeting R1CS arithmetization and large fields.
It took a few hours of work for Opus 4.7, and some light steering into the right direction, but in the end the model came up with a reasonable implementation. We then asked the LLM to aggressively optimize the circuits, by driving down a cost metric of the circuit (number of constraints). We immediately got very promising results, just by asking to come up with optimization ideas, implement them and prove that the new circuit still satisfies soundness and completeness. Sometimes, it came up with unsound optimizations, however, since it could not prove them, it backtracked and got itself back on to the right approach.
The result was a (non-deterministic) circuit beating the current, human optimized, state of the art for SHA256 compression. This experience lead us to create "zk.golf" which is an open competition to produce optimized, formally verified circuits to lower the bar for the use of ZKPs and make their application more efficient.
Come play (https://zk.golf/llms.txt) and learn about formal verification.
Neat, but I feel like you need to define "circuit" on that page! I thought this was like for silicon design or something.
A matter of perspective. Anyone who works with SNARKs (ZK or otherwise) gets the terminology right away
Circuit is the standard term used for zero knowledge "programs"
this is super cool, didnt know zk circuits are really generalized version of all sorts of physical circuits
they're the same, arithmetic circuits are just made out of addition and multiplication gates. They're used all over the place in programmable cryptography (ZKP, FHE, MPC)
I'm racing to be the first submission, amazing project :)
I look forward to the coming era of human-optional formally verified programming competitions.
I wonder what other optimization+verification problems are out there that will make good LLM feedback loops.
Maybe something with query planners.
someone named "zrschresearch" is cheating. looks like they found a way to only measure cost on specific best case inputs where its trivially 0. its using a correct implementation so the proof checks out but the cost is obviously fake.
fixed!
Saw this earlier on LinkedIn and checked it out. Awesome initiative!
So... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?
In a world where llms read everything… every human contribution is a fishing expedition. At least here humans are trying to push a very hard frontier that llms arent good at yet.