Birbla

Discussion summary

zkGolf is a project focused on optimizing formally verified circuits, with discussions on dataset collection, verification methods, and terminology. Participants express interest and clarify concepts related to circuits and their applications.

What the discussion says

  • Some see it as a hard frontier for LLMs to assist with.
  • Concerns about cheating in cost measurement methods.
  • Enthusiasm for the project's potential and future competitions.
  • Clarification that circuits refer to arithmetic circuits used in cryptography.
“Every human contribution is a fishing expedition.”
— chews
“Looking forward to human-optional verified programming competitions.”
— pvillano

Comments

Hacker News

So... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?

by rirze

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.

by chews

Saw this earlier on LinkedIn and checked it out. Awesome initiative!

by TheFirstNubian

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.

by tancop

fixed!

by baby

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.

by pvillano

I'm racing to be the first submission, amazing project :)

by baby

Neat, but I feel like you need to define "circuit" on that page! I thought this was like for silicon design or something.

by IshKebab

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)

by baby

Circuit is the standard term used for zero knowledge "programs"

by AtHeartEngineer

A matter of perspective. Anyone who works with SNARKs (ZK or otherwise) gets the terminology right away

by ludamad

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • So... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?
    by rirze
  • 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.
    by chews
  • Saw this earlier on LinkedIn and checked it out. Awesome initiative!
    by TheFirstNubian
  • 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.
    by tancop
  • fixed!
    by baby
  • 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.

    by pvillano
  • I'm racing to be the first submission, amazing project :)
    by baby
  • Neat, but I feel like you need to define "circuit" on that page! I thought this was like for silicon design or something.
    by IshKebab
  • 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)
    by baby
  • Circuit is the standard term used for zero knowledge "programs"
    by AtHeartEngineer
  • A matter of perspective. Anyone who works with SNARKs (ZK or otherwise) gets the terminology right away
    by ludamad

Related stories

Reducing Doom Loops with Final Token Preference Optimization

liquid.ai · 29 points · 9 comments

Decoding the obfuscated bash script on a Uniqlo t-shirt

tris.sherliker.net · 1072 points · 181 comments

StreetComplete: Fixing OpenStreetMap, one tiny quest at a time

streetcomplete.app · 761 points · 182 comments

Every new car sold in the European Union must include a driver monitoring camera

allaboutcookies.org · 737 points · 969 comments

Chat Control 1.0 and 2.0 Explained

fightchatcontrol.eu · 645 points · 238 comments

Microsoft fire idTech team at Id software

gamefromscratch.com · 597 points · 533 comments