論文の概要: 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における前提選択の実践的定理証明問題について検討した。

関連論文リスト

• stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic [0.5956301166481089]
  論理式を意味的に基底としたベクトル表現(機能埋め込み)を提案する。 我々はいくつかの望ましい性質を持つ公式の連続的な埋め込みを計算する。 本稿では,学習モデル検査とニューロシンボリック・フレームワークの2つの課題において,アプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2024-05-23T10:04:56Z)
• A Recursive Bateson-Inspired Model for the Generation of Semantic Formal Concepts from Spatial Sensory Data [77.34726150561087]
  本稿では,複雑な感覚データから階層構造を生成するための記号のみの手法を提案する。 このアプローチは、概念や概念の創始の鍵としてのバテソンの差異の概念に基づいている。 このモデルは、トレーニングなしでかなりリッチだが人間に読まれる概念表現を生成することができる。
  論文  参考訳（メタデータ） (2023-07-16T15:59:13Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。 線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。 2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
  論文  参考訳（メタデータ） (2023-05-23T01:25:29Z)
• Data-driven abstractions via adaptive refinements and a Kantorovich metric [extended version] [56.94699829208978]
  本稿では,動的システムのスマートでスケーラブルな抽象化のための適応的洗練手順を提案する。 最適構造を学ぶために、マルコフ連鎖の間のカントロビッチに着想を得た計量を定義する。 本稿では,従来の線形プログラミング手法よりも計算量が多くなることを示す。
  論文  参考訳（メタデータ） (2023-03-30T11:26:40Z)
• The Many-Worlds Calculus [0.0]
  このフレームワークで計算をモデル化するための色付きPROPを提案する。 このモデルは、通常のテスト、確率的および非決定論的分岐、および量子分岐をサポートすることができる。 我々は、言語が普遍的であることを証明し、方程式理論は、この意味論に関して完備であるべきである。
  論文  参考訳（メタデータ） (2022-06-21T10:10:26Z)
• 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)
• 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)

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

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