論文の概要: Vampire With a Brain Is a Good ITP Hammer

• arxiv url: http://arxiv.org/abs/2102.03529v1
• Date: Sat, 6 Feb 2021 07:24:53 GMT
• ステータス: 処理完了
• システム内更新日: 2021-02-09 15:44:52.611398
• Title: Vampire With a Brain Is a Good ITP Hammer
• Title（参考訳）: 脳を持つ吸血鬼は良いITPハンマーです
• Authors: Martin Suda
• Abstract要約: 我々は,効率のよい神経誘導による飽和手順の強化により,完全なMizarライブラリ上でのハンティングにおけるヴァンパイアの性能を向上させる。 節の論理的内容を考慮した従来のニューラルメソッドと比較して、これはニューラルガイダンスの大きなリアルタイム高速化につながる。 得られたシステムは、優れた学習能力を示し、Mizarライブラリ上で最先端のパフォーマンスを達成する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Vampire has been for a long time the strongest first-order automated theorem prover, widely used for hammer-style proof automation in ITPs such as Mizar, Isabelle, HOL and Coq. In this work, we considerably improve the performance of Vampire in hammering over the full Mizar library by enhancing its saturation procedure with efficient neural guidance. In particular, we employ a recursive neural network classifying the generated clauses based only on their derivation history. Compared to previous neural methods based on considering the logical content of the clauses, this leads to large real-time speedup of the neural guidance. The resulting system shows good learning capability and achieves state-of-the-art performance on the Mizar library, while proving many theorems that the related ENIGMA system could not prove in a similar hammering evaluation.
• Abstract（参考訳）: ヴァンパイアは長い間、Mizar、Isabelle、HOL、CoqなどのITPにおけるハンマースタイルの証明自動化に広く使われている最強の1階自動定理証明器である。 そこで本研究では,神経誘導による飽和処理の効率化により,全ミザーライブラリを打破するヴァンパイアの性能を大幅に向上した。 特に,生成した節を導出履歴のみに基づいて分類する再帰的ニューラルネットワークを用いる。 節の論理的内容を考慮した従来のニューラルメソッドと比較して、これはニューラルガイダンスの大きなリアルタイム高速化につながる。 結果として得られたシステムは優れた学習能力を示し、Mizarライブラリで最先端のパフォーマンスを達成し、関連するENIGMAシステムが同様のハンマー評価では証明できない多くの定理を証明します。

関連論文リスト

• Interpretable Language Modeling via Induction-head Ngram Models [74.26720927767398]
  誘導ヘッドngramモデル(Induction-Gram)を提案する。 この誘導ヘッドは、カスタムのニューラル類似度メトリックを使用して、モデルの入力コンテキストを効率的に検索し、潜在的に次の単語補完を行う。 実験により,本手法はベースラインの解釈可能なモデルよりも,単語の次単語予測を大幅に改善することが示された。
  論文  参考訳（メタデータ） (2024-10-31T12:33:26Z)
• Neural Attention: Enhancing QKV Calculation in Self-Attention Mechanism with Neural Networks [25.75678339426731]
  本稿では,QKVを用いたニューラルネットワークの計算手法について検討する。 我々は、IWSLT 2017ドイツ語翻訳タスクデータセットの実験を行い、従来の手法で近似した。 また,Wikitext-103データセットを用いてRobertaモデルをトレーニングする際の優位性を示した。
  論文  参考訳（メタデータ） (2023-10-17T17:06:26Z)
• Heterogenous Memory Augmented Neural Networks [84.29338268789684]
  ニューラルネットワークのための新しいヘテロジニアスメモリ拡張手法を提案する。 学習可能なメモリトークンをアテンション機構付きで導入することにより、膨大な計算オーバーヘッドを伴わずに性能を効果的に向上させることができる。 In-distriion (ID) と Out-of-distriion (OOD) の両方の条件下での様々な画像およびグラフベースのタスクに対するアプローチを示す。
  論文  参考訳（メタデータ） (2023-10-17T01:05:28Z)
