論文の概要: ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)

• arxiv url: http://arxiv.org/abs/2002.05406v2
• Date: Tue, 28 Apr 2020 13:59:26 GMT
• ステータス: 処理完了
• システム内更新日: 2023-01-01 09:35:59.684296
• Title: ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
• Title（参考訳）: ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (システム記述)
• Authors: Jan Jakub\r{u}v, Karel Chvalovsk\'y, Miroslav Ol\v{s}\'ak, Bartosz Piotrowski, Martin Suda, Josef Urban
• Abstract要約: 本稿では,飽和式自動定理証明器の勾配押し上げと神経誘導の実装について述べる。 勾配ブースティング法では、論理式のアリティに基づく符号化を考慮し、手動で抽象的な特徴を生成できる。 ニューラルネットワークでは,シンボルに依存しないグラフニューラルネットワーク(GNN)と,その用語や節の埋め込みを用いる。
• 参考スコア（独自算出の注目度）: 0.4893345190925177
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems. For the gradient-boosting guidance, we manually create abstracted features by considering arity-based encodings of formulas. For the neural guidance, we use symbol-independent graph neural networks (GNNs) and their embedding of the terms and clauses. The two methods are efficiently implemented in the E prover and its ENIGMA learning-guided framework. To provide competitive real-time performance of the GNNs, we have developed a new context-based approach to evaluation of generated clauses in E. Clauses are evaluated jointly in larger batches and with respect to a large number of already selected clauses (context) by the GNN that estimates their collectively most useful subset in several rounds of message passing. This means that approximative inference rounds done by the GNN are efficiently interleaved with precise symbolic inference rounds done inside E. The methods are evaluated on the MPTP large-theory benchmark and shown to achieve comparable real-time performance to state-of-the-art symbol-based methods. The methods also show high complementarity, solving a large number of hard Mizar problems.
• Abstract（参考訳）: 本稿では,問題間の一貫したシンボル名に依存しない飽和式自動定理証明器の勾配促進と神経誘導の実装について述べる。 グラデーションブースティングガイダンスでは,数式のarityに基づくエンコーディングを考慮し,手作業で抽象的な特徴を創造する。 ニューラルネットワークでは,シンボルに依存しないグラフニューラルネットワーク(GNN)と,その用語や節の埋め込みを用いる。 この2つの手法はe proverとそのenigma learning-guided frameworkで効率的に実装されている。 複数ラウンドのメッセージパッシングにおいて,集合的に最も有用なサブセットを推定するGNNによって,多数の選択済みの節(コンテキスト)に対して,より大きなバッチで共同評価を行う。 これは、GNNが行った近似推論ラウンドは、E内部で行われた正確なシンボル推論ラウンドと効率よくインターリーブされ、MPTPの大規模理論ベンチマークで評価され、最先端のシンボルベース手法と同等のリアルタイム性能が得られることを示す。 これらの手法は高い相補性を示し、多くのハードミザー問題を解く。

関連論文リスト

• Efficient Graph Similarity Computation with Alignment Regularization [7.143879014059894]
  グラフ類似性計算(GSC)は、グラフニューラルネットワーク(GNN)を用いた学習に基づく予測タスクである。 適応正規化(AReg)と呼ばれる,シンプルながら強力な正規化技術によって,高品質な学習が達成可能であることを示す。 推論段階では、GNNエンコーダによって学習されたグラフレベル表現は、ARegを再度使用せずに直接類似度スコアを計算するために使用される。
  論文  参考訳（メタデータ） (2024-06-21T07:37:28Z)
• LOGIN: A Large Language Model Consulted Graph Neural Network Training Framework [30.54068909225463]
  我々は,GNN設計プロセスの合理化とLarge Language Models(LLM)の利点を活用して,下流タスクにおけるGNNの性能向上を目指す。 我々は,LLMs-as-Consultants(LLMs-as-Consultants)という新たなパラダイムを策定し,LLMとGNNを対話的に統合する。 両グラフのノード分類におけるLOGINの有効性を実証的に評価した。
  論文  参考訳（メタデータ） (2024-05-22T18:17:20Z)
• Ensemble Quadratic Assignment Network for Graph Matching [52.20001802006391]
  グラフマッチングはコンピュータビジョンやパターン認識において一般的に用いられる技法である。 最近のデータ駆動型アプローチは、グラフマッチングの精度を著しく改善した。 データ駆動手法と従来の手法の利点を組み合わせたグラフニューラルネットワーク(GNN)に基づくアプローチを提案する。
  論文  参考訳（メタデータ） (2024-03-11T06:34:05Z)
