Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Discovering algorithms by enumerating terms in Haskell

twitter.com

Post reply on HN
Print view View original

31–40 of 50 posts

Re: Discovering algorithms by enumerating terms in Haskell

#31

Post by amritananda »

grnnja wrote: post #25

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 appr…

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

Re: Discovering algorithms by enumerating terms in Haskell

#32

Post by YeGoblynQueenne »

nextos wrote: post #18
bmc7505 wrote: post #13

Maciej Bendkowski has some related work [1] on generating random lambda terms, but was unable to overcome what he calls the asymptotic sparsity problem: Sampling simply-typed terms seems notoriously more challenging than sampling closed ones. Even rejection sampling, whenever applicable, admits serious limitations due to the imminent asymptotic sparsity problem — asymptotically almost no term, be it either plain or c…

There are quite a few publications that explore the concept of generating programs, either using typed or untyped functional languages. For example, wake-sleep learning and NN on a Lisp-like language [1] or synthesis of Haskell guided by refinement types [2]. [1] https://royalsocietypublishing.org/doi/full/10.1098/rsta.202... . [2] https://dl.acm.org/doi/abs/10.1145/2980983.2908093

>> There are quite a few publications that explore the concept of generating programs, either using typed or untyped functional languages.

That's Inductive Functional Programming (IFP), a kind of Inductive Programming that also includes Inductive Logic Programming (ILP). The canonical example of IFP is Magic Haskeller:

https://nautilus.cs.miyazaki-u.ac.jp/~skata/MagicHaskeller.h...

As an example of a modern ILP I suggest Popper:

https://github.com/logic-and-learning-lab/Popper/

Or Louise (mine):

https://github.com/stassa/louise

One of the DreamCoder papers describes Inductive Programming as a form of weakly supervised learning, in the sense that such systems learn to generate programs not from examples of programs, but from examples of the target programs' beuav908rs, i.e. their inputs and outputs. By contrast LLMs or slightly older neural program synthesis systems are trained on examples that consist of pairs of (programming-task, program-solving-the-task).

Another way to see the difference between Inductive Programming systems and conventional machine learning systems used for program synthesis is that Inductive Programming systems learn by solving problems rather than from observing solutions.

The advantage is that, in this way, we can learn programs that we don't know how to write (because we don't have to generate examples of such programs) whereas with conventional machine learning we can only generate programs like the ones the system's been trained on before.

Another advantage is that it's much easier to generate examples. For instance, if I want to learn a program that reverses a list, I give some examples of lists and their reverse, e.g. reverse([a,b,c],[c,b,a]) and reverse([1,2,3],[3,2,1]) whereas e.g. an LLM must be trained on explicit examples of list-reversing programs; like, their source code.

IFP and ILP systems are also very sample efficient, so they only need a handful of examples, often just one, whereas neural net-based systems may need millions (no exaggeration- can give a ref if needed).

The disadvantage is that learning a program usually (but not always - see Louise, above) implies searching a very large combinatorial space and that can get very expensive, very, very fast. But, there are ways around that.

Re: Discovering algorithms by enumerating terms in Haskell

#33

Post by YeGoblynQueenne »

bmc7505 wrote: post #23
nextos wrote: post #18

Earlier quoted context omitted.

There are quite a few publications that explore the concept of generating programs, either using typed or untyped functional languages. For example, wake-sleep learning and NN on a Lisp-like language [1] or synthesis of Haskell guided by refinement types [2]. [1] https://royalsocietypublishing.org/doi/full/10.1098/rsta.202... . [2] https://dl.acm.org/doi/abs/10.1145/2980983.2908093

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 enjo…

>> The trick is not just synthesizing valid functions, but doing so in a parallel communication-free manner, without compromising soundness or completeness.

Right! A great way to do this is to learn a program by using it to prove the training examples while it is being learned. A very cool ability that some systems of the new wave of Inductive Logic Programming can pull off, but probably nothing else can far as I can tell.

