[SnowflakeOnIce]

The classical synthesis approaches seem to have much more emphasis on correctness and specification than modern LLM-based synthesis though — things like deriving provably correct lock-free data structures.

The LLM-based synthesis work I've seen, in contrast, maybe uses a set of unit tests for correctness testing.

It doesn't feel like modern LLM-based synthesis supplants the classical approaches.

[lmeyerov]

If you think about classical synthesis as fancy tricks around optimizing SAT encodings & search, neural synthesis becomes about how to solve np-hard problems there instantly. There are other perspectives as well, but that's already a dual LLM paper for a bunch of individual classical papers, without losing safety. Ex: leapfrog the concolic execution papers via a fast oracle.

Likewise, a lot of cool work is about automating the proof theory much better. Terrance Tao has been going down that rabbithole, which is amazing, and I hope the security community does too. I know Dawn Song, one of the big names here, is.

Another big area is making programming more accessible by assuming synthesizers, and language design decisions around that. A lot of that work has been shifting bc LLMs too. Ex: Historically PLs had zero domain understanding, just logic, and that has really flipped since GPT4, so the concept of a DSL is now also flipping.

Finally.. a lot of neural synthesis can and does entirely ignore the SAT aspect. There is a lot of depth to it on its own, and amazing results.

[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.

[Karrot_Kream]

Have a few papers on hand to start reading about these?

[lmeyerov]

Edit: I'd be curious which other papers/authors folks would add who are doing interesting work here.

One starting point is to look at great synthesis, mechanized proofs, and PL folks who have been exploring neural synthesis, and the papers they write + cite:

* Arjun guha: starcoder llm, llm type inference, etc

* Sumit Gulwani & Rishabh Singh (whose pre-llm work is on the syllabus)

* Nikhil Swamy (f*), Sorin Lerner (coq)

* A practical area that has a well-funded intersection because of urgency is security, such as niches like smart contracts, and broader bug finding & repair. Eg, simpler applied methods by Trail of Bits, and any academics they cite. Same thing for DARPA challenge participants: they likely have relevant non-DARPA papers.

* I've been curious about the assisted proof work community Terence Tao has fallen into here as well

* Edit: There are a bunch of Devin-like teams (ex: Princeton team markets a lot, ...), and while interesting empirically, they generally are not as principaled, which is the topic here, so I'm not listing. A lot of OOPSLA, MSR, etc papers are doing incremental work here afaict, so work to sort out

An important distinction for me is whether it is an agentic system (which is much of it and can more easily use heavier & classic methods), training an existing architecture (often a stepping stone to more interesting work), or making a novel architecture (via traditional NLP+NN tricks vs synthesis-informed ones). Most practical results today have been clever agentic, better training sets, and basic NLP-flavored arch tweaks. I suspect that is because those are easiest and early days/years, and thus look more for diversity of explorations right now vs deep in any one track.