JEFL: Joint Embedding of Formal Proof Libraries

TL;DR

This paper introduces JEFL, a neural embedding method for matching similar concepts across different formal proof libraries, addressing heterogeneity issues in logical foundations.

Contribution

It presents an unsupervised embedding approach based on fasttext and tree traversal, improving concept retrieval across proof libraries.

Findings

Embedding approach outperforms previous algorithms in concept matching

Neural embeddings offer better explainability and customizability

Potential for integration into interactive proof assistants

Abstract

The heterogeneous nature of the logical foundations used in different interactive proof assistant libraries has rendered discovery of similar mathematical concepts among them difficult. In this paper, we compare a previously proposed algorithm for matching concepts across libraries with our unsupervised embedding approach that can help us retrieve similar concepts. Our approach is based on the fasttext implementation of Word2Vec, on top of which a tree traversal module is added to adapt its algorithm to the representation format of our data export pipeline. We compare the explainability, customizability, and online-servability of the approaches and argue that the neural embedding approach has more potential to be integrated into an interactive proof assistant.