論文の概要: Fast and Slow Enigmas and Parental Guidance

• arxiv url: http://arxiv.org/abs/2107.06750v1
• Date: Wed, 14 Jul 2021 14:53:08 GMT
• ステータス: 処理完了
• システム内更新日: 2021-07-15 14:20:50.546561
• Title: Fast and Slow Enigmas and Parental Guidance
• Title（参考訳）: 高速・低速エニグマと親性指導
• Authors: Zarathustra Goertzel, Karel Chvalovsk\'y, Jan Jakub\r{u}v, Miroslav Ol\v{s}\'ak, Josef Urban
• Abstract要約: ENIGMAは、E自動定理証明器における節の選択をガイドする。 サーバベースのGPU評価を追加することで、ニューラルネットワークのガイダンスを大幅に高速化します。 2つ目の追加は、EやProver9のようなシステムで現在使われている高速な重量ベースリジェクションフィルタによって動機付けられている。 3つ目の追加は「両親によって子供を裁く」ことに基づいており、おそらくはそれが条項を作成する前に推論を拒絶する可能性がある。
• 参考スコア（独自算出の注目度）: 1.0424613957613162
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We describe several additions to the ENIGMA system that guides clause selection in the E automated theorem prover. First, we significantly speed up its neural guidance by adding server-based GPU evaluation. The second addition is motivated by fast weight-based rejection filters that are currently used in systems like E and Prover9. Such systems can be made more intelligent by instead training fast versions of ENIGMA that implement more intelligent pre-filtering. This results in combinations of trainable fast and slow thinking that improves over both the fast-only and slow-only methods. The third addition is based on "judging the children by their parents", i.e., possibly rejecting an inference before it produces a clause. This is motivated by standard evolutionary mechanisms, where there is always a cost to producing all possible offsprings in the current population. This saves time by not evaluating all clauses by more expensive methods and provides a complementary view of the generated clauses. The methods are evaluated on a large benchmark coming from the Mizar Mathematical Library, showing good improvements over the state of the art.
• Abstract（参考訳）: 本稿では,E自動定理証明器における節選択を導くENIGMAシステムへのいくつかの追加について述べる。 まず、サーバベースのGPU評価を追加することにより、ニューラルネットワークのガイダンスを大幅に高速化する。 第2の追加は、eやprovr9などのシステムで現在使用されている、軽量なリジェクションフィルタによるものだ。 このようなシステムは、よりインテリジェントな事前フィルタリングを実装するENIGMAの高速バージョンをトレーニングすることで、よりインテリジェントにすることができる。 これにより、トレーニング可能な高速かつ低速な思考の組み合わせが実現され、高速と低速の両方で改善される。 3つ目の追加は「両親によって子供を裁く」こと、つまり、条項を作成する前に推論を拒絶することに基づいている。 これは、現在の人口において可能なすべての子孫を生産するコストが常にかかる標準的な進化メカニズムによって動機付けられる。 これにより、全ての節をより高価な方法で評価しないことで時間を節約し、生成された節の補完的なビューを提供する。 これらの手法は、Mizar Mathematical Libraryからの大規模なベンチマークで評価され、最先端の優れた改善が示されている。

関連論文リスト

• Optimizing Tensor Computation Graphs with Equality Saturation and Monte Carlo Tree Search [0.0]
  モンテカルロ木探索を用いて優れた表現を構築するテンソルグラフ書き換え手法を提案する。 提案手法は,既存の手法と比較して,ニューラルネットワークの推論速度を最大11%向上させる。
  論文  参考訳（メタデータ） (2024-10-07T22:22:02Z)
• Efficient Few-Shot Object Detection via Knowledge Inheritance [62.36414544915032]
  Few-shot Object Detection (FSOD) は、未確認のタスクに少ないトレーニングサンプルで適応できるジェネリック検出器を学習することを目的としている。 計算量の増加を伴わない効率的なプレトレイン・トランスファー・フレームワーク(PTF)のベースラインを提案する。 また,予測された新しいウェイトと事前訓練されたベースウェイトとのベクトル長の不整合を軽減するために,適応長再スケーリング(ALR)戦略を提案する。
  論文  参考訳（メタデータ） (2022-03-23T06:24:31Z)
• Boosting Fast Adversarial Training with Learnable Adversarial Initialization [79.90495058040537]
  対人訓練(AT)は、対人訓練の例を活用することにより、モデルロバスト性を改善するのに有効であることが示されている。 トレーニング効率を向上させるため,高速AT法では1回だけ勾配を計算することにより高速勾配符号法(FGSM)が採用されている。
  論文  参考訳（メタデータ） (2021-10-11T05:37:00Z)
• Nesterov Accelerated ADMM for Fast Diffeomorphic Image Registration [63.15453821022452]
  ディープラーニングに基づくアプローチの最近の発展は、DiffIRのサブ秒間実行を実現している。 本稿では,中間定常速度場を機能的に構成する簡易な反復スキームを提案する。 次に、任意の順序の正規化項を用いて、これらの速度場に滑らかさを課す凸最適化モデルを提案する。
  論文  参考訳（メタデータ） (2021-09-26T19:56:45Z)
• Highly Parallel Autoregressive Entity Linking with Discriminative Correction [51.947280241185]
  自己回帰リンクを全ての潜在的な言及に対して並列化する,非常に効率的な手法を提案する。 我々のモデルは以前の生成法より70倍高速で精度が高い。
  論文  参考訳（メタデータ） (2021-09-08T17:28:26Z)
• Higher-order Derivatives of Weighted Finite-state Machines [68.43084108204741]
  本研究では、重み付き有限状態機械の正規化定数に関する高次微分の計算について検討する。 文献に記載されていないすべての順序の導関数を評価するための一般アルゴリズムを提案する。 我々のアルゴリズムは以前のアルゴリズムよりもはるかに高速である。
  論文  参考訳（メタデータ） (2021-06-01T19:51:55Z)
• Vampire With a Brain Is a Good ITP Hammer [0.0]
  我々は,効率のよい神経誘導による飽和手順の強化により,完全なMizarライブラリ上でのハンティングにおけるヴァンパイアの性能を向上させる。 節の論理的内容を考慮した従来のニューラルメソッドと比較して、これはニューラルガイダンスの大きなリアルタイム高速化につながる。 得られたシステムは、優れた学習能力を示し、Mizarライブラリ上で最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2021-02-06T07:24:53Z)
• Faster Person Re-Identification [68.22203008760269]
  本稿では,新しいハッシュコード検索戦略を定式化することによって,高速ReIDのための新しいソリューションを提案する。 より短いコードを使用して、より正確なReIDのいくつかのトップ候補を洗練するために、より広い一致の類似性を粗くランク付けし、より長いコードを使用する。 2つのデータセットに対する実験結果から,提案手法(CtF)は現在のハッシュReID法よりも8%精度が高いだけでなく,5倍高速であることがわかった。
  論文  参考訳（メタデータ） (2020-08-16T03:02:49Z)

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

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