[almostgotcaught]

> about how to solve np-hard problems there instantly. ... without losing safety. Ex: leapfrog the concolic execution papers via a fast oracle

Just want to point out to unknowing readers: none of this is true and the author of these comments is "talking his book".

Source: do I really need to explain how LLMs do not solve NP-hard problems "instantly"?

[lmeyerov]

Most of the papers in the syllabus are about the SAT/SMT-based solver era of program synthesis, and neural synthesis is popularly - with open benchmarks - succeeding on problems those failed to gain traction on.

The research question is shifting to how to either bridge the worlds (better together) or leave the old one. That doesn't make SMT era papers wrong, but as with Bayesian vs NN, relatively impractical or otherwise irrelevant for most people until a major breakthrough happens (if ever). Ex: Agentic loops are interesting from a direct reuse of classical synthesis results perspective, and I know big labs are experimenting with different methods.

I'm transparent that I was part of the old world, and while synthesis was a design hope for our startup (I was publicly demoing SOTA here 10 years ago!), it was never to the quality we could invest in commercializing those school of methods. When GPT4 hit, we could finally add synthesis-based methods that ship. I get the impression you are part of the older SMT world and reject modern advances, and would wonder the reverse for you. It's a bit galling to be accused of voting with my feet - and shipping - after patiently waiting 10 years as an invalidating thing instead of taking that as a proof point that maybe there is something going on.