mlsanityData to 13 Oct 2026

JEFL: Joint Embedding of Formal Proof Libraries

arXiv 2107.10188 ↗First posted 21 Jul 2021cs.LO cs.CL cs.LGcited by 0

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. No citing papers in the map yet (data through 13 Oct 2026). Builds on 12 of its 37 references that are in the map. First posted on arXiv 21 Jul 2021.

Builds on

12 of 37 references.

References · 12

  1. 2013Efficient Estimation of Word Representations in Vector Spacecited by 4,360
  2. 2013Distributed Representations of Words and Phrases and their Compositionalitycited by 3,467
  3. 2016node2vec: Scalable Feature Learning for Networkscited by 1,915
  4. 2016Enriching Word Vectors with Subword Informationcited by 1,581
  5. 2014DeepWalk: Online Learning of Social Representationscited by 1,544
  6. 2016Bag of Tricks for Efficient Text Classificationcited by 872
  7. 2013HOL(y)Hammer: Online ATP Service for HOL Lightcited by 8
  8. 2015Sharing HOL4 and HOL Light proof knowledgecited by 4
  9. 2013Lemma Mining over HOL Lightcited by 3
  10. 2013The MMT API: A Generic MKM Systemcited by 1
  11. 2014Proof Pattern Search in Coq/SSReflectcited by 1
  12. 2014Matching concepts across HOL librariescited by 1

Built on by

Not cited yet.