Let me help you: work on figuring out how to spend the millions of dollars every year Jane Street will pay you to clock in. I've heard private aviation is expensive, for example. :)
A lot of places claim they want to hire extremely smart autists, and some do. But these types of employees are incredibly hard to manage. Imagine herding cats. So if you don't invest a lot of effort in building an environment to let this person cook, go down the right rabbit holes and not rub others the wrong way, a person like this is a huge liability to the org.
A lot of companies who claim to want highly intelligent and autonomous engineers by revealed preference actually want glorified slightly above average ticket pushers.
At least by the looks of it, Jane Street appears to be an odd one to genuinely value competence.
The strong affinity between autism and intelligence seems strongest in technical fields, and engineering and computer science in particular. Autism does not seem to be over-represented to anywhere near the same degree in many other domains that are full of intelligent people.
Is this just from your direct experience or do you have data to back that up? Are you talking about credentialed engineering like mechanical or civil engineering or just software developers?
There's plenty of data on the clustering of high-functioning autistic workers in engineering and computer science, and the massively disproportionate share of autistic children with fathers and grandfathers in those fields. I work across technical and non-technical academic fields and the difference is quite obvious. It also follows naturally from some of the common presentations of autism, e.g., the high co-occurrence of dyslexia.
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.
Google says "Jane Street has global office locations in New York, London, Hong Kong, Singapore, Amsterdam, and Chicago" so if you're really at a loss where to spend your money, I would recommend searching for yacht dealerships in those cities. I'm sure it won't be a problem anymore.
> I ended up using a tool called ‘z3’. It’s kind of magical? Every time it finds a solution I get a surge of joy.
This resonates so much. I had a similar feeling after going to my very first operations research lecture. Solving seemingly incomprehensibly complex problems by framing them as a bunch of simple constraints and getting a solution seemed like such magic.
Yeah this was my experience too. I have an undergrad business degree, but got nerd sniped by an optimization problem, found a solution with constraint programming, and ended up going down a 15 year operations research rabbit hole with it.
Many people say that the way to tackle a hard problem is to break it down into smaller problems. I disagree. The best way to tackle a hard problem is to break it down into a defined search space and as many seemingly-redundant constraints as you can possibly list, then dump it all into a solver, go take a nap for a few hours or possibly a month, then come back to the problem solved for you.
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.
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
The neural net engineering challenge was so awesome, I got really into it, spent way too much time and then was shocked when I actually managed to solve it. Since then I've gotten interested in... hardware. God help me
Degate is even a bit overkill, it is meant for when you only have images of the physical chip. This challenge has the full GDS files, which are the files that are sent to the fab for manufacturing. They still contain information about all of the separate layers. In this case they even contained the stdcell names, making even full transistor and logic function extraction unnecessary.
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?
Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer.
It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more in detail what my solution looked like, though I intend to write some follow up posts that are a bit more in the weeds of the solution. And frankly, the code I used is pretty ugly but it got the job done.
This is my first blog post, so if you have any feedback please let me know. All the writing, all the code was done by me, by hand, in vim.
> It turns out that this ‘sky130’ thing is like a … standard? Or something for making chips.
Very cool seeing someone completely naive going into this :)
If you want to read more about a bit more... cheaty way to do this, I have written about using formal verification machinery to straight up force the solution out of the netlist here: https://atx.name/electronics/asic-re/ . Could be a bit of an infohazard, but I think journey is the goal and yours was certainly more educational :)
I'll definitely be reading this thankyou! I think this would have been a much better way to approach it, it's a bit of a joke in the piece that I always do things the hard way, but it's a genuine mystery to me why I operate this way.
I should add I have an EE degree (but have never worked as an EE), so even though I don't know industry standards like this sky130 thing, it's not completely foreign to me.
I really enjoyed the writing, cheers. And yes, you may have done it the hard way, but you probably learnt 10x more by doing that.
As for what to do next, I used to spend way too much of my late-2000s time on puzzle hunts (particularly the Melbourne Uni one [1]) and this tickled the same part of my brain. Unfortunately they're no longer a thing, but it definitely sounds like you'd enjoy something similar.
That particular one may be no longer a thing, but there are definitely still plenty of puzzle hunts going on. See e.g. https://en.wikipedia.org/wiki/Puzzle_hunt which has a list.
Incredible amount of determination, but you really did make it hard for yourself!
You can install librelane to get the whole open silicon tool suite and the sky130 PDK. Circuit extraction can be done with magic. Going from a spice netlist to verilog netlist is pretty mechanical and not a hard transform to write. You almost immediately have something that can be simulated and a good baseline for further reversing.
So that was the missing part for me! I did it from scratch (with custom Python script with gdstk and shapely) (the GDS file does have the cells annotated, so not a big problem but still). I was thinking about scripting the "trace net" tool in klayout but decided that's going to probably bring its own can of worms...
You can give the cell instances a stable name by setting GDS property 98, which I learned about from my reconnaissance of the puzzle author's github and sky130 visualization tool. This way I was able to spot check a pass over the netlist that broke up the regions into a hierarchical design.
I'd like to do a full writeup but haven't had the time.
Since this was for fun, and the goal was learning at least as much as solving the problem that is just fine. More people should get NIH for those purposes.
Now if he is presenting his tools as a good way to solve this problem, something you should use, or any such - that would be a bad thing. Good tools for this are complex and need to be done as part of a large team. If good tools that others should use is the goal then he should join some other group making those tools. I'm sure there is an existing open source project (maybe KiCAD - I'm not in this space so that is the only name I can come up with but maybe their goals are different?) that does this and would welcome more help.
just for info: https://en.wikipedia.org/wiki/GDSII will tell you about the GDS format. It apparently stands for Graphic Data System II (originally developed by Calma in the late 1970s).
That's really interesting that you actually used z3 to extract the output from the circuit! It hadn't occurred to me that it would be possible to do that. I suppose I got a little fixated on my approach of running a verilog simulation, and I only used z3 to solve one part (though the hardest part I think). How did you get a $DAYJOB involving formal verification?
Yeah I briefly considered switching to a simulator to get the final output, but then luckily realized the Z3 setup I had was already acting as a super-powered simulator anyway!
I'm not actually using formal verification at $DAYJOB, there we're using MILP solvers (which are closely related to SAT solvers) as part of the compilation flow when scheduling operations onto hardware accelerators.
I have been interested in formal verification for hardware for a while, but so far haven't found an opportunity to apply it. There are some great resources online though: the ZipCpu blog at https://zipcpu.com/formal/formal.html and SymbiYosys website at https://symbiyosys.readthedocs.io/en/latest/. I hindsight I could probably have used SymbiYosys instead of Z3, it would have saved me from having to walk the graph and map the gates to equations myself.
I checked and the solution is unique (at least within some reasonable bounds in terms of runtime etc, it's possible there is a 1000 bits long special solution hidden somewhere, but due to the relatively small amount of flops I doubt it).
z3 is also just so thoroughly optimized that even if your formulation of the constraints is inefficient it is faster. it is a great library that lets you solve pretty complicated DP problems with a few dozen lines of code.
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.
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...)
Solving the puzzle with the assistance of a lower capability LLM model (even though I had access to more) turned out to be fun and good learning experience.
curious what the actual use case for a challenge like this is from Jane Streets side .. guess the obvious one is trading even closer to the wire .. being able to reverse engineer .. inspect circuits to uncover flaws or optimisations that shave latency or improve determinism in the trading stack .. but I wonder if there are other less obvious applications ..
I read their posts and podcasts. They high frequency trade. They work in micro- and nano-seconds. I don't know what I'm talking about here, don't quote me, but a top guy said they 'process packets' the data is starting to be sent out while it's still arriving. Close to the wire/metal
Probably this is just an unfamiliar domain for most non-hardware folks, so it's a nice challenge that might introduce Jane Street to some people they might want to interview for non-hardware roles.
I wonder how far a LLM could get with this. It will be cool when we get to the point where you can decap a chip, take a picture, and then an LLM can create an emulator for that chip.
I'd say they could solve it much faster than I could. Some of the other commenters are mentioning tools that would have made this so much easier, and I'd assume an LLM would know to use them
I have used Codex (Sol 5.6 or whatever) to solve this problem. It turns the problem into Z3, then iteratively work through the problems until it figured out the solution.
Personally, I did not learn that much from that experience. So I am glad that there's other people working on it as well. I am mostly interested in the techniques used to solve this.
I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide?
That itself is a learning experience. What is even the point of technical interview questions or take home questions? This means that I am now open to hiring completely non-technical person, as long as they have a good personality and management skills more than a competent developer.
"I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide?"
This is sad conclusion. Maybe you're more right than wrong, but my answer to the "value" question would be:
Solving even harder problems based on lessons from solving easier ones? Pretty similar to the trajectory in this blog post. Perhaps aided additionally by llms and other tools that can solve the subproblems so you can focus on the less obvious/automatable aspects of the problem?
But note the tension, only by being involved in the problem solving to some extent do you become better at it. So if your default is to say "An LLM can or will soon be able to solve it, why bother?", then your situation will become more desperate and your outlook more negative in a self-reinforcing way.
The fact that agents can solve these is telling and the Infosec Capture The Flag community is trying to figure out how to approach.
I recently solved a (in)famously hard challenge (disobey conference hacker ticket) more or less by accident. I say by accident because I have always ignored this challenges as they generally require a lot of patience and motivation to solve. Some years they haven't been solved at all.
This year I had a GPT sub with some unused quota so I thought let's see how far it gets.
And it crunched through the whole thing in an evening and morning (occasional poking from me to keep going and steer it right).
Like anon, I learned nothing except that the agents have become really good at solving puzzles. Last time I had thrown a puzzle on them was Advent of code, with GPT3 I think and it struggled so much I gave up my experiment on day 7 or something.
If learning is the point then obviously that was a missed opportunity.
If success was the intent, then it's a win.
While challenges are fun, sometimes the requirement is simply to achieve the end goal, with no other point than that.
If your job is to stop terrorists, and that includes hacking into a system and extracting their plans, the "fun" of it isn't the point, only the end goal it's important. Sometimes when we do things like this for fun we forget that someone else out there absolutely needs to achieve the result and doesn't care how it's achieved.
It's the part of penetration testing some people miss. (It's not generally a fun job, almost everyone I know that did it got out as soon as possible. They weren't solving problems, they just running audit scripts and generating reports.)
> 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 and ran my own exhaustive solver against that recovered constraint system.
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!
I got one better puzzle. Predict Jane algo moves when they try to manipulate market and frontrun their orders.
Let them taste their own medicine. :)
> Well I don’t really know what to work on next
Let me help you: work on figuring out how to spend the millions of dollars every year Jane Street will pay you to clock in. I've heard private aviation is expensive, for example. :)
A lot of places claim they want to hire extremely smart autists, and some do. But these types of employees are incredibly hard to manage. Imagine herding cats. So if you don't invest a lot of effort in building an environment to let this person cook, go down the right rabbit holes and not rub others the wrong way, a person like this is a huge liability to the org.
A lot of companies who claim to want highly intelligent and autonomous engineers by revealed preference actually want glorified slightly above average ticket pushers.
At least by the looks of it, Jane Street appears to be an odd one to genuinely value competence.
There are a lot of incredibly smart non-autists. Or maybe slightly autistic, but enough awareness of the real world that they can be managed.
The strong affinity between autism and intelligence seems strongest in technical fields, and engineering and computer science in particular. Autism does not seem to be over-represented to anywhere near the same degree in many other domains that are full of intelligent people.
Is this just from your direct experience or do you have data to back that up? Are you talking about credentialed engineering like mechanical or civil engineering or just software developers?
https://pmc.ncbi.nlm.nih.gov/articles/PMC9058071/ (if "strong affinity" means "bimodal distribution and I ignore the lower pole")
https://pubmed.ncbi.nlm.nih.gov/38497251/ (if "engineering and computer science" means "IT")
I don't know if it's actually true but the idea is interesting.
There's plenty of data on the clustering of high-functioning autistic workers in engineering and computer science, and the massively disproportionate share of autistic children with fathers and grandfathers in those fields. I work across technical and non-technical academic fields and the difference is quite obvious. It also follows naturally from some of the common presentations of autism, e.g., the high co-occurrence of dyslexia.
There's this trend on the internet to attribute success at any remotely technically challenging problem to the glorious power of autism.
Good mentorship can make all the difference in the universe.
I can be a glorified slightly above average ticket pusher, where do I sign up for a million per year job?!
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.
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.
Google says "Jane Street has global office locations in New York, London, Hong Kong, Singapore, Amsterdam, and Chicago" so if you're really at a loss where to spend your money, I would recommend searching for yacht dealerships in those cities. I'm sure it won't be a problem anymore.
> I ended up using a tool called ‘z3’. It’s kind of magical? Every time it finds a solution I get a surge of joy.
This resonates so much. I had a similar feeling after going to my very first operations research lecture. Solving seemingly incomprehensibly complex problems by framing them as a bunch of simple constraints and getting a solution seemed like such magic.
Yeah this was my experience too. I have an undergrad business degree, but got nerd sniped by an optimization problem, found a solution with constraint programming, and ended up going down a 15 year operations research rabbit hole with it.
Many people say that the way to tackle a hard problem is to break it down into smaller problems. I disagree. The best way to tackle a hard problem is to break it down into a defined search space and as many seemingly-redundant constraints as you can possibly list, then dump it all into a solver, go take a nap for a few hours or possibly a month, then come back to the problem solved for you.
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
Oh no
The neural net engineering challenge was so awesome, I got really into it, spent way too much time and then was shocked when I actually managed to solve it. Since then I've gotten interested in... hardware. God help me
To help with such tasks for real chips (given the good quality images) there is Degate[1][2] open source software.
[1] https://www.degate.org/
[2] https://github.com/DegateCommunity/Degate
Degate is even a bit overkill, it is meant for when you only have images of the physical chip. This challenge has the full GDS files, which are the files that are sent to the fab for manufacturing. They still contain information about all of the separate layers. In this case they even contained the stdcell names, making even full transistor and logic function extraction unnecessary.
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.
Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer.
It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more in detail what my solution looked like, though I intend to write some follow up posts that are a bit more in the weeds of the solution. And frankly, the code I used is pretty ugly but it got the job done.
This is my first blog post, so if you have any feedback please let me know. All the writing, all the code was done by me, by hand, in vim.
[0] https://blog.janestreet.com/can-you-reverse-engineer-an-asic...
> It turns out that this ‘sky130’ thing is like a … standard? Or something for making chips.
Very cool seeing someone completely naive going into this :)
If you want to read more about a bit more... cheaty way to do this, I have written about using formal verification machinery to straight up force the solution out of the netlist here: https://atx.name/electronics/asic-re/ . Could be a bit of an infohazard, but I think journey is the goal and yours was certainly more educational :)
I'll definitely be reading this thankyou! I think this would have been a much better way to approach it, it's a bit of a joke in the piece that I always do things the hard way, but it's a genuine mystery to me why I operate this way.
I should add I have an EE degree (but have never worked as an EE), so even though I don't know industry standards like this sky130 thing, it's not completely foreign to me.
Nice solution and good easter egg find!
I really enjoyed the writing, cheers. And yes, you may have done it the hard way, but you probably learnt 10x more by doing that.
As for what to do next, I used to spend way too much of my late-2000s time on puzzle hunts (particularly the Melbourne Uni one [1]) and this tickled the same part of my brain. Unfortunately they're no longer a thing, but it definitely sounds like you'd enjoy something similar.
[1]: https://www.puzzles.wiki/wiki/MUMS_Puzzle_Hunt
That particular one may be no longer a thing, but there are definitely still plenty of puzzle hunts going on. See e.g. https://en.wikipedia.org/wiki/Puzzle_hunt which has a list.
Incredible amount of determination, but you really did make it hard for yourself!
You can install librelane to get the whole open silicon tool suite and the sky130 PDK. Circuit extraction can be done with magic. Going from a spice netlist to verilog netlist is pretty mechanical and not a hard transform to write. You almost immediately have something that can be simulated and a good baseline for further reversing.
> Circuit extraction can be done with magic.
So that was the missing part for me! I did it from scratch (with custom Python script with gdstk and shapely) (the GDS file does have the cells annotated, so not a big problem but still). I was thinking about scripting the "trace net" tool in klayout but decided that's going to probably bring its own can of worms...
You can give the cell instances a stable name by setting GDS property 98, which I learned about from my reconnaissance of the puzzle author's github and sky130 visualization tool. This way I was able to spot check a pass over the netlist that broke up the regions into a hierarchical design.
I'd like to do a full writeup but haven't had the time.
> Incredible amount of determination
That's very kind of you. At some point I had put so much of myself in to it that I was in too deep and the only was out was to keep digging.
I'll take a look at librelane thanks!
Nice! I ended up using the KLayout Python API to parse the GDS and extract the netlist, which was actually quite nice to use.
Also, yosys has support for doing “assertion checking”, which I used in my solution: https://sunaabh.com/systems/2026/08/18/jspuzzle.html
I'm not sure I've ever seen such a vicious case of NIH-syndrome. Regardless, congrats on the solve!
Since this was for fun, and the goal was learning at least as much as solving the problem that is just fine. More people should get NIH for those purposes.
Now if he is presenting his tools as a good way to solve this problem, something you should use, or any such - that would be a bad thing. Good tools for this are complex and need to be done as part of a large team. If good tools that others should use is the goal then he should join some other group making those tools. I'm sure there is an existing open source project (maybe KiCAD - I'm not in this space so that is the only name I can come up with but maybe their goals are different?) that does this and would welcome more help.
I first thought you were teasing Jane Street instead of OP. Maybe shows that OP is a good culture fit for Jane Street :)
Hi Chris,
just for info: https://en.wikipedia.org/wiki/GDSII will tell you about the GDS format. It apparently stands for Graphic Data System II (originally developed by Calma in the late 1970s).
No spoilers! But thanks I did find out after I published, I just thought it was funnier not to know while I was working on it
There's a typo on your link to the two stars image.
It should be `/img/two-stars.png` instead it's right now `/img/two-starts.pgn`.
For those interested in the image itself: https://jestoph.com/img/two-stars.png
oh boy here we go again
Congrats on solving the challenge!
I also briefly wrote about my approach here, with less pictures but going into slightly more detail about how to convert circuits to z3 equations: https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079...
That's really interesting that you actually used z3 to extract the output from the circuit! It hadn't occurred to me that it would be possible to do that. I suppose I got a little fixated on my approach of running a verilog simulation, and I only used z3 to solve one part (though the hardest part I think). How did you get a $DAYJOB involving formal verification?
Yeah I briefly considered switching to a simulator to get the final output, but then luckily realized the Z3 setup I had was already acting as a super-powered simulator anyway!
I'm not actually using formal verification at $DAYJOB, there we're using MILP solvers (which are closely related to SAT solvers) as part of the compilation flow when scheduling operations onto hardware accelerators.
I have been interested in formal verification for hardware for a while, but so far haven't found an opportunity to apply it. There are some great resources online though: the ZipCpu blog at https://zipcpu.com/formal/formal.html and SymbiYosys website at https://symbiyosys.readthedocs.io/en/latest/. I hindsight I could probably have used SymbiYosys instead of Z3, it would have saved me from having to walk the graph and map the gates to equations myself.
If there's a "two stars" solution, then maybe there is also a "three stars" solution?
I checked and the solution is unique (at least within some reasonable bounds in terms of runtime etc, it's possible there is a 1000 bits long special solution hidden somewhere, but due to the relatively small amount of flops I doubt it).
Weren't you supposed to wait until the submissions close to publish spoilers?
(Or did they close yesterday?)
> Submissions close on September 4th, 2026.
https://blog.janestreet.com/can-you-reverse-engineer-an-asic...
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 also just so thoroughly optimized that even if your formulation of the constraints is inefficient it is faster. it is a great library that lets you solve pretty complicated DP problems with a few dozen lines of code.
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.
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...)
Solving the puzzle with the assistance of a lower capability LLM model (even though I had access to more) turned out to be fun and good learning experience.
Aspirational. This is how I want to spend my available time.
So cool to see someone who loves challenges. Congrats!
I love this person!
reading the post felt like going down an authentic manic rabbit hole, thanks for sharing your artisanal words @anitil
So good
curious what the actual use case for a challenge like this is from Jane Streets side .. guess the obvious one is trading even closer to the wire .. being able to reverse engineer .. inspect circuits to uncover flaws or optimisations that shave latency or improve determinism in the trading stack .. but I wonder if there are other less obvious applications ..
I read their posts and podcasts. They high frequency trade. They work in micro- and nano-seconds. I don't know what I'm talking about here, don't quote me, but a top guy said they 'process packets' the data is starting to be sent out while it's still arriving. Close to the wire/metal
Probably this is just an unfamiliar domain for most non-hardware folks, so it's a nice challenge that might introduce Jane Street to some people they might want to interview for non-hardware roles.
But, they do have a hardware division, and Jane Street has a podcast that talks about some of the things they do https://signalsandthreads.com/?tag=hardware
wow thanks for sharing, will check it out
I wonder how far a LLM could get with this. It will be cool when we get to the point where you can decap a chip, take a picture, and then an LLM can create an emulator for that chip.
I'd say they could solve it much faster than I could. Some of the other commenters are mentioning tools that would have made this so much easier, and I'd assume an LLM would know to use them
This would need good image recognition, but maybe not so far out of the realm of possibility.
These GDS design files have a lot more structure to them.
nice one
I have used Codex (Sol 5.6 or whatever) to solve this problem. It turns the problem into Z3, then iteratively work through the problems until it figured out the solution.
Personally, I did not learn that much from that experience. So I am glad that there's other people working on it as well. I am mostly interested in the techniques used to solve this.
> Personally, I did not learn that much from that experience.
What did you expect?
I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide?
That itself is a learning experience. What is even the point of technical interview questions or take home questions? This means that I am now open to hiring completely non-technical person, as long as they have a good personality and management skills more than a competent developer.
"I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide?"
This is sad conclusion. Maybe you're more right than wrong, but my answer to the "value" question would be:
Solving even harder problems based on lessons from solving easier ones? Pretty similar to the trajectory in this blog post. Perhaps aided additionally by llms and other tools that can solve the subproblems so you can focus on the less obvious/automatable aspects of the problem?
But note the tension, only by being involved in the problem solving to some extent do you become better at it. So if your default is to say "An LLM can or will soon be able to solve it, why bother?", then your situation will become more desperate and your outlook more negative in a self-reinforcing way.
The fact that agents can solve these is telling and the Infosec Capture The Flag community is trying to figure out how to approach.
I recently solved a (in)famously hard challenge (disobey conference hacker ticket) more or less by accident. I say by accident because I have always ignored this challenges as they generally require a lot of patience and motivation to solve. Some years they haven't been solved at all. This year I had a GPT sub with some unused quota so I thought let's see how far it gets.
And it crunched through the whole thing in an evening and morning (occasional poking from me to keep going and steer it right).
Like anon, I learned nothing except that the agents have become really good at solving puzzles. Last time I had thrown a puzzle on them was Advent of code, with GPT3 I think and it struggled so much I gave up my experiment on day 7 or something.
>I have used Codex (Sol 5.6 or whatever) to solve this problem.
>Personally, I did not learn that much from that experience
Fire is hot, water is wet, etc
If learning is the point then obviously that was a missed opportunity.
If success was the intent, then it's a win.
While challenges are fun, sometimes the requirement is simply to achieve the end goal, with no other point than that.
If your job is to stop terrorists, and that includes hacking into a system and extracting their plans, the "fun" of it isn't the point, only the end goal it's important. Sometimes when we do things like this for fun we forget that someone else out there absolutely needs to achieve the result and doesn't care how it's achieved.
It's the part of penetration testing some people miss. (It's not generally a fun job, almost everyone I know that did it got out as soon as possible. They weren't solving problems, they just running audit scripts and generating reports.)
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 and ran my own exhaustive solver against that recovered constraint system.
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.