• A Stable, Fast, and Fully Automatic Learning Algorithm for Predictive Coding Networks [65.34977803841007]
  予測符号化ネットワークは、ベイズ統計学と神経科学の両方にルーツを持つ神経科学にインスパイアされたモデルである。 シナプス重みに対する更新規則の時間的スケジュールを変更するだけで、元の規則よりもずっと効率的で安定したアルゴリズムが得られることを示す。
  論文  参考訳（メタデータ） (2022-11-16T00:11:04Z)
• Boosting Tail Neural Network for Realtime Custom Keyword Spotting [2.5137859989323537]
  本稿では,リアルタイムカスタムキーワードスポッティング(RCKS)の性能向上を目的としたBoosting Tail Neural Network(BTNN)を提案する。 脳科学にインスパイアされた多くの機械学習アルゴリズムは、弱い分類器を使って困難な問題を解決するために開発された。
  論文  参考訳（メタデータ） (2022-05-24T13:26:39Z)
• Can we learn gradients by Hamiltonian Neural Networks? [68.8204255655161]
  本稿では,勾配を学習するODEニューラルネットワークに基づくメタラーナを提案する。 提案手法は,LLUアクティベーションを最適化したMLMとMNISTデータセットにおいて,LSTMに基づくメタラーナーよりも優れていることを示す。
  論文  参考訳（メタデータ） (2021-10-31T18:35:10Z)
• Fast and Slow Enigmas and Parental Guidance [1.0424613957613162]
  ENIGMAは、E自動定理証明器における節の選択をガイドする。 サーバベースのGPU評価を追加することで、ニューラルネットワークのガイダンスを大幅に高速化します。 2つ目の追加は、EやProver9のようなシステムで現在使われている高速な重量ベースリジェクションフィルタによって動機付けられている。 3つ目の追加は「両親によって子供を裁く」ことに基づいており、おそらくはそれが条項を作成する前に推論を拒絶する可能性がある。
  論文  参考訳（メタデータ） (2021-07-14T14:53:08Z)
• Why Do Pretrained Language Models Help in Downstream Tasks? An Analysis of Head and Prompt Tuning [66.44344616836158]
  本稿では,事前学習タスクと下流タスクをテキストの潜在変数生成モデルに関連付ける分析フレームワークを提案する。 HMMの特定の非退化条件下では、単純な分類ヘッドがダウンストリームタスクを解くことができ、また、迅速なチューニングにより、より弱い非退化条件で下流の保証を得ることができ、さらに、メモリ拡張HMMの回復保証がバニラHMMよりも強いことを示す。
  論文  参考訳（メタデータ） (2021-06-17T03:31:47Z)
• New Techniques that Improve ENIGMA-style Clause Selection Guidance [0.0]
  飽和定理証明者における機械学習項選択指導の話題を再検討する。 再帰ニューラルネットワークを使用して、その導出履歴と、自動的に供給される理論公理の有無に基づいて節を分類します。 ネットワークによって導かれる自動定理の証明器のヴァンパイアはリアルタイム評価のSMT-LIBの関連したサブセットの41%の改善を達成します。
  論文  参考訳（メタデータ） (2021-02-26T16:13:45Z)
• Closed Loop Neural-Symbolic Learning via Integrating Neural Perception, Grammar Parsing, and Symbolic Reasoning [134.77207192945053]
  従来の手法は強化学習アプローチを用いてニューラルシンボリックモデルを学ぶ。 我々は,脳神経知覚と記号的推論を橋渡しする前に,textbfgrammarモデルをテキストシンボリックとして導入する。 本稿では,トップダウンのヒューマンライクな学習手順を模倣して誤りを伝播する新しいtextbfback-searchアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2020-06-11T17:42:49Z)

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

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