Fugu-MT 論文翻訳(概要): JEFL: Joint Embedding of Formal Proof Libraries

論文の概要: JEFL: Joint Embedding of Formal Proof Libraries

arxiv url: http://arxiv.org/abs/2107.10188v1
Date: Wed, 21 Jul 2021 16:31:33 GMT
ステータス: 処理完了
システム内更新日: 2021-07-22 15:58:59.573309
Title: JEFL: Joint Embedding of Formal Proof Libraries
Title（参考訳）: JEFL:形式証明ライブラリの共同埋め込み
Authors: Qingxiang Wang, Cezary Kaliszyk
Abstract要約: これまでに提案したライブラリ間の概念マッチングアルゴリズムと,類似概念の検索を支援する非教師なし埋め込み手法を比較した。我々は、ニューラルネットワークの埋め込みアプローチが、よりインタラクティブな証明アシスタントに統合される可能性があると論じる。
参考スコア（独自算出の注目度）: 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.
Abstract（参考訳）: 異なる対話型証明アシスタントライブラリで使用される論理的基盤の異質性は、類似した数学的概念の発見を困難にしている。本稿では,従来提案されていたライブラリ間の概念マッチングアルゴリズムと,類似概念の検索を支援する非教師なし埋め込み手法を比較した。我々のアプローチは、Word2Vecの高速テキスト実装に基づいており、その上にツリートラバーサルモジュールを追加して、そのアルゴリズムをデータエクスポートパイプラインの表現形式に適応させる。我々は、アプローチの説明可能性、カスタマイズ性、オンライン可観測性を比較し、ニューラル埋め込みアプローチは、対話型証明アシスタントに統合される可能性が高いと主張している。

関連論文リスト

GSSF: Generalized Structural Sparse Function for Deep Cross-modal Metric Learning [51.677086019209554]
ペアワイド類似性学習のためのモダリティ間の強力な関係を捕捉する汎用構造スパースを提案する。距離メートル法は、対角線とブロック対角線の2つの形式を微妙にカプセル化する。クロスモーダルと2つの余分なユニモーダル検索タスクの実験は、その優位性と柔軟性を検証した。
論文参考訳（メタデータ） (2024-10-20T03:45:50Z)
Simbanex: Similarity-based Exploration of IEEE VIS Publications [1.9955582583198124]
本研究では,複数の埋め込みを類似性計算に用いて,バイオロメトリやサイエントメトリに適用する。 MVNを個別に埋め込み可能なアスペクトに分割することにより、類似性に基づくクラスタリングの新しい手法の入力として使用する柔軟なベクトル表現を得ることができる。これらの前処理のステップに基づいて、我々はSimbanexというビジュアル分析アプリケーションを開発し、基礎となる出版物における類似パターンのインタラクティブなビジュアル探索を目的としている。
論文参考訳（メタデータ） (2024-08-31T15:26:01Z)
Disentangling Dense Embeddings with Sparse Autoencoders [0.0]
スパースオートエンコーダ(SAE)は、複雑なニューラルネットワークから解釈可能な特徴を抽出する可能性を示している。大規模言語モデルからの高密度テキスト埋め込みに対するSAEの最初の応用の1つを提示する。その結果,解釈可能性を提供しながら意味的忠実さを保っていることが明らかとなった。
論文参考訳（メタデータ） (2024-08-01T15:46:22Z)
Finding structure in logographic writing with library learning [55.63800121311418]
書記システムにおける構造を発見するための計算フレームワークを開発する。我々の枠組みは中国語の表記体系における既知の言語構造を発見する。図書館学習のアプローチが、人間の認知における構造の形成の基盤となる基本的な計算原理を明らかにするのにどのように役立つかを実証する。
論文参考訳（メタデータ） (2024-05-11T04:23:53Z)
Deep Boosting Learning: A Brand-new Cooperative Approach for Image-Text Matching [53.05954114863596]
画像テキストマッチングのための新しいDeep Boosting Learning (DBL)アルゴリズムを提案する。アンカーブランチは、まずデータプロパティに関する洞察を提供するために訓練される。ターゲットブランチは、一致したサンプルと未一致のサンプルとの相対距離をさらに拡大するために、より適応的なマージン制約を同時に課される。
論文参考訳（メタデータ） (2024-04-28T08:44:28Z)
Relation-aware Ensemble Learning for Knowledge Graph Embedding [68.94900786314666]
我々は,既存の手法を関係性に配慮した方法で活用し,アンサンブルを学習することを提案する。関係認識アンサンブルを用いてこれらのセマンティクスを探索すると、一般的なアンサンブル法よりもはるかに大きな検索空間が得られる。本稿では,リレーショナルなアンサンブル重みを独立に検索する分割探索合成アルゴリズムRelEns-DSCを提案する。
論文参考訳（メタデータ） (2023-10-13T07:40:12Z)
Unsupervised Interpretable Basis Extraction for Concept-Based Visual Explanations [53.973055975918655]
提案手法を用いて抽出したベースに変換すると,中間層表現がより解釈可能であることを示す。提案手法は,提案手法を教師付きアプローチから抽出したベースと,教師付き手法から抽出したベースを比較した結果,教師なし手法は教師付き手法の限界を構成する強みを有し,今後の研究の方向性を示す。
論文参考訳（メタデータ） (2023-03-19T00:37:19Z)
A Proposed Conceptual Framework for a Representational Approach to Information Retrieval [42.67826268399347]
本稿では,情報検索と自然言語処理における最近の発展を理解するための概念的枠組みについて概説する。本稿では,コアテキスト検索問題を論理的スコアリングモデルと物理的検索モデルに分解する表現的アプローチを提案する。
論文参考訳（メタデータ） (2021-10-04T15:57:02Z)
PAIR: Leveraging Passage-Centric Similarity Relation for Improving Dense Passage Retrieval [87.68667887072324]
本稿では,クエリ中心とPAssage中心のsmilarity Relations(PAIR)を併用した新しい手法を提案する。本稿では,2種類の類似性関係の形式的定式化を導入することにより,3つの主要な技術的貢献を行う。 MSMARCOとNatural Questionsの両方のデータセットにおいて、従来の最先端モデルよりも大幅に優れています。
論文参考訳（メタデータ） (2021-08-13T02:07:43Z)
Ontology-based Interpretable Machine Learning for Textual Data [35.01650633374998]
本稿では,予測モデルを説明するためのサンプリング手法に基づいて,解釈可能なモデルを学習する新しい解釈フレームワークを提案する。説明のために探索空間を狭めるために,学習可能なアンカーアルゴリズムを設計する。さらに、学習された解釈可能な表現とアンカーを組み合わせることで、理解可能な説明を生成する一連の規則が導入された。
論文参考訳（メタデータ） (2020-04-01T02:51:57Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。