[HN Gopher] Program Synthesis
       ___________________________________________________________________
        
       Program Synthesis
        
       Author : downboots
       Score  : 21 points
       Date   : 2024-04-13 03:52 UTC (1 days ago)
        
 (HTM) web link (en.wikipedia.org)
 (TXT) w3m dump (en.wikipedia.org)
        
       | discardable_dan wrote:
       | Unfortunately, this entire field has been superseded by LLMs.
       | They are so much more-effective that it's absurd.
        
         | Smaug123 wrote:
         | 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.
        
       | marojejian wrote:
       | 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.
        
       | chilmers wrote:
       | 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 wrote:
         | 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...
        
       | coolvision wrote:
       | 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/
        
         | andoando wrote:
         | 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 wrote:
         | LLMs today still struggle to met specifications exactly, which
         | is what synthesis is good at.
        
         | the_panopticon wrote:
         | 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.
        
       | nekitamo wrote:
       | 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!
        
       ___________________________________________________________________
       (page generated 2024-04-14 23:00 UTC)