Fugu-MT 論文翻訳(概要): New Techniques that Improve ENIGMA-style Clause Selection Guidance

論文の概要: New Techniques that Improve ENIGMA-style Clause Selection Guidance

arxiv url: http://arxiv.org/abs/2102.13564v1
Date: Fri, 26 Feb 2021 16:13:45 GMT
ステータス: 処理完了
システム内更新日: 2021-03-01 13:53:38.511174
Title: New Techniques that Improve ENIGMA-style Clause Selection Guidance
Title（参考訳）: ENIGMA-style Clause Selection Guidanceを改善する新しい手法
Authors: Martin Suda
Abstract要約: 飽和定理証明者における機械学習項選択指導の話題を再検討する。再帰ニューラルネットワークを使用して、その導出履歴と、自動的に供給される理論公理の有無に基づいて節を分類します。ネットワークによって導かれる自動定理の証明器のヴァンパイアはリアルタイム評価のSMT-LIBの関連したサブセットの41%の改善を達成します。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a classifier for recognizing clauses that appeared in previously discovered proofs. In subsequent runs, clauses classified positively are prioritized for selection. We propose several improvements to this approach and experimentally confirm their viability. For the demonstration, we use a Recursive Neural Network to classify clauses based on their derivation history and the presence or absence of automatically supplied theory axioms therein. The automatic theorem prover Vampire guided by the network achieves a 41% improvement on a relevant subset of SMT-LIB in a real time evaluation.
Abstract（参考訳）: 飽和定理証明者における機械学習項選択指導の話題を再検討する。最近ENIGMAシステムによって普及した中心的なアイデアは、以前に発見された証明に現れる節を認識するための分類器を学ぶことです。その後の実行では、選択のためにポジティブに分類された節が優先される。我々はこのアプローチのいくつかの改善を提案し,その妥当性を実験的に確認する。実演では、帰納的ニューラルネットワークを用いて、その導出履歴と自動的に供給される理論公理の存在の有無に基づいて節を分類する。ネットワークによって導かれる自動定理の証明器のヴァンパイアはリアルタイム評価のSMT-LIBの関連したサブセットの41%の改善を達成します。

関連論文リスト

Revisiting Differential Verification: Equivalence Verification with Confidence [0.6562256987706128]
検証済みニューラルネットワーク(NN)がデプロイ前にプルーニング(および再トレーニング)されると、新しいNNが元のNNと同等に振る舞うことを証明することが望ましい。本稿では,NN間の差異を推論する差分検証の考え方を再考する。
論文参考訳（メタデータ） (2024-10-26T15:53:25Z)
Large-scale Pre-trained Models are Surprisingly Strong in Incremental Novel Class Discovery [76.63807209414789]
我々は,クラスiNCDにおける現状問題に挑戦し,クラス発見を継続的に,真に教師なしで行う学習パラダイムを提案する。凍結したPTMバックボーンと学習可能な線形分類器から構成される単純なベースラインを提案する。
論文参考訳（メタデータ） (2023-03-28T13:47:16Z)
Parametric Classification for Generalized Category Discovery: A Baseline Study [70.73212959385387]
Generalized Category Discovery (GCD)は、ラベル付きサンプルから学習した知識を用いて、ラベルなしデータセットで新しいカテゴリを発見することを目的としている。パラメトリック分類器の故障を調査し,高品質な監視が可能であった場合の過去の設計選択の有効性を検証し,信頼性の低い疑似ラベルを重要課題として同定する。エントロピー正規化の利点を生かし、複数のGCDベンチマークにおける最先端性能を実現し、未知のクラス数に対して強いロバスト性を示す、単純で効果的なパラメトリック分類法を提案する。
論文参考訳（メタデータ） (2022-11-21T18:47:11Z)
Learning Theorem Proving Components [1.138814184953183]
本稿では、前述した節の文脈における評価に基づいて、次の節を選択するグラフニューラルネットワーク(GNN)を提案する。本研究では、ENIGMAを用いたいくつかのアルゴリズムと実験について述べるとともに、節のグラフの重要な構成要素を学習することに基づく文脈評価の考え方を前進させる。
論文参考訳（メタデータ） (2021-07-21T12:00:05Z)
Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
論文参考訳（メタデータ） (2021-06-07T18:35:57Z)
Vampire With a Brain Is a Good ITP Hammer [0.0]
我々は,効率のよい神経誘導による飽和手順の強化により,完全なMizarライブラリ上でのハンティングにおけるヴァンパイアの性能を向上させる。節の論理的内容を考慮した従来のニューラルメソッドと比較して、これはニューラルガイダンスの大きなリアルタイム高速化につながる。得られたシステムは、優れた学習能力を示し、Mizarライブラリ上で最先端のパフォーマンスを達成する。
論文参考訳（メタデータ） (2021-02-06T07:24:53Z)
Binary Classification from Multiple Unlabeled Datasets via Surrogate Set Classification [94.55805516167369]
我々は m 個の U 集合を $mge2$ で二進分類する新しい手法を提案する。我々のキーとなる考え方は、サロゲート集合分類(SSC)と呼ばれる補助的分類タスクを考えることである。
論文参考訳（メタデータ） (2021-02-01T07:36:38Z)
A Correspondence Variational Autoencoder for Unsupervised Acoustic Word Embeddings [50.524054820564395]
そこで本稿では,変数分割音声セグメントを固定次元表現にマッピングするための教師なしモデルを提案する。結果として得られる音響単語の埋め込みは、低リソース言語とゼロリソース言語のための検索、発見、インデックスシステムの基礎を形成することができる。
論文参考訳（メタデータ） (2020-12-03T19:24:42Z)
Pre-training Is (Almost) All You Need: An Application to Commonsense Reasoning [61.32992639292889]
事前学習されたトランスモデルの微調整は、一般的なNLPタスクを解決するための標準的なアプローチとなっている。そこで本研究では,可視性ランキングタスクをフルテキスト形式でキャストする新たなスコアリング手法を提案する。提案手法は, ランダム再起動にまたがって, より安定した学習段階を提供することを示す。
論文参考訳（メタデータ） (2020-04-29T10:54:40Z)
Stateful Premise Selection by Recurrent Neural Networks [0.7614628596146599]
本研究では,大規模な形式ライブラリ上での新たな目標の証明において,事実(前提)を選択するための新たな学習ベース手法を開発する。我々のステートフルアーキテクチャは、最近言語翻訳のようなステートフルなタスクで成功しているリカレントニューラルネットワークに基づいている。
論文参考訳（メタデータ） (2020-03-11T14:59:37Z)
MSE-Optimal Neural Network Initialization via Layer Fusion [68.72356718879428]
ディープニューラルネットワークは、さまざまな分類と推論タスクに対して最先端のパフォーマンスを達成する。グラデーションと非進化性の組み合わせは、学習を新しい問題の影響を受けやすいものにする。確率変数を用いて学習した深層ネットワークの近傍層を融合する手法を提案する。
論文参考訳（メタデータ） (2020-01-28T18:25:15Z)

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