I think your uncertainty stems from a very basic uncertainty at the base of this whole operation. What exactly makes one program "more likely" than another for the purposes of search & synthesis is a wide open question, and one to which I do not have a satisfactory answer. What I can do, however, is outline the general framework within which I am currently trying to answer that question.
First of all, yes, I am using almost exactly the same set up that Will & Greg are in that demonstration. An RNN only processes inputs and gives us a simple output, like a score. When people do things like sentence generation with RNNs, they augment the basic RNN model with some kind of search, often some kind of beam search, that incorporates the RNN as a scoring function to arrive at a high-scoring sentence. So what I am doing is really just replacing that beam search component with the barliman architecture from the demo. Barliman already does search over programs, and the RNN component is just being used here to add heuristic scores to that search and change its order. I am not doing an RNN program synthesis generation operation separate from/outside of the Barliman search. The RNN, again, is just a heuristic scoring function. As for how to actually build that function, that is what I don't yet know precisely for the new approach I am trying. At one extreme, you could imagine a simple dictionary where we take the input & output from (append '() '(a)) -> '(a), synthesize a program the normal way, and then memoize it so that if we ever run that exact query again, we can just look up the program we synthesized last time. To get less extreme, and more useful, we want to be able to, for instance, extract features from the input and output, such as list-typed, empty, length-1, etc etc, and use those to predict that certain elements of the synthesized program are more or less likely based on the relations between the input and output. The hoped for result is the "scoring function" described above that just guides the usual Barliman search to try first the combinations more likely to result from the features of the inputs and outputs. So, if input and output are all lists, car and cdr may be more likely to show up in the program relating them than +. This is a long way form a workable sketch of how to actually do this, but I hope this at least goes somewhat to your questions about how the learning and the Barliman search could all fit together, and how we can start to define something like a heuristic for "correct" programs. Evan On Sat, Sep 9, 2017 at 11:44 AM, Timothy Washington <[email protected]> wrote: > As a layman, I need to step back and understand the metaphor of how RNNs > can help generate programs. When I think through the metaphor for this > approach, given some embeddings, and training data, an RNN can learn the > most likely pattern sequence, given prior observed activity. I understand > Barliman's core problem to be how to search a space of symbols, and arrange > their construction, which yields "correct" programs. > > Investigating RNNs as a way to search that space either by > > - predicting (or generating) a series (or composition) of symbols > - sequence-sequence translation, like language , taking a > specification and translating that into an arrangement of symbols > > What I'm struggling with, is what arbitrates truth. Ie *(if (null? a)* can > lead Barliman to synthesize *if* then *null?* then *a*. And we can use an > RNN to synthesize this. But how does Barliman know to fork on that truth > value in the first place ? One thing we can say is that generated programs > are more correct, the closer they come to meeting a specification, under > all inputs. Presumably we're passing in logic expressions, which translate > to the synthesized code? And we can use generative testing to gain > confidence in the properties of the code? > > So I'm searching for the most useful abstraction. How do we judge the > correctness of the arrangement of symbols , given some logic expression, as > specification? My understanding of your approach is that you're looking for > likely symbols, given the distribution over some context syntax in the > environment. > > Ie, > > - This approach can learn the prior that *"null?" is common inside an > "if," * > - but we would really like to *extract from the "if" context, the fact > that we need to generate an expression that evaluates to true or false* > - *and has an empty list available at the top of the environment, > which should make null? very likely. * > - *Moreover, since the standard lisp "if" is actually choosing > between false and not false, you could think about the probability > 1-p(false) etc. * > - *Essentially, we end up wanting as general a way as possible to end > up with **some kind of distribution over the syntax conditioned on the > current environment**, whether it contains **ground values** or > **constrained > logic variables**. * > > > I like the "*likely symbols, given the distribution over some context > syntax in the environment*" approach, if I've understood that correctly. > > - Are you using the specification William Byrd and Greg Rosenblatt > showed here <https://www.youtube.com/watch?v=er_lLvkklsk>? > - And how are you judging correctness of each arrangement of symbols, > and the entire program? Maybe "i. a* distribution, over ii. the > arangement of symbols iii. conditioned on the current environment*" > can lead to a fitness score, for a given query? Ie, the top-level and > subsequent logic expressions generate queries describing what satisfies > each one. Then single symbols and compositions of symbols produce a score > measuring how well they match the query. "*As long as we can define > derivatives through the operations, the program’s output is differentiable > with respect to the probabilities. We can then define a loss, and train the > neural net to produce programs that give the correct answer*" (from > here <https://distill.pub/2016/augmented-rnns/#neural-programmer>). > - I'm just thinking out loud there. The core question is what is > the correctness, or fitness test? > > > Tim Washington > Interruptsoftware.com <http://interruptsoftware.com> > 415.283.8889 <(415)%20283-8889> > > > On Mon, Sep 4, 2017 at 2:14 PM, Apocalypse Mystic < > [email protected]> wrote: > >> Yeah, so some of the Barliman systems always assemble programs in the >> same order. Eg, to synthesize (if (null? a) ... it might always synthesize >> if then null? then a, which means we can use a standard RNN type approach >> that just summarizes if+null? when generating a. There are a couple >> subtleties, including differentiating between (list list) and (list >> (list)), and the fact that, depending on how you write the interpreter, >> either "if" or "(null? a)" might be generated first, so you can't >> necessarily just read training data left to right, but neither of these is >> a show stopper and you can definitely get a system to work with this >> approach. >> >> The less-than-satisfactory part of this approach is that it never looks >> at the actual values we have in the interpreter. This approach can learn >> the prior that "null?" is common inside an "if," but we would really like >> to extract from the "if" context the fact that we need to generate an >> expression that evaluates to true or false, and has an empty list available >> at the top of the environment, which should make null? very likely. >> Moreover, since the standard lisp "if" is actually choosing between false >> and not false, you could think about the probability 1-p(false) etc. >> Essentially, we end up wanting as general a way as possible to end up with >> some kind of distribution over the syntax conditioned on the current >> environment, whether it contains ground values or constrained logic >> variables. >> >> I don't have a clear sense of how to do that as a learning problem right >> now, but I am working on modifications to the constraint system to try to >> get the right information to the right part of the interpreter at the right >> time so that I can start to think about how to learn it. >> >> Evan >> > -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/minikanren. For more options, visit https://groups.google.com/d/optout.