• Efficient Link Prediction via GNN Layers Induced by Negative Sampling [92.05291395292537]
  リンク予測のためのグラフニューラルネットワーク(GNN)は、緩やかに2つの広いカテゴリに分けられる。 まず、Emphnode-wiseアーキテクチャは各ノードの個別の埋め込みをプリコンパイルし、後に単純なデコーダで結合して予測を行う。 第二に、エンフェッジワイド法は、ペアワイド関係の表現を強化するために、エッジ固有のサブグラフ埋め込みの形成に依存している。
  論文  参考訳（メタデータ） (2023-10-14T07:02:54Z)
• Optimal Inference in Contextual Stochastic Block Models [0.0]
  属性グラフの教師なしコミュニティ検出のために,文脈ブロックモデル (cSBM) を提案した。 cSBMは、半教師付きノード分類のためのグラフニューラルネットワーク(GNN)の性能を評価するための合成データセットとして広く利用されている。 本稿では,本アルゴリズムが到達した精度と,本論文で提案したGNNアーキテクチャの性能との間には,かなりのギャップが存在することを示す。
  論文  参考訳（メタデータ） (2023-06-06T10:02:57Z)
• Scalable Learning of Latent Language Structure With Logical Offline Cycle Consistency [71.42261918225773]
  概念的には、LOCCOは、トレーニング対象のセマンティクスを使用してラベルなしテキストのアノテーションを生成する、自己学習の一形態と見なすことができる。 追加ボーナスとして、LOCCOによって生成されたアノテーションは、神経テキスト生成モデルをトレーニングするために自明に再利用することができる。
  論文  参考訳（メタデータ） (2023-05-31T16:47:20Z)
• Graph Neural Networks for Contextual ASR with the Tree-Constrained Pointer Generator [9.053645441056256]
  本稿では,グラフニューラルネットワーク(GNN)符号化を用いたエンドツーエンドのコンテキストASRを実現するための革新的な手法を提案する。 GNNエンコーディングは、各ツリーノードでのASR復号処理において、将来のワードピースのルックアヘッドを促進する。 Librispeech と AMI corpus を用いて,視覚的な文脈的 ASR パイプラインに従ってシステム性能を評価した。
  論文  参考訳（メタデータ） (2023-05-30T08:20:58Z)
• Neural Structured Prediction for Inductive Node Classification [29.908759584092167]
  本稿では,ラベル付き学習グラフのモデルを学習し,未ラベルの試験グラフ上でノードラベルを推論するために一般化することを目的とした,帰納的環境におけるノード分類について検討する。 本稿では,両者の利点を組み合わせたSPN(Structured Proxy Network)という新しいアプローチを提案する。
  論文  参考訳（メタデータ） (2022-04-15T15:50:27Z)
• VQ-GNN: A Universal Framework to Scale up Graph Neural Networks using Vector Quantization [70.8567058758375]
  VQ-GNNは、Vector Quantization(VQ)を使用して、パフォーマンスを損なうことなく、畳み込みベースのGNNをスケールアップするための普遍的なフレームワークである。 我々のフレームワークは,グラフ畳み込み行列の低ランク版と組み合わせた量子化表現を用いて,GNNの「隣の爆発」問題を回避する。
  論文  参考訳（メタデータ） (2021-10-27T11:48:50Z)
• Distance Encoding: Design Provably More Powerful Neural Networks for Graph Representation Learning [63.97983530843762]
  グラフニューラルネットワーク(GNN)はグラフ表現学習において大きな成功を収めている。 GNNは、実際には非常に異なるグラフ部分構造に対して同一の表現を生成する。 より強力なGNNは、最近高階試験を模倣して提案され、基礎となるグラフ構造を疎結合にできないため、非効率である。 本稿では,グラフ表現学習の新たなクラスとして距離分解(DE)を提案する。
  論文  参考訳（メタデータ） (2020-08-31T23:15:40Z)
• Binarized Graph Neural Network [65.20589262811677]
  我々は二項化グラフニューラルネットワークを開発し、二項化ネットワークパラメータを用いてノードのバイナリ表現を学習する。 提案手法は既存のGNNベースの埋め込み手法にシームレスに統合できる。 実験により、提案された二項化グラフニューラルネットワーク、すなわちBGNは、時間と空間の両方の観点から、桁違いに効率的であることが示されている。
  論文  参考訳（メタデータ） (2020-04-19T09:43:14Z)

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

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