論文の概要: A Study of Continuous Vector Representationsfor Theorem Proving

• arxiv url: http://arxiv.org/abs/2101.09142v1
• Date: Fri, 22 Jan 2021 15:04:54 GMT
• ステータス: 処理完了
• システム内更新日: 2021-03-20 17:21:02.201390
• Title: A Study of Continuous Vector Representationsfor Theorem Proving
• Title（参考訳）: 定理証明のための連続ベクトル表現に関する研究
• Authors: Stanis{\l}aw Purga{\l}, Julian Parsert, Cezary Kaliszyk
• Abstract要約: 我々は,論理特性の保存と可逆性を考慮したエンコードを開発した。 これは、すべての記号を含む公式のツリー形状が密度ベクトル表現から再構築できることを意味する。 これらの構文的および意味的特性のトレーニングに使用できるデータセットを提案する。
• 参考スコア（独自算出の注目度）: 2.0518509649405106
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Applying machine learning to mathematical terms and formulas requires a suitable representation of formulas that is adequate for AI methods. In this paper, we develop an encoding that allows for logical properties to be preserved and is additionally reversible. This means that the tree shape of a formula including all symbols can be reconstructed from the dense vector representation. We do that by training two decoders: one that extracts the top symbol of the tree and one that extracts embedding vectors of subtrees. The syntactic and semantic logical properties that we aim to reserve include both structural formula properties, applicability of natural deduction steps, and even more complex operations like unifiability. We propose datasets that can be used to train these syntactic and semantic properties. We evaluate the viability of the developed encoding across the proposed datasets as well as for the practical theorem proving problem of premise selection in the Mizar corpus.
• Abstract（参考訳）: 機械学習を数学的用語や公式に適用するには、AI手法に適した公式の表現が必要である。 本稿では,論理特性を保存し,さらに可逆性を持たせるエンコーディングを開発する。 つまり、すべての記号を含む公式の木の形状は、濃密なベクトル表現から再構成できる。 これは2つのデコーダをトレーニングすることで実現します。1つは木の一番上のシンボルを抽出し、もう1つは部分木の埋め込みベクトルを抽出します。 私たちが予約しようとしている構文的および意味的論理特性には、構造的公式性、自然推論ステップの適用性、さらにユニフィラビリティのようなより複雑な操作が含まれる。 これらの構文的および意味的特性のトレーニングに使用できるデータセットを提案する。 提案したデータセット間での符号化の実現可能性と,Mizar corpusにおける前提選択の実践的定理証明問題について検討した。

関連論文リスト

• Semantic Representations of Mathematical Expressions in a Continuous Vector Space [0.0]
  連続ベクトル空間における数学的表現を表現するためのアプローチについて述べる。 我々は、視覚的に異なるが数学的に等価な表現に基づいて訓練されたシーケンス・ツー・シーケンス・アーキテクチャのエンコーダを用いて、ベクトル表現を生成する。
  論文  参考訳（メタデータ） (2022-10-08T22:33:39Z)
• Object Representations as Fixed Points: Training Iterative Refinement Algorithms with Implicit Differentiation [88.14365009076907]
  反復的洗練は表現学習に有用なパラダイムである。 トレーニングの安定性とトラクタビリティを向上させる暗黙の差別化アプローチを開発する。
  論文  参考訳（メタデータ） (2022-07-02T10:00:35Z)
• Prolog-based agnostic explanation module for structured pattern classification [2.0824228840987447]
  本稿では,Prologをベースとした推論モジュールを提案する。 また、予測されたものではなく、接地トラスラベルを使ってe-ifクエリを解決できる。 全体として、本手法は、構造化パターン分類問題に適用可能な4つの明確に定義された段階から構成される。
  論文  参考訳（メタデータ） (2021-12-23T15:28:40Z)
• Inducing Transformer's Compositional Generalization Ability via Auxiliary Sequence Prediction Tasks [86.10875837475783]
  体系的な構成性は人間の言語において必須のメカニズムであり、既知の部品の組換えによって新しい表現を作り出すことができる。 既存のニューラルモデルには、記号構造を学習する基本的な能力がないことが示されている。 本稿では,関数の進行と引数のセマンティクスを追跡する2つの補助シーケンス予測タスクを提案する。
  論文  参考訳（メタデータ） (2021-09-30T16:41:19Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。 精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。 導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
  論文  参考訳（メタデータ） (2021-07-30T08:27:15Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。 実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。 従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
  論文  参考訳（メタデータ） (2021-05-09T14:22:43Z)
• Abelian Neural Networks [48.52497085313911]
  まず、アベリア群演算のためのニューラルネットワークアーキテクチャを構築し、普遍近似特性を導出する。 連想対称の特徴づけを用いて、アベリア半群演算に拡張する。 固定単語埋め込み上でモデルをトレーニングし、元の word2vec よりも優れた性能を示す。
  論文  参考訳（メタデータ） (2021-02-24T11:52:21Z)
• Fork or Fail: Cycle-Consistent Training with Many-to-One Mappings [67.11712279612583]
  サイクル一貫性トレーニングは、2つの関心領域間の前方および逆マッピングの学習に広く用いられている。 我々は条件付き変分オートエンコーダ(cvae)アプローチを開発し、これは全射写像を暗黙の単射に変換するものと見なすことができる。 私たちのパイプラインは、グラフからテキストへの多様性を促進しながら、サイクルトレーニング中に多くのマッピングをキャプチャできます。
  論文  参考訳（メタデータ） (2020-12-14T10:59:59Z)
• Neural Proof Nets [0.8379286663107844]
  本稿では,Sinkhorn ネットワークをベースとした証明ネットのニューラルバリアントを提案する。 AEThelでは,テキスト文の正しい書き起こしを線形ラムダ計算の証明や用語として70%の精度で行うことができる。
  論文  参考訳（メタデータ） (2020-09-26T22:48:47Z)
• Building powerful and equivariant graph neural networks with structural message-passing [74.93169425144755]
  本稿では,2つのアイデアに基づいた,強力かつ同変なメッセージパッシングフレームワークを提案する。 まず、各ノードの周囲の局所的コンテキスト行列を学習するために、特徴に加えてノードの1ホット符号化を伝搬する。 次に,メッセージのパラメトリゼーション手法を提案する。
  論文  参考訳（メタデータ） (2020-06-26T17:15:16Z)
• Lattice Representation Learning [6.427169570069738]
  ユークリッド空間に埋め込まれた格子を利用する離散表現を学習するための理論とアルゴリズムを導入する。 格子表現は興味深い性質の組み合わせを持つ:a) 格子量子化を用いて明示的に計算できるが、導入したアイデアを使って効率的に学習することができる。 この記事では、トレーニングや推論時間に使用される式をリンクする新しい数学的結果や、2つの一般的なデータセットに対する実験的な検証など、最初の2つの特性を探索し、活用するための基盤の整備に焦点をあてる。
  論文  参考訳（メタデータ） (2020-06-24T16:05:11Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。