論文の概要: An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic

• arxiv url: http://arxiv.org/abs/2002.00423v2
• Date: Sun, 15 Mar 2020 16:41:53 GMT
• ステータス: 処理完了
• システム内更新日: 2023-01-04 19:58:32.352432
• Title: An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
• Title（参考訳）: 一階述語論理における自動定理証明のための公式埋め込みの実験的研究
• Authors: Ibrahim Abdelaziz, Veronika Thost, Maxwell Crouse, Achille Fokoue
• Abstract要約: 本研究では,一般的なグラフベースエンコーディングを持つ現行システムに適用されるパターンベースの埋め込みについて,実験的に比較する。 実験により、より複雑なグラフベースの埋め込みにより、より単純な実行時の符号化方式の利点が打ち消されることが示された。
• 参考スコア（独自算出の注目度）: 13.633012068936894
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated theorem proving in first-order logic is an active research area which is successfully supported by machine learning. While there have been various proposals for encoding logical formulas into numerical vectors -- from simple strings to more involved graph-based embeddings -- little is known about how these different encodings compare. In this paper, we study and experimentally compare pattern-based embeddings that are applied in current systems with popular graph-based encodings, most of which have not been considered in the theorem proving context before. Our experiments show that the advantages of simpler encoding schemes in terms of runtime are outdone by more complex graph-based embeddings, which yield more efficient search strategies and simpler proofs. To support this, we present a detailed analysis across several dimensions of theorem prover performance beyond just proof completion rate, thus providing empirical evidence to help guide future research on neural-guided theorem proving towards the most promising directions.
• Abstract（参考訳）: 一階述語論理における自動定理証明は、機械学習によって支持される活発な研究領域である。 単純な文字列からグラフベースの埋め込みまで、論理式を数値ベクトルにエンコードする様々な提案があったが、これらの異なるエンコーディングの比較についてはほとんど知られていない。 本稿では,現在のシステムで採用されているパターンベース埋め込みと,一般的なグラフベースのエンコーディングを実験的に比較する。 実験により, より複雑なグラフベースの埋め込みにより, より効率的な探索戦略とより単純な証明により, より単純な符号化方式の利点が打ち消されることが示された。 そこで本研究では,証明完了率以上の数次元の定理証明器の性能について詳細な解析を行い,最も有望な方向に向けての神経誘導定理の今後の研究を導くための実証的証拠を提供する。

関連論文リスト

• Rethinking Complex Queries on Knowledge Graphs with Neural Link Predictors [58.340159346749964]
  本稿では,証明可能な推論能力を備えた複雑なクエリを用いたエンドツーエンド学習を支援するニューラルシンボリック手法を提案する。 これまでに検討されていない10種類の新しいクエリを含む新しいデータセットを開発する。 提案手法は,新しいデータセットにおいて先行手法を著しく上回り,既存データセットにおける先行手法を同時に上回っている。
  論文  参考訳（メタデータ） (2023-04-14T11:35:35Z)
• Towards Efficient Fine-tuning of Pre-trained Code Models: An Experimental Study and Beyond [52.656743602538825]
  微調整された事前訓練されたコードモデルは、大きな計算コストを発生させる。 我々は、レイヤーワイドで事前訓練された表現と、微調整中に符号化されたコード知識に何が起こるのかを実験的に検討する。 本稿では,レイヤ凍結により事前学習したコードモデルを効率的に微調整するTellyを提案する。
  論文  参考訳（メタデータ） (2023-04-11T13:34:13Z)
• Fast Rule-Based Decoding: Revisiting Syntactic Rules in Neural Constituency Parsing [9.858565876426411]
  従来の研究では、構文規則に基づく確率論的統計手法が特に選挙区解析に有効であることが示されている。 本稿では,GPUアクセラレーションを利用した高速なCKY復号法を最初に実装し,さらに構文規則に基づく(ルール制約付き)CKY復号法を導出する。
  論文  参考訳（メタデータ） (2022-12-16T13:07:09Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Proving Theorems using Incremental Learning and Hindsight Experience Replay [45.277067974919106]
  等式のない一階述語論理のドメイン固有プローバを学習するための一般的な漸進学習アルゴリズムを提案する。 我々は、証明が見つからない場合でも学べるように、後見経験の再生を定理証明に適用する。 我々は、この方法で訓練されたプローバーがTPTPデータセットの最先端の伝統的なプローバーにマッチし、時には超えることを示した。
  論文  参考訳（メタデータ） (2021-12-20T16:40:26Z)
• Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
  TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。 我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
  論文  参考訳（メタデータ） (2021-06-07T18:35:57Z)
• Neural Proof Nets [0.8379286663107844]
  本稿では,Sinkhorn ネットワークをベースとした証明ネットのニューラルバリアントを提案する。 AEThelでは,テキスト文の正しい書き起こしを線形ラムダ計算の証明や用語として70%の精度で行うことができる。
  論文  参考訳（メタデータ） (2020-09-26T22:48:47Z)
• Learning Reasoning Strategies in End-to-End Differentiable Proving [50.9791149533921]
  条件付き定理プローバーは勾配に基づく最適化により最適規則選択戦略を学習する。 条件付き定理プローサは拡張性があり、CLUTRRデータセット上で最先端の結果が得られることを示す。
  論文  参考訳（メタデータ） (2020-07-13T16:22:14Z)
• Approximation Algorithms for Sparse Principal Component Analysis [57.5357874512594]
  主成分分析(PCA)は、機械学習と統計学において広く使われている次元削減手法である。 スパース主成分分析(Sparse principal Component Analysis)と呼ばれる,スパース主成分負荷を求める様々な手法が提案されている。 本研究では,SPCA問題に対するしきい値の精度,時間,近似アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2020-06-23T04:25:36Z)
• Option Discovery in the Absence of Rewards with Manifold Analysis [16.260113196512865]
  我々は、特定の報酬やタスクの割り当てにアクセスできることなく、体系的にオプションを発見できるアルゴリズムを導出する。 従来の手法とは対照的に,本アルゴリズムはグラフラプラシアンのスペクトルをフル活用する。
  論文  参考訳（メタデータ） (2020-03-12T16:14:24Z)

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

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