Paper: Property Preserving Embedding of First-order Logic

Stream: Machine Learning for Theorem Proving

[Jason Rute]

Property Preserving Embedding of First-order Logic, Julian Parsert, Stephanie Autherith and Cezary Kaliszyk

[Jason Rute]

I haven't read it yet, but they appeared to present on this in AITP 2019.

[Jason Rute]

Coming up with formula embeddings will be incredibly important for theorem proving. I'm starting to fully come to grips with this. I think to understand this, one can think of the analogy with text processing. For example, predict how a user will rate a movie from their IMDB review. Early last decade the state of the art was tools like TF-IDF which roughly counts the occurrences of words in the sentence (or document) and compares them to the occurrences in the dataset. There are similar tools currently being used for formulas which count the symbols or some connected groups of symbols. These don't take into account the whole formula structure. Next, came tools like recurrent neural networks, convolutional neural networks, and LSTMs. These take into account sentence structure, but again they don't take into account the meanings of the symbols except in so far as the task being trained on. This is similar to current graph neural network approaches to formulas. Finally, now the best language models are are pre-trained by training on larger datasets of sentences (e.g. wikipedia) in a self-supervised manner. For example, the goal might be just to predict the next word in a sentence. Then when one applies this to smaller datasets, like the IMBD datasets, they can "transfer" this knowledge to the smaller dataset. We are starting to see similar approaches in theorem proving and I'm excited about this. I could easily image two scenarios. One, we can basically create algorithms which explore formulas of a certain type (FOL, HOL, DTT, etc) and learn to recognize patterns that can then be applied to specific problems (even on unseen formulas). Second, we can take embeddings trained on say Coq and apply them to Lean (or vice versa). I think the similarities in the logic should make the ability to transfer embeddings quite doable.