JEFL: Joint Embedding of Formal Proof Libraries
- URL: http://arxiv.org/abs/2107.10188v1
- Date: Wed, 21 Jul 2021 16:31:33 GMT
- Title: JEFL: Joint Embedding of Formal Proof Libraries
- Authors: Qingxiang Wang, Cezary Kaliszyk
- Abstract summary: We compare a previously proposed algorithm for matching concepts across libraries with our unsupervised embedding approach that can help us retrieve similar concepts.
We argue that the neural embedding approach has more potential to be integrated into an interactive proof assistant.
- Score: 2.423990103106667
- License: http://creativecommons.org/licenses/by/4.0/
- 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.
Related papers
- Ensuring Responsible Sourcing of Large Language Model Training Data Through Knowledge Graph Comparison [0.0]
Recently, publishers, newspapers, and other creators of copyrighted corpora against large language model (LLM) developers have been accused of plagiarism.
We propose a novel system, a variant of a plagiarism detection system, that assesses whether a knowledge source has been used in the training or fine-tuning of a large language model.
arXiv Detail & Related papers (2024-07-02T20:49:21Z) - Finding structure in logographic writing with library learning [55.63800121311418]
We develop a computational framework for discovering structure in a writing system.
Our framework discovers known linguistic structures in the Chinese writing system.
We demonstrate how a library learning approach may help reveal the fundamental computational principles that underlie the creation of structures in human cognition.
arXiv Detail & Related papers (2024-05-11T04:23:53Z) - Deep Boosting Learning: A Brand-new Cooperative Approach for Image-Text Matching [53.05954114863596]
We propose a brand-new Deep Boosting Learning (DBL) algorithm for image-text matching.
An anchor branch is first trained to provide insights into the data properties.
A target branch is concurrently tasked with more adaptive margin constraints to further enlarge the relative distance between matched and unmatched samples.
arXiv Detail & Related papers (2024-04-28T08:44:28Z) - Tracing the Genealogies of Ideas with Large Language Model Embeddings [0.0]
I present a novel method to detect intellectual influence across a large corpus.
I apply this method to vectorize sentences from a corpus of roughly 400,000 nonfiction books and academic publications from the 19th century.
arXiv Detail & Related papers (2024-01-13T18:42:27Z) - Relation-aware Ensemble Learning for Knowledge Graph Embedding [68.94900786314666]
We propose to learn an ensemble by leveraging existing methods in a relation-aware manner.
exploring these semantics using relation-aware ensemble leads to a much larger search space than general ensemble methods.
We propose a divide-search-combine algorithm RelEns-DSC that searches the relation-wise ensemble weights independently.
arXiv Detail & Related papers (2023-10-13T07:40:12Z) - Description-Based Text Similarity [59.552704474862004]
We identify the need to search for texts based on abstract descriptions of their content.
We propose an alternative model that significantly improves when used in standard nearest neighbor search.
arXiv Detail & Related papers (2023-05-21T17:14:31Z) - Unsupervised Interpretable Basis Extraction for Concept-Based Visual
Explanations [53.973055975918655]
We show that, intermediate layer representations become more interpretable when transformed to the bases extracted with our method.
We compare the bases extracted with our method with the bases derived with a supervised approach and find that, in one aspect, the proposed unsupervised approach has a strength that constitutes a limitation of the supervised one and give potential directions for future research.
arXiv Detail & Related papers (2023-03-19T00:37:19Z) - Suggesting Relevant Questions for a Query Using Statistical Natural
Language Processing Technique [0.0]
Suggesting similar questions for a user query has many applications ranging from reducing search time of users on e-commerce websites, training of employees in companies to holistic learning for students.
The use of Natural Language Processing techniques for suggesting similar questions is prevalent over the existing architecture.
arXiv Detail & Related papers (2022-04-26T04:30:16Z) - A Proposed Conceptual Framework for a Representational Approach to
Information Retrieval [42.67826268399347]
This paper outlines a conceptual framework for understanding recent developments in information retrieval and natural language processing.
I propose a representational approach that breaks the core text retrieval problem into a logical scoring model and a physical retrieval model.
arXiv Detail & Related papers (2021-10-04T15:57:02Z) - PAIR: Leveraging Passage-Centric Similarity Relation for Improving Dense
Passage Retrieval [87.68667887072324]
We propose a novel approach that leverages query-centric and PAssage-centric sImilarity Relations (called PAIR) for dense passage retrieval.
To implement our approach, we make three major technical contributions by introducing formal formulations of the two kinds of similarity relations.
Our approach significantly outperforms previous state-of-the-art models on both MSMARCO and Natural Questions datasets.
arXiv Detail & Related papers (2021-08-13T02:07:43Z) - Ontology-based Interpretable Machine Learning for Textual Data [35.01650633374998]
We introduce a novel interpreting framework that learns an interpretable model based on sampling technique to explain prediction models.
To narrow down the search space for explanations, we design a learnable anchor algorithm.
A set of regulations is further introduced, regarding combining learned interpretable representations with anchors to generate comprehensible explanations.
arXiv Detail & Related papers (2020-04-01T02:51:57Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.