[HN Gopher] Discovering algorithms by enumerating terms in Haskell
___________________________________________________________________
Discovering algorithms by enumerating terms in Haskell
Author : agomez314
Score : 78 points
Date : 2024-08-02 18:57 UTC (1 days ago)
(HTM) web link (twitter.com)
(TXT) w3m dump (twitter.com)
| tadfisher wrote:
| I'm confused, what is the search space? All possible functions
| from Int -> Int? And how do you verify a result is optimal across
| inputs?
| solomatov wrote:
| My guess is they sample closed lambda terms representing
| functions.
| LightMachine wrote:
| The search space I'm using is that of all functions of a given
| dependent type. That allows you to make the search space by
| using a strong enough type.
|
| For example, if you search for `Integer -> Integer -> Integer`
| function, it will consider Integers of different bit-sizes. But
| if you instead search for `[?](n: Nat). Int(n) -> Int(n) ->
| Int(n)`, you will only consider integers of the same bit-size,
| which is a much smaller space. You can make arbitrary
| restrictions to shorten your search.
| treyd wrote:
| I'm confused about what this could be, with a title as technical
| as this but being posted somewhere with the signal:noise of
| Twitter, also where I can't view it.
| 082349872349872 wrote:
| For non-twitter, I was looking the other day at
| https://reasonablypolymorphic.com/blog/syntax-guided-synthes...
| , which unfortunately points at a dead page related to
| https://sygus.org/comp/2019/ , but seems related?
| pbib wrote:
| I believe the dead link in the article is referencing this
| journal paper[1], which is an expanded version of the
| original syntax guided synthesis paper.
|
| [1] https://web.eecs.umich.edu/~weimerw/2022-481W/readings/Al
| ur1...
| 082349872349872 wrote:
| Thanks! Looks like barliman is also (like its namesake?)
| slowly progressing: https://github.com/webyrd/Barliman
| dleslie wrote:
| Might help to read some of the author's earlier work, like:
|
| https://medium.com/@maiavictor/solving-the-mystery-behind-ab...
|
| And the Omega documentation:
|
| https://hackage.haskell.org/package/control-monad-omega-0.3/...
|
| But I'll admit, I want to see a paper or code.
| mordechai9000 wrote:
| "Perhaps I'm being really naive and an exponential wall is about
| to humble (and embarrass) me."
|
| There is something fascinating and awe-inspiring about searching
| very large, enumerative datasets for useful results. Like
| wandering Borge's Library of Babel in search of not just meaning
| but something true and useful.
| kccqzy wrote:
| 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?
| garyrob wrote:
| Maybe this could be used with the Evolutionary Algorithm subset
| known as Genetic Programming, originally popularized by John Koza
| in the 80s?
| diwank wrote:
| More on the Omega monad from its author:
|
| http://web.archive.org/web/20210616105135/http://lukepalmer....
| LightMachine wrote:
| Uhm author here. Not sure why this tweet is on Hacker News, as it
| is just a non-technical "blog post". But I've posted a follow-up
| today with some code and details, if you're curious:
|
| https://x.com/VictorTaelin/status/1819774880130158663
|
| That's as much as I can share for now though
| smusamashah wrote:
| Only thing I could read (don't understand any of this
| otherwise) was that you take input pairs and you give python
| function to generate that output. Does that mean that many math
| etc problems can be just solved? What kind of python code will
| it generate to return primes?
| pyinstallwoes wrote:
| I imagine it like content addressable computation which
| implicitly means data too.
|
| Why compute anything more than once? Find by identity and
| reuse.
|
| This then opens up interesting things when applied in a
| network that can optimize pathing (like an internet, DHT-like
| overlay).
| LightMachine wrote:
| 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.
| bmc7505 wrote:
| 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 l-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
| nextos wrote:
| 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.20
| 2....
|
| [2] https://dl.acm.org/doi/abs/10.1145/2980983.2908093
| tomsmeding wrote:
| Another relevant publication in this line of research:
| https://dl.acm.org/doi/10.1145/3632919
| bmc7505 wrote:
| 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, e.g., 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 Godel 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 a-equivalence). The
| author seems to be invoking some kind of equivalence relation
| by "superposition", but the technical details are a little
| fuzzy.
|
| This problem is closely related to model counting in the CSP
| literature, so a practical speedup could lead to improvements
| on a lot of interesting benchmarks.
|
| Most existing program synthesizers do not satisfy all of
| these desiderata (soundness, completeness, naturalness,
| incrementality).
| sporkl wrote:
| This kind of reminds me of what happens when you implement an
| interpreter in a relational programming language, which lets you
| do cool stuff like generating quines by specifying that the
| program and it's output should be the same.
|
| Quick search lead to this paper which is exactly what I'm talking
| about: http://webyrd.net/quines/quines.pdf
| verdverm wrote:
| Super interesting. Sounds like the algo I created Prioritized
| Grammar Enumeration.
|
| https://seminars.math.binghamton.edu/ComboSem/worm-chiu.pge_...
|
| PGE is essentially a BFS/DFS traversal of the space of all
| formulas, by using local enumeration of the AST. The biggest
| gains where from eliminating duplicate work (commutativity /
| associativity) and not going down bad branches (too much
| complexity added for no meaningful change to output). A lot of
| overlap in ideas here, and a lot of open research questions that
| could be worked on (like can use use RL to help guide the search
| like A*). There's definitely an exponential explosion or wall as
| the AST gets wider / deeper.
|
| At one point I wrote the core algorithm in Haskell, which made it
| so much more concise and beautiful, but eventually landed on
| python https://github.com/verdverm/pypge
|
| In all of Genetic Programming / Symbolic Regression, everyone
| starts by trying to generate computer code and then switches to
| just math formula. They are different classes of problems because
| code has more "genes" and is order sensitive, whereas math is not
| jmull wrote:
| It's kind of vague, but... it sounds like this is essentially a
| breadth first search (where the graph being searched is
| represented by a grammar)?
|
| Hard to tell.
| grnnja wrote:
| 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...
___________________________________________________________________
(page generated 2024-08-03 23:00 UTC)