Live data from Hacker News

Solving the Jane Street reverse engineering challenge

jestoph.com

71–80 of 85 posts

Re: Solving the Jane Street reverse engineering challenge

#71
post #68

I gave the problem to chatGPT 5.6 Sol Pro and this was the result: > Worked for 12m 36s > Solved https://chatgpt.com/s/t_6a9aed0b09988191b0f2850dee056b48 Edit: It didn't independently solve it. > 1. Used the public reconstruction to obtain the recovered RTL/constraint structure, including the 11×11 region map and the fact that it is a two-stars-per-row/column/region, non-touching puzzle. > 2. Then independently wrote…

Looks like it did not actually solve it, but instead it just found an existing solution at https://github.com/NotCleo/GDS-to-RTL and verified parts of it?

I have no doubt that modern agents can solve challenges like this even without external help, but you should at least briefly look at the output before posting it online!

Re: Solving the Jane Street reverse engineering challenge

#72
post #68

I gave the problem to chatGPT 5.6 Sol Pro and this was the result: > Worked for 12m 36s > Solved https://chatgpt.com/s/t_6a9aed0b09988191b0f2850dee056b48 Edit: It didn't independently solve it. > 1. Used the public reconstruction to obtain the recovered RTL/constraint structure, including the 11×11 region map and the fact that it is a two-stars-per-row/column/region, non-touching puzzle. > 2. Then independently wrote…

Looks like it did not actually solve it, but instead it just found an existing solution at https://github.com/NotCleo/GDS-to-RTL and verified parts of it? I have no doubt that modern agents can solve challenges like this even without external help, but you should at least briefly look at the output before posting it online!

[deleted]

Re: Solving the Jane Street reverse engineering challenge

#73
post #68

I gave the problem to chatGPT 5.6 Sol Pro and this was the result: > Worked for 12m 36s > Solved https://chatgpt.com/s/t_6a9aed0b09988191b0f2850dee056b48 Edit: It didn't independently solve it. > 1. Used the public reconstruction to obtain the recovered RTL/constraint structure, including the 11×11 region map and the fact that it is a two-stars-per-row/column/region, non-touching puzzle. > 2. Then independently wrote…

Looks like it did not actually solve it, but instead it just found an existing solution at https://github.com/NotCleo/GDS-to-RTL and verified parts of it? I have no doubt that modern agents can solve challenges like this even without external help, but you should at least briefly look at the output before posting it online!

Thanks for pushing back, I've edited my initial post. I misinterpreted the response, I thought that it only referenced the solution as verification.

Re: Solving the Jane Street reverse engineering challenge

#74
I don't think I can ever be motivated by such challenges. It's either I'm getting up to speed to the state of the art from the very basics and then I can try to figure out if something was missing along the way or solve unsolved useful problems, or I will not be interested.

I just can't tinker for the sake of tinkering. Too goal oriented I guess.

Just me? (that is also why school started to bore me right before high school and why I learn better on my own, I did go too College but thank god I didn't do CompSci or that would have disgusted me...)

Re: Solving the Jane Street reverse engineering challenge

#75
post #62

I love z3. I used it for the first time for Jane Street's puzzle last year involving a hashing alg disguised as a neural network. I use a lot of MCMC at work and I have made a few small investigations into MCMC model formal verification via z3, but nothing real yet. This has inspired me to pick that back up.

Can you share more about the connection between MCMC and SAT/SMT? That's a crossover I never thought I'd see.

Sure! Roughly we are using hierarchical models for reads on underlying count or prevalence data. We use those higher-order means or other fit params to kick off remediation tasks at different levels of that hierarchy depending on those higher level params. We assume some correlation between sibling nodes in that hierarchy.

Question: Can one or another of those thresholds in sibling or parent nodes ever be met if some number of the samples are below some floor reading? Or, how many zeros does it take to silence a threshold check on the node itself, a sibling, or a parent?

To make this tractable I have tried gridding fit parameters, freezing randomness, and using simplified algs like original Metropolis-Hastings

Re: Solving the Jane Street reverse engineering challenge

#77

Interesting that they have their own open-source OCaml toolchain for chip design. I thought received wisdom was that everyone in industry is still tied to horrendous vendor toolchains. Is this a realistic alternative for production-grade chip design?

Hardcaml compiles to verilog and then you use the horrendous vendor toolchains.

Re: Solving the Jane Street reverse engineering challenge

#78
post #59

I know nothing about z3 but it's from Microsoft. Would Google's OR-Tools component CP-SAT also be useful for something like this?

Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.

In general that's true, but to reason about boolean circuits like in this challenge we only need a SAT solver. Z3 is just used for it's convenient API.

Re: Solving the Jane Street reverse engineering challenge

#79
post #45
post #42

Earlier quoted context omitted.

Please, explain how you determined this person was an "extremely smart autist".

I took it as a compliment!

I find it hard to believe that saying autistic people are "incredibly hard to manage", that managing them is like "herding cats" and their presence is a "huge liability to the org" is anywhere near complimentary. Autism presents in thousands of ways, and the portrayal is, at best, caricatural.

Re: Solving the Jane Street reverse engineering challenge

#80
post #79
post #45

Earlier quoted context omitted.

I took it as a compliment!

I find it hard to believe that saying autistic people are "incredibly hard to manage", that managing them is like "herding cats" and their presence is a "huge liability to the org" is anywhere near complimentary. Autism presents in thousands of ways, and the portrayal is, at best, caricatural.

Okay dude, don't need to white knight autists. There's a particular archetype of extremely intelligent and technical yet socially unaware or prickly people that's not unfounded in reality. These are the people who do incredible feats. You need a degree of unagreeableness and arrogance to go against the grain and accomplish great things.

It's a thing, I assure you. And it's pretty common parlance in online / technical culture. We don't need to word police this thing.

Post reply on HN