[grnnja]

What the author is getting at is a pretty cool research area called program synthesis, where the goal is to create a program that satisfies a specification.

Most techniques are essentially brute force enumeration with tricks to improve performance, so they tend to struggle to find larger programs. A lot of active research is in improving performance.

Compared to asking a LLM to write a program, program synthesis approaches will guarantee that a solution will satisfy the specification which can be very powerful.

In particular, as the author has discovered, one area where program synthesis excels is finding small intricate bitwise operator heavy programs that can be hard to reason about as a human.

The most famous example of program synthesis is Microsoft's FlashFill, which is used in Excel. You give it a few input output examples and FlashFill will try to create a small program to generalize them, and you can apply the program to more inputs, which saves you a bunch of time. An example from the paper is:

  Input -> Output

  International Business Machines -> IBM
  Principles Of Programming Languages -> POPL
  International Conference on Software Engineering -> ICSE

  String Program: Loop(\w : Concatenate(SubStr2(v_1, UpperTok, w)))

Here's a few papers:

EUSOLVER: https://www.cis.upenn.edu/~alur/Tacas17.pdf

FlashFill: https://www.microsoft.com/en-us/research/wp-content/uploads/...

BlinkFill: https://www.vldb.org/pvldb/vol9/p816-singh.pdf

Synquid: https://cseweb.ucsd.edu/~npolikarpova/publications/pldi16.pd...

[YeGoblynQueenne]

Note that FlashFill is an example of inductive program synthesis, i.e. program synthesis from an incomplete specification, e.g. one in the form of input-output examples, program traces, or natural language descriptions.

Program synthesis from a complete specification is known as deductive program synthesis and the simplest example is compilation of a program in a high-level language to a machine code. A "complete" specification is what it says on the tin: it fully specifies the program to be synthesised.

[amritananda]

Program synthesis is also pretty much equivalent to generating proofs of propositions by the Curry-Howard Isomorphism. There was a post from a few days ago about using ML to generate proofs in Lean. I'm sure there's ongoing research to do the same thing with synthesis (which imo is probably going to be more effective at pruning the search space than brute force).

[sashank_1509]

Either I have become paranoid or this feels LLM generated

[IIAOPSW]

or both