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

• DISRetrieval: Harnessing Discourse Structure for Long Document Retrieval [51.89673002051528]
  DISRetrieval is a novel hierarchical retrieval framework that leverages linguistic discourse structure to enhance long document understanding.<n>Our studies confirm that discourse structure significantly enhances retrieval effectiveness across different document lengths and query types.
  arXiv  Detail & Related papers  (2025-05-26T14:45:12Z)
• Semantic Correspondence: Unified Benchmarking and a Strong Baseline [14.012377730820342]
  We present the first extensive survey of semantic correspondence methods.<n>We aggregate and summarize the results of methods in literature across various benchmarks into a unified comparative table.<n>We propose a simple yet effective baseline that achieves state-of-the-art performance on multiple benchmarks.
  arXiv  Detail & Related papers  (2025-05-23T16:07:16Z)
• Scalable Multi-phase Word Embedding Using Conjunctive Propositional Clauses [14.088007380798635]
  We introduce a novel approach incorporating two-phase training to discover contextual embeddings of input sequences. This technique not only facilitates the design of a scalable model but also preserves interpretability. Our experimental findings revealed that the proposed method yields competitive performance compared to the previous approaches.
  arXiv  Detail & Related papers  (2025-01-31T10:39:04Z)
• GSSF: Generalized Structural Sparse Function for Deep Cross-modal Metric Learning [51.677086019209554]
  We propose a Generalized Structural Sparse to capture powerful relationships across modalities for pair-wise similarity learning. The distance metric delicately encapsulates two formats of diagonal and block-diagonal terms. Experiments on cross-modal and two extra uni-modal retrieval tasks have validated its superiority and flexibility.
  arXiv  Detail & Related papers  (2024-10-20T03:45:50Z)
• Simbanex: Similarity-based Exploration of IEEE VIS Publications [1.9955582583198124]
  In this work, we use multiple embeddings for similarity calculations to be applied in bibliometrics and scientometrics. By dividing our MVN into separately embeddable aspects, we are able to obtain a flexible vector representation which we use as input to a novel method of similarity-based clustering. Based on these preprocessing steps, we developed a visual analytics application, called Simbanex, that has been designed for the interactive visual exploration of similarity patterns within the underlying publications.
  arXiv  Detail & Related papers  (2024-08-31T15:26:01Z)
• Disentangling Dense Embeddings with Sparse Autoencoders [0.0]
  Sparse autoencoders (SAEs) have shown promise in extracting interpretable features from complex neural networks. We present one of the first applications of SAEs to dense text embeddings from large language models. We show that the resulting sparse representations maintain semantic fidelity while offering interpretability.
  arXiv  Detail & Related papers  (2024-08-01T15:46:22Z)
• 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)
• 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)
• 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)
• 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.