Re: Discovering algorithms by enumerating terms in Haskell

#34

Post by 6gvONxR4sf7o »

bmc7505 wrote: post #13

Maciej Bendkowski has some related work [1] on generating random lambda terms, but was unable to overcome what he calls the asymptotic sparsity problem: Sampling simply-typed terms seems notoriously more challenging than sampling closed ones. Even rejection sampling, whenever applicable, admits serious limitations due to the imminent asymptotic sparsity problem — asymptotically almost no term, be it either plain or c…

I did some work on this about a decade ago, using RL on STLC, and that was the same problem I faced. It’s too bad so few well typed expression trees are very useful programs.

Re: Discovering algorithms by enumerating terms in Haskell

#35

Post by cvoss »

Did you know that there is an efficient algorithm for learning (guessing) a regular language from a series of examples/non-examples? Basically, you directly construct the smallest automaton that correctly discriminates the training inputs. It's Dana Angluin's L* algorithm.

The technique generalizes to finite tree automata, meaning you can discover generators of simple expression grammars, given examples/non-examples.

So if you can construe your problem as a labeled tree recognition problem, assuming it's solvable using a finite tree automaton, then you can discover the algorithm for it efficiently.

For example, if you have three strings of bits (2 inputs and 1 output) and line them up as a single string of triplets of bits, it does not surprise me that it is easy to discover the automaton state transition rules that give you the carry bit for each triple and tell you when to reject the triple because the output bit is not correct for the two input bits.

The author has arranged the problem this way when sketching the ADC template and has also jump-started the search by assuming the solution space includes exactly one output bit for each pair of input bits. (That may seem like an obvious necessity, but that is a constraint which is not required by the tree automaton formulation, which need not differentiate "inputs" and "outputs".)

Re: Discovering algorithms by enumerating terms in Haskell

#36

Post by sashank_1509 »

grnnja wrote: post #25

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 appr…

Either I have become paranoid or this feels LLM generated

Re: Discovering algorithms by enumerating terms in Haskell

#37

Post by IIAOPSW »

sashank_1509 wrote: post #36
grnnja wrote: post #25

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 appr…

Either I have become paranoid or this feels LLM generated

or both

Re: Discovering algorithms by enumerating terms in Haskell

#38

Post by trenchgun »

kccqzy wrote: post #6

I don't think the original submission has enough details for us to reproduce or even understand what's being done. Omega monad is just a diagonal search monad that supports infinity. I don't understand the syntax in the screenshot. What's the type of the terms being enumerated? I can see lambda, but what's @inc or the pluses and minuses?

Yeah, also the submission headline is wrong. He was using Haskell only for the toy example. He is using HVM for the actual Discrete Program Search. See also the follow up post: https://x.com/VictorTaelin/status/1819774880130158663

Re: Discovering algorithms by enumerating terms in Haskell

#40

Post by nextos »

YeGoblynQueenne wrote: post #32
nextos wrote: post #18

Earlier quoted context omitted.

There are quite a few publications that explore the concept of generating programs, either using typed or untyped functional languages. For example, wake-sleep learning and NN on a Lisp-like language [1] or synthesis of Haskell guided by refinement types [2]. [1] https://royalsocietypublishing.org/doi/full/10.1098/rsta.202... . [2] https://dl.acm.org/doi/abs/10.1145/2980983.2908093

>> There are quite a few publications that explore the concept of generating programs, either using typed or untyped functional languages. That's Inductive Functional Programming (IFP), a kind of Inductive Programming that also includes Inductive Logic Programming (ILP). The canonical example of IFP is Magic Haskeller: https://nautilus.cs.miyazaki-u.ac.jp/~skata/MagicHaskeller.h... As an example of a modern ILP I sug…

Thanks, I know ILP quite well and also your research, Muggleton et al, etc.

It is a very interesting field which I hope makes a comeback once systems become neurosymbolic.

Post reply on HN