Program synthesis | Hacker News Reader

Program synthesis

en.wikipedia.org

54 pointsdownboots19 comments

This is probably my favorite field for future ML development. It both covers the areas where we are weakest (compositionality, planning), but also is feasible for training (easy to generate samples and create objective functions, vs. say IRL tasks), and is immensely valuable if we succeed.

If an ML engineering agent that is actually comparable to a human is developed, things are going to we weird. fast.

+1 to this. IMO the first versions of AGI are going to be program synthesizers.

I've worked a bit on inductive syntax-guided synthesis, but did it at the worst time -- right before it was made obsolete by LLMs: https://grgv.xyz/inductive_program_synthesis/

I am confused. Isnt the whole point of this that these programs provably do what they do? Isnt that the opposite of LLMs?

Seems more like LLMs made something more immediately useful.

LLMs today still struggle to met specifications exactly, which is what synthesis is good at.

There is interesting research in having LLMs cull the search space (for instance, asking the llm to provide which instructions are needed to complete the spec and provide an implementation) and then using more traditional techniques like ilp (or other symbolic means) to find the final program that corresponds to the spec. That way the result meets the spec but converges much (much!) faster than the traditional way for far complexer cases. Sometimes the llm gets it right in one shot (and the engine just verifies it is correct), sometimes it will never get it correct but ilp will finish the job just fine.

I agree this is an interesting direction. IIRC the top (open) bitvector synthesiser works like this (albeit not with ILP).

Trouble with ILP is that it doesn't work on GPUs (as of April 2024) and on CPUs synthesis and other forms of learning are hopeless. That may change in the future ...

I recall working on this for synthesizing UEFI and Linux drivers https://trustworthy.systems/publications/nicta_full_text/769... back in the day. Luckily some of the artifacts made it to open source. Unluckily the generated source code was tough for humans to read and maintain. The readability of LLM-based source code solutions from tools like Github CoPilot is amazing in comparison.

If this is what programmers believe, I pity software users of the future.

I stumbled on the idea of Program Synthesis when I was looking to solve VMProtect's Mixed-Boolean-Arithmetic (MBA) expressions in my own VMP Decompiler. I tried experimenting with this project but had limited success:

https://github.com/quarkslab/qsynthesis

I have yet to try the project from Denuvo but it looks promising:

https://github.com/DenuvoSoftwareSolutions/SiMBA

If any commenter has other suggestions, would love to hear them!

I associate program synthesis pretty heavily with William Byrd following his demo in the second half of this talk:

https://youtu.be/OyfBQmvr2Hc?feature=shared&t=4656

Is anyone familiar with how this differs from 'animation' ?

Isn't this a synonym for "Computer programming"?

With modern high level languages, yes, perhaps. The article says as much.

Perhaps I'm missing something, but is program synthesis just writing a compiler for a long-winded functional programming language? I'm not even clear if it will avoid bugs, since your specification could just as easily have a missing or mistaken constraint as the equivalent program?

This Wikipedia article is a very small slice of a large field[1]. SyGuS is a language to specify inputs and constraints meant to standardize the field. The main benefit to this standardization is to allow researchers to benchmark their synthesizers against others'. Naturally, this leads to an annual competition (SyGuS-Comp).

There are other ways to specify your desired program, such as sets of input-output pairs, or natural language as others are discussing with LLMs. SyGuS is a denotational, rather than operational way to describe a program's behavior.

If a synthesized program satisfies the specification given, then by definition it is bug free. It's possibly the largest problem facing the field that specifications are difficult to write, and often harder than just writing the code correctly yourself. I believe the S-expression based language is chosen primarily due to its easy parsing and generation.

[1] https://people.csail.mit.edu/asolar/SynthesisCourse/Lecture1...

Unfortunately, this entire field has been superseded by LLMs. They are so much more-effective that it's absurd.

Depends on the definition of "effective", of course. They're certainly more prolific, but "provably satisfies a specification" (from the first line of the Wikipedia page) is kind of the opposite of what they do.

As someone who worked in the field, I think there were 3 big directions in the last ~20 years that remain relevant:

* Experiments in interface design, the equivalent of language design. These balance being able to guide the system and being able to maintain code written this way. Cleverness here ended up leading to a lot of gains in the more practical systems, and IMO, is one of the more important problems in scaling LLM tools to be a bigger part of how teams build software.

* Optimized search procedures. Ex: Concolic execution and counter-example guided execution, that are the outer loop and tricks over whatever per-step model (SMT, LLM) is used. Think algorithms behind optimal agents that go beyond "we run lint, feed it into the LLM, and loop until the output is good."

* How to discharge useful fragments to SMT solvers and other technologies. Not used much publicly nor discussed, but we already find value here, such as generating database queries.

The last 10 years has seen a move to combining neural methods with symbolic, so I view them as complementary, and so should most folks doing agent-based LLM work (read: most). It was frustrating to me that the ML methods (largely bayesian) at the time I was attempting failed so our group found more mileage in sticking to the symbolic side. Likewise, even LLMs aren't the be-all for AI methods -- there's a lot of cool recommender work we do that is outside of the LLM.

Nowadays, we're building louie.ai to finally do both sides of the equation. Our focus is less on SMT and more on search + LLM, but we've already found cases where combining LLMs with classic PL approaches helped some of our query synthesis problems. If folks are interested in opportunities here, the graphistry team has open roles, immediately on a security principle researcher / senior SA, and we expect a senior backend/infra SE soon as well.

Reply on news.ycombinator.com