9 ms·

Program synthesis

54 points by downboots 3y ago

discardable_dan 3y ago
Unfortunately, this entire field has been superseded by LLMs. They are so much more-effective that it's absurd.
- Smaug123 3y ago
  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.
- lmeyerov 3y ago
  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.
marojejian 3y ago
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.
- killthebuddha 3y ago
  +1 to this. IMO the first versions of AGI are going to be program synthesizers.
chilmers 3y ago
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?
- _iv 3y ago
  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.htm https://people.csail.mit.edu/asolar/SynthesisCourse/Lecture1...
coolvision 3y ago
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/ https://grgv.xyz/inductive_program_synthesis/
- andoando 3y ago
  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.
- YorkshireSeason 3y ago
  LLMs today still struggle to met specifications exactly, which is what synthesis is good at.
  - anonzzzies 3y ago
    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.
    - YorkshireSeason 3y ago
      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 ...
- the_panopticon 3y ago
  I recall working on this for synthesizing UEFI and Linux drivers https://trustworthy.systems/publications/nicta_full_text/7690.pdf 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.
nekitamo 3y ago
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 https://github.com/quarkslab/qsynthesis I have yet to try the project from Denuvo but it looks promising: https://github.com/DenuvoSoftwareSolutions/SiMBA https://github.com/DenuvoSoftwareSolutions/SiMBA If any commenter has other suggestions, would love to hear them!
TZubiri 3y ago
Isn't this a synonym for "Computer programming"?
- basil-rash 3y ago
  With modern high level languages, yes, perhaps. The article says as much.
LanternLight83 3y ago
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 https://youtu.be/OyfBQmvr2Hc?feature=shared&t=4656
meltyness 3y ago
Is anyone familiar with how this differs from 'animation' ?

Program synthesis

54 points by downboots 3y ago

discardable_dan 3y ago

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

Smaug123 3y ago
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.
lmeyerov 3y ago
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.

marojejian 3y ago

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.

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

chilmers 3y ago

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?

_iv 3y ago
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.htm https://people.csail.mit.edu/asolar/SynthesisCourse/Lecture1...

coolvision 3y ago

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/ https://grgv.xyz/inductive_program_synthesis/

andoando 3y ago
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.
YorkshireSeason 3y ago
LLMs today still struggle to met specifications exactly, which is what synthesis is good at.
- anonzzzies 3y ago
  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.
  - YorkshireSeason 3y ago
    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 ...
the_panopticon 3y ago
I recall working on this for synthesizing UEFI and Linux drivers https://trustworthy.systems/publications/nicta_full_text/7690.pdf 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.

nekitamo 3y ago

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 https://github.com/quarkslab/qsynthesis I have yet to try the project from Denuvo but it looks promising: https://github.com/DenuvoSoftwareSolutions/SiMBA https://github.com/DenuvoSoftwareSolutions/SiMBA If any commenter has other suggestions, would love to hear them!

TZubiri 3y ago

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

basil-rash 3y ago
With modern high level languages, yes, perhaps. The article says as much.

LanternLight83 3y ago

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 https://youtu.be/OyfBQmvr2Hc?feature=shared&t=4656

meltyness 3y ago

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