Rendered at 21:21:32 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
piker 11 hours ago [-]
> 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. :)
bko 10 hours ago [-]
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.
vovavili 10 hours ago [-]
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.
bluGill 9 hours ago [-]
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.
Emma_Goldman 9 hours ago [-]
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.
skinfaxi 7 hours ago [-]
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?
I don't know if it's actually true but the idea is interesting.
Emma_Goldman 5 hours ago [-]
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.
ambicapter 5 hours ago [-]
There's this trend on the internet to attribute success at any remotely technically challenging problem to the glorious power of autism.
bob1029 7 hours ago [-]
Good mentorship can make all the difference in the universe.
karmakurtisaani 2 hours ago [-]
I can be a glorified slightly above average ticket pusher, where do I sign up for a million per year job?!
folkrav 9 hours ago [-]
Please, explain how you determined this person was an "extremely smart autist".
anitil 9 hours ago [-]
I took it as a compliment!
folkrav 4 hours ago [-]
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.
bko 3 hours ago [-]
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.
walrus01 11 hours ago [-]
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.
ctippett 8 hours ago [-]
> 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.
darksaints 5 hours ago [-]
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.
mdritch 6 hours ago [-]
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.
kachnuv_ocasek 5 hours ago [-]
Can you share more about the connection between MCMC and SAT/SMT? That's a crossover I never thought I'd see.
mdritch 5 hours ago [-]
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
ngriffiths 1 hours ago [-]
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
xvilka 10 hours ago [-]
To help with such tasks for real chips (given the good quality images) there is Degate[1][2] open source software.
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.
anonymousDan 5 hours ago [-]
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?
vzcx 5 hours ago [-]
Hardcaml compiles to verilog and then you use the horrendous vendor toolchains.
anitil 11 hours ago [-]
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 :)
anitil 10 hours ago [-]
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.
vzcx 10 hours ago [-]
Nice solution and good easter egg find!
NamTaf 10 hours ago [-]
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.
vzcx 10 hours ago [-]
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.
__atx__ 10 hours ago [-]
> 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...
vzcx 10 hours ago [-]
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.
anitil 10 hours ago [-]
> 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!
BalistaCRATZ 10 hours ago [-]
Nice! I ended up using the KLayout Python API to parse the GDS and extract the netlist, which was actually quite nice to use.
I'm not sure I've ever seen such a vicious case of NIH-syndrome. Regardless, congrats on the solve!
bluGill 9 hours ago [-]
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.
_false 9 hours ago [-]
I first thought you were teasing Jane Street instead of OP. Maybe shows that OP is a good culture fit for Jane Street :)
AlDante2 9 hours ago [-]
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).
anitil 9 hours ago [-]
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
paretolaw 24 minutes ago [-]
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. :)
aavshr 8 hours ago [-]
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`.
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?
karelpeeters 10 hours ago [-]
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.
amelius 10 hours ago [-]
If there's a "two stars" solution, then maybe there is also a "three stars" solution?
__atx__ 2 hours ago [-]
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).
6 hours ago [-]
eru 8 hours ago [-]
Weren't you supposed to wait until the submissions close to publish spoilers?
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?
nostrebored 6 hours ago [-]
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.
myng111 6 hours ago [-]
Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.
karelpeeters 4 hours ago [-]
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.
aatd86 5 hours ago [-]
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...)
skr3178 7 hours ago [-]
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.
chermi 5 hours ago [-]
Aspirational. This is how I want to spend my available time.
motoxpro 9 hours ago [-]
So cool to see someone who loves challenges. Congrats!
mring33621 10 hours ago [-]
I love this person!
emptyheaded 6 hours ago [-]
reading the post felt like going down an authentic manic rabbit hole, thanks for sharing your artisanal words @anitil
fabflying 9 hours ago [-]
So good
gyanchawdhary 10 hours ago [-]
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 ..
bux93 9 hours ago [-]
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 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
charcircuit 11 hours ago [-]
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.
anitil 10 hours ago [-]
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
vzcx 10 hours ago [-]
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.
dahshanlabs 10 hours ago [-]
nice one
siramikvarze 32 minutes ago [-]
[dead]
dhzzwgzua 10 hours ago [-]
[dead]
zeninkhan 11 hours ago [-]
[dead]
Taurenking 7 hours ago [-]
[dead]
anon-3988 10 hours ago [-]
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.
seritools 10 hours ago [-]
> Personally, I did not learn that much from that experience.
What did you expect?
anon-3988 6 hours ago [-]
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.
chermi 3 hours ago [-]
"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.
gnyman 9 hours ago [-]
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.
yuye 8 hours ago [-]
>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
topham 29 minutes ago [-]
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.)
josu 5 hours ago [-]
I gave the problem to chatGPT 5.6 Sol Pro and this was the result:
> 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.
karelpeeters 5 hours ago [-]
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!
josu 5 hours ago [-]
Thanks for pushing back, I've edited my initial post. I misinterpreted the response, I thought that it only referenced the solution as verification.
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. :)
At least by the looks of it, Jane Street appears to be an odd one to genuinely value competence.
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.
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.
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.
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.
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
[1] https://www.degate.org/
[2] https://github.com/DegateCommunity/Degate
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...
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 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.
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
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...
I'd like to do a full writeup but haven't had the time.
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!
Also, yosys has support for doing “assertion checking”, which I used in my solution: https://sunaabh.com/systems/2026/08/18/jspuzzle.html
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).
Let them taste their own medicine. :)
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
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...
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.
(Or did they close yesterday?)
https://blog.janestreet.com/can-you-reverse-engineer-an-asic...
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...)
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
These GDS design files have a lot more structure to them.
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.
What did you expect?
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.
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.
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.
>Personally, I did not learn that much from that experience
Fire is hot, water is wet, etc
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.)
> 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.
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!