論文の概要: 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システムが同様のハンマー評価では証明できない多くの定理を証明します。

関連論文リスト

• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Efficient Event-based Delay Learning in Spiking Neural Networks [0.1350479308585481]
  スパイキングニューラルネットワーク(SNN)は、従来のニューラルネットワークに代わるエネルギー効率の高い代替手段として注目を集めている。 本研究では,EventPropProp形式に基づくSNNのための新しいイベントベーストレーニング手法を提案する。 提案手法は,現在最先端の遅延学習手法のメモリの半分以下を用いており,最大26倍高速であることを示す。
  論文  参考訳（メタデータ） (2025-01-13T13:44:34Z)
• Interpretable Language Modeling via Induction-head Ngram Models [74.26720927767398]
  誘導ヘッドngramモデル(Induction-Gram)を提案する。 この誘導ヘッドは、カスタムのニューラル類似度メトリックを使用して、モデルの入力コンテキストを効率的に検索し、潜在的に次の単語補完を行う。 実験により,本手法はベースラインの解釈可能なモデルよりも,単語の次単語予測を大幅に改善することが示された。
  論文  参考訳（メタデータ） (2024-10-31T12:33: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)
• 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)

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

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