5 ms·

Maciej Bendkowski has some related work [1] on generating random lambda terms, but was unable to overcome what he calls the asymptotic sparsity problem: Samp

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 closed, is at the same time (simply) typeable. [...] Asymptotic sparsity of simply-typed λ-terms is an impenetrable barrier to rejection sampling techniques. As the term size tends to infinity, so does the induced rejection overhead. In order to postpone this inevitable obstacle, it is possible to use dedicated mechanisms interrupting the sampler as soon as it is clear that the partially generated term cannot be extended to a typeable one. The current state-of-the-art samplers take this approach, combining Boltzmann models with modern logic programming execution engines backed by highly-optimised unification algorithms. Nonetheless, even with these sophisticated optimisations, such samplers are not likely to generate terms of sizes larger than one hundred. I would be curious to see a more rigorous analysis of the sample complexity of generating well-typed expressions in, e.g., the STLC. Maybe there is a way to avoid or reduce the rejection rate before evaluation. [1]: https://arxiv.org/pdf/2005.08856 https://arxiv.org/pdf/2005.08856

nextos 2y ago
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.2022.0050 https://royalsocietypublishing.org/doi/full/10.1098/rsta.202.... [2] https://dl.acm.org/doi/abs/10.1145/2980983.2908093 https://dl.acm.org/doi/abs/10.1145/2980983.2908093
- tomsmeding 2y ago
  Another relevant publication in this line of research: https://dl.acm.org/doi/10.1145/3632919 https://dl.acm.org/doi/10.1145/3632919
- bmc7505 2y ago
  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).
  - YeGoblynQueenne 2y ago
    >> 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.
- YeGoblynQueenne 2y ago
  >> 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.html 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/ https://github.com/logic-and-learning-lab/Popper/ Or Louise (mine): https://github.com/stassa/louise 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.
  - nextos 2y ago
    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.
6gvONxR4sf7o 2y ago
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.

nextos 2y ago

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.2022.0050 https://royalsocietypublishing.org/doi/full/10.1098/rsta.202.... [2] https://dl.acm.org/doi/abs/10.1145/2980983.2908093 https://dl.acm.org/doi/abs/10.1145/2980983.2908093

tomsmeding 2y ago
Another relevant publication in this line of research: https://dl.acm.org/doi/10.1145/3632919 https://dl.acm.org/doi/10.1145/3632919
bmc7505 2y ago
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).
- YeGoblynQueenne 2y ago
  >> 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.
YeGoblynQueenne 2y ago
>> 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.html 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/ https://github.com/logic-and-learning-lab/Popper/ Or Louise (mine): https://github.com/stassa/louise 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.
- nextos 2y ago
  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.

6gvONxR4sf7o 2y ago

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.