Introduction to Program Synthesis

eval is crucial, as that's the only way to agree with the computer what it is doing matches what you want it to do.

I wouldn't worry about speeds. We should expect compute and inference to be faster in the future, where we can sample easily 10k programs in a second, check all of them against test cases.

I'd worry about communicating precisely to computers when test cases are awkward to write.

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.

Hi Squircle!

I mostly left academia after graduating, and am not actively following current research, although I still live in Cambridge and attend a fair number of research events. I can say that deep learning has taken over PL research, just like everything else. A good number of PL and synthesis people have shifted heavily into pure deep learning, and a large proportion of those that haven't are working either on applying deep learning and LLMs to solve PL problems, fusing PL and ML techniques (aka "neurosymbolic programming" -- the Scallop project from Mayur Naik's group is particularly exciting to me), or finding ways to use PL techniques to solve ML problems. For an example of the latter, I just flipped through this year's PLDI papers, and one caught my eye that sounds like it has nothing to do with AI, "Hashing Modulo Context-Sensitive Alpha Equivalence." (Decoding the jargon, that means "How to deal with an enormous set of programs that contain lambdas" -- something that comes up when doing search-based synthesis and superoptimization.) Its abstract ends: "We have employed the algorithm to obtain a large-scale, densely packed, interconnected graph of mathematical knowledge from the Coq proof assistant for machine learning purposes."

I think PL techniques do provide the key to overcoming a lot of the problems with LLMs. You want your LLM to have better correctness, reasoning, and goal-directed search -- researchers in programming languages and formal methods are expert at this. I am here to some extent conflating PL/FM techniques with traditional automated reasoning, but I think that's a fine conflation to make, because such techniques have been incubated by the PL/FM communities for the past 30 years since they were sidelined by AI. Case in point: very large fraction of computational logic and automated reasoning papers are motivated by problems in program analysis, verification, and synthesis.. https://easychair.org/smart-program/FLoC2022/index.html

As for what I have been up to: Trained a few hundred more software engineers, mirdin.com . While I mostly stayed away from AI stuff during my Ph. D., I've given in to the tides, and am now building a startup using my AI, PL, and pedagogy expertise to solve all problems related to codebase-learning (onboarding new hires, changing teams faster, etc).

At the very end of my Ph. D., I discovered a new program synthesis technique based on constrained tree automata, and used it to build a synthesizer which is 8x more performant on one benchmark than the previous SOTA while using 10x less code. https://www.jameskoppel.com/files/papers/ecta.pdf . So the research I've done since graduating has largely been follow-ups to that. See https://www.computer.org/csdl/proceedings-article/icst/2023/... , https://pldi22.sigplan.org/details/egraphs-2022-papers/4/E-G... . I'm currently on two collaborations. One is continuing to develop algorithms for new kinds of constrained tree automata that can synthesize more kinds of programs. The other is an outgrowth of my startup: an empirical study on existing tools for codebase learning.

Anyway, that's not a comprehensive answer on what to watch out for in the field, which I am not presently qualified to give if I ever was, but it's the things that have my attention.

Oh, but: watch Isil Dillig. Everything that comes out of her lab is good.

1. I've been a doomer since before the term was invented, and I never had any worry about synthesis research based on symbolic techniques. Gödel is our friend here: they're not powerful enough to model themselves. The best you get is stuff like https://ieeexplore.ieee.org/abstract/document/7886678?casa_t... . An important component of the Sketch synthesizer is its simplifier, and this paper used Sketch to synthesize a better simplifier, and that speeds up synthesis times by 15%-60%. But that's a one-time improvement. The exponential take off comes from somewhere else.

2. Let me see if I understand your question: I think you're saying "The frame problem of AI and philosophy, https://plato.stanford.edu/entries/frame-problem/ , was the major blocker in AI systems, and now it's been solved by deep learning. What is the corresponding problem in program synthesis?" I think your "pretty damn robust" comment is important, but haven't yet figured out what you mean.

Part of the reason I found this confusing is that the literal frame problem also appears in PL and synthesis, primarily in the verification of heap-based imperative programs. See the "frame rule" of separation logic.

So anyway, what do I see as the big challenges stopping synthesis from reaching its dream of being able to generate well-designed large programs with little input?

My two answers:

First, there's the problem of finding good abstractions. You see this in very old work:trying to prove an imperative program works is easy to automate EXCEPT for the problem of finding loop invariants. This has remained a challenging problem in the 50 years since it was first described. Craig interpolation is the classic solution, but it only goes so far. The synthesis view is: figuring out how to write loops is not straightforward because you need to summarize infinitely possible states. And that's loops; designing data structures and finding good invariants for stateful applications is harder still.

Second is what I like to call the "semantic veil." Generally, for any given chunk of code, there are multiple goals and abstractions that yield the same chunk of code. See my analogy to dairy-free chocolate chips in https://www.pathsensitive.com/2023/03/modules-matter-most-fo... . So deducing the intentions of a piece of code from just the code itself is literally impossible. Unfortunately, the way humans design programs is much better understood as being about these higher-level organizational structures, and not about the code itself. This is an area where I'm excited about the potential of LLMs: they can make excellent use of the information in priors and in natural language to guess said intentions.

Supporting an old codebase is a pretty broad question. There are quite a few companies supporting COBOL.

But for migrations, and really anything interesting or unique, I recommend Semantic Designs. http://www.semdesigns.com/ . Past customers include ADP, the Social Security Administration, the Bank of Australia/New Zealand, and Goldman Sachs Australia.

They do everything, but COBOL migrations are their bread-and-butter. There are hundreds of COBOL dialects out there, and they have no trouble supporting all of them.

I did interned for them in 2016, and the CEO served on my thesis committee. But I'm not saying this because I worked there; I worked there because I thought they had the best tech.

That's very relevant to generate-and-test program search.

The SBSE (search-based software engineering) and APR (automated program repair) communities do that kind of stuff. E.g.: There's a paper from that world, which I can't presently find, on "super mutants": basically, use environmental variables as feature flags so that you can compile 100 variants at once. Back when I worked in this space, one of the best things I did was run the Java compiler from within nailgun (program that saves JVM startup time) to compile mutants faster.

Symbolic program synthesis doesn't work like this. They effectively has its own compiler toolchain that transform programs into constraint systems and/or do partial evaluation of programs with wholes. Most of them never run a traditional compiler; they just guarantee that they output correct code.

Could you give an example of an apples-to-apples comparison between (symbolic) program synthesis and LLMs that the latter wins?

The reason I am asking is because, in my experience, LLMs never match the 100% precision (relative to the specification that is synthesised against), which program synthesis effortlessly matches.

On the apples-to-apples comparisons, LLMs often only obtain 70% - 80% precision, which means they are effectively solving a simpler synthesis problem. (Yes they have other benefits, like being able to extract knowledge from natural language, which conventional synthesis can't do, but that's offen not needed.)

Do you have a link to literature review?