3 ms·

This is a very classic view, and while interesting, IMO the modern take doesn't start till lecture 22. I would expect a reformulation of the lecture series by n

This is a very classic view, and while interesting, IMO the modern take doesn't start till lecture 22. I would expect a reformulation of the lecture series by now. As is, it reads as if an AI course does 21 lectures on Bayesian methods and then ends with a couple on neural networks: Bayesian tricks are neat, but not how I'd structure a general course. Cool but... I wonder what an update would look like. (I overlapped in the same synthesis research lab as the author by a few years, and currently do LLMs for code synthesis in louie.ai... and much of the coursework was from around those Berkeley years and some MIT ones 10-20 years ago afaict. A lot of foundational work has happened since then.).

SnowflakeOnIce 2y ago
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 2y ago
  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.
  - Karrot_Kream 2y ago
    Have a few papers on hand to start reading about these?
    - lmeyerov 2y ago
      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.
  - almostgotcaught 2y ago
    > 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"?

SnowflakeOnIce 2y ago

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 2y ago
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.
- Karrot_Kream 2y ago
  Have a few papers on hand to start reading about these?
  - lmeyerov 2y ago
    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.
- almostgotcaught 2y ago
  > 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"?