論文の概要: 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の高速テキスト実装に基づいており、その上にツリートラバーサルモジュールを追加して、そのアルゴリズムをデータエクスポートパイプラインの表現形式に適応させる。
我々は、アプローチの説明可能性、カスタマイズ性、オンライン可観測性を比較し、ニューラル埋め込みアプローチは、対話型証明アシスタントに統合される可能性が高いと主張している。
関連論文リスト
- Tracing the Genealogies of Ideas with Large Language Model Embeddings [0.0]
大規模コーパスにまたがる知的影響を検出する新しい手法を提案する。
この手法を用いて、19世紀の約40万冊のノンフィクション書籍と学術出版物のコーパスから文章をベクトル化する。
論文 参考訳(メタデータ) (2024-01-13T18:42:27Z) - Relation-aware Ensemble Learning for Knowledge Graph Embedding [68.94900786314666]
我々は,既存の手法を関係性に配慮した方法で活用し,アンサンブルを学習することを提案する。
関係認識アンサンブルを用いてこれらのセマンティクスを探索すると、一般的なアンサンブル法よりもはるかに大きな検索空間が得られる。
本稿では,リレーショナルなアンサンブル重みを独立に検索する分割探索合成アルゴリズムRelEns-DSCを提案する。
論文 参考訳(メタデータ) (2023-10-13T07:40:12Z) - Multimodal Relation Extraction with Cross-Modal Retrieval and Synthesis [89.04041100520881]
本研究は,対象物,文,画像全体に基づいて,テキストおよび視覚的証拠を検索することを提案する。
我々は,オブジェクトレベル,画像レベル,文レベル情報を合成し,同一性と異なるモダリティ間の推論を改善する新しい手法を開発した。
論文 参考訳(メタデータ) (2023-05-25T15:26:13Z) - Unsupervised Interpretable Basis Extraction for Concept-Based Visual
Explanations [53.973055975918655]
提案手法を用いて抽出したベースに変換すると,中間層表現がより解釈可能であることを示す。
提案手法は,提案手法を教師付きアプローチから抽出したベースと,教師付き手法から抽出したベースを比較した結果,教師なし手法は教師付き手法の限界を構成する強みを有し,今後の研究の方向性を示す。
論文 参考訳(メタデータ) (2023-03-19T00:37:19Z) - Relational Sentence Embedding for Flexible Semantic Matching [86.21393054423355]
文埋め込みの可能性を明らかにするための新しいパラダイムとして,文埋め込み(Sentence Embedding, RSE)を提案する。
RSEは文関係のモデル化に有効で柔軟性があり、一連の最先端の埋め込み手法より優れている。
論文 参考訳(メタデータ) (2022-12-17T05:25:17Z) - UnifieR: A Unified Retriever for Large-Scale Retrieval [84.61239936314597]
大規模な検索は、クエリを与えられた巨大なコレクションから関連ドキュメントをリコールすることである。
事前学習型言語モデル(PLM)に基づく最近の検索手法は,高密度ベクターあるいはレキシコンに基づくパラダイムに大別することができる。
本論文では,高密度ベクトルとレキシコンに基づく検索を2つの表現能力を持つ1つのモデルで統合する学習フレームワークUnifieRを提案する。
論文 参考訳(メタデータ) (2022-05-23T11:01:59Z) - Suggesting Relevant Questions for a Query Using Statistical Natural
Language Processing Technique [0.0]
ユーザクエリに対する同様の質問の推奨には、EコマースWebサイトのユーザの検索時間短縮、企業の従業員のトレーニング、学生の全体学習など、多くのアプリケーションがある。
同様の疑問を提起するために自然言語処理技術が使われているのは、既存のアーキテクチャ上で一般的である。
論文 参考訳(メタデータ) (2022-04-26T04:30:16Z) - A Proposed Conceptual Framework for a Representational Approach to
Information Retrieval [42.67826268399347]
本稿では,情報検索と自然言語処理における最近の発展を理解するための概念的枠組みについて概説する。
本稿では,コアテキスト検索問題を論理的スコアリングモデルと物理的検索モデルに分解する表現的アプローチを提案する。
論文 参考訳(メタデータ) (2021-10-04T15:57:02Z) - Imposing Relation Structure in Language-Model Embeddings Using
Contrastive Learning [30.00047118880045]
グラフ構造における関係をエンコードするために文埋め込みを訓練する新しいコントラスト学習フレームワークを提案する。
結果として得られた関係認識文の埋め込みは、関係抽出タスクにおける最先端の結果を得る。
論文 参考訳(メタデータ) (2021-09-02T10:58:27Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。