Representation learning or Vector Embedding

[siddhartha-gadgil]

There are many ways in which, given a (weighted) collection of linear terms, we can generate weighted graphs. Namely, we traverse based on:

• combinations of terms: function application, lambdas etc.
• terms joined to their types.
• alternatively, terms mapped to types to give relations between types only.
• ordering, sectioning etc of sources.

Each of these give representations of terms and types as vectors. We can use these for various decisions and maps, e.g.

• deciding whether a statement is a priori likely to be true - so we can recognize strong statements.
• map statements to likely ingredients in their proofs.
• basic evaluation of a statement, better than just complexity.

[siddhartha-gadgil]

Bird2Vec lessons:

• no magic in word2vec;
• should first of all use type information;
• should learn vectors with actual predictions, first, not synthetic ones.

[siddhartha-gadgil]

Is not really an issue, but part of better learning and dynamics.

[siddhartha-gadgil]

• This is now ready for implementation given the generation of equation terms.
• We don't need to use predictions but can use actual nodes that are constructed.
• Key cost: discriminate between existing and non-existing nodes that are equation terms for the given node.
• Islands: Can model mapping into islands by a low rank linear map plus a scalar multiple of the identity.
• Given a new term we can simply learn afresh starting with the state we had already learnt.

[siddhartha-gadgil]

• Simplify: just use some form of force-directed graph.
• This is not representation learning, just a simple form of Vector embedding

[siddhartha-gadgil]

Can use bi-directional flows as in #256

[siddhartha-gadgil]

This has been implemented a while ago as RepresentationLearner, but

• we must test.
• we may want bi-directional flows for robustness.

[siddhartha-gadgil]

code2vec may be directly applicable here.

[siddhartha-gadgil]

• The transformer approach may be much better.
• It lets us avoid unnatural linearizations; we can use positional embeddings based on representations in place of trignometric functions, for example.

[siddhartha-gadgil]

Representations: force directed

• We represent elements using a force-directed model, based either on explicit forces or predictions.
• If we use predictions, then positive and negative samples correspond to attractive and repulsive forces.
• We can have a single repulsive force based on distance of points in the representation, stronger when they are close.
• We have a norm, essentially a descriptive complexity, on elements.
• Elements with small descriptive complexity are attracted to the origin.
• We get a similar attraction between the lhs and rhs of relations when the other terms have smaird attll complexity.
• A third attractive force depends on the representations: essentially if the representations of f and g are close and so are those of x and y, then there is an attraction between f(x) and g(y).
• We have a variant of the above where we consider projections and have attractions if these are small, but should be a projected attraction.

[siddhartha-gadgil]

Representations: Use predictions and dot products

• A model where we learnt two representations and predicted with dot products was not much worse than force-directed.
• On the other hand, this needs far fewer choices.
• Hence it is probably best to go with this.