Hacker News Reader

Comment by coolvision | Hacker News Reader

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/

View on HN

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 ...

If this is what programmers believe, I pity software users of 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.

Reply on news.ycombinator.com