9 ms·

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_pr

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 2y 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 2y ago
LLMs today still struggle to met specifications exactly, which is what synthesis is good at.
- anonzzzies 2y 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 2y 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 2y 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.
dkjaudyeqooe 2y ago
If this is what programmers believe, I pity software users of the future.

andoando 2y 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 2y ago

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

anonzzzies 2y 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 2y 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 2y 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.

dkjaudyeqooe 2y ago

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