Discovering algorithms by enumerating terms in Haskell

It will just return the smallest function that passes your tests.

It works by enumerating ALL possible functions and running them. Obviously, that naive approach is exponential, so, the entire point is whether we can apply some clever tricks (based on optimal evaluators) to make this search "slightly less intractable".

So, to answer your question directly: if you asked it to design a prime number generator, if it found anything at all, it would probably be a simple, slow trial-and-error algorithm, or something in these lines.

The trick is not just synthesizing valid functions, but doing so in a parallel communication-free manner, without compromising soundness or completeness. You want to massively scale up a discrete sampler without replacement. One very efficient way of doing this is by constructing an explicit bijection from the sample space to the integers, sampling integers, then decoding them into programs.

While this technique enjoys certain advantages, i.e., it is embarrassingly parallelizable and guaranteed to enumerate distinct solutions with a bounded delay, it also somewhat unnatural. By flattening the distribution onto the integers a la Gödel numbering, it destroys locality, does not play well with incremental decoding methods (left-to-right is currently en vogue in generative language modeling), and will fail if the sample space is uncountable.

Another key step is reducing symmetries in your sample space by quotienting it somehow (e.g., by α-equivalence). The author seems to be invoking some kind of equivalence relation by “superposition”, but the technical details here are a little fuzzy.

This problem is also closely related to model counting in the CSP literature, so a practical speedup could lead to improvements on a lot of interesting downstream benchmarks.

In general, the problem of program induction from input-output examples is not well-posed, so specialized solvers that can make stronger assumptions will usually have an advantage on domain-specific benchmarks. Most existing program synthesizers do not satisfy all of these desiderata (e.g., soundness, completeness, naturalness, incrementality).

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

William Byrd is the creator of miniKanren btw. And an HN user.

Hi LightMachine. I can't read Haskel (?). In this screenshot:

https://x.com/VictorTaelin/status/1819208143638831404/photo/...

What's the highlighted program (?) on line 1875997?