Fugu-MT 論文翻訳(概要): The Isabelle ENIGMA

論文の概要: The Isabelle ENIGMA

arxiv url: http://arxiv.org/abs/2205.01981v1
Date: Wed, 4 May 2022 10:15:57 GMT
ステータス: 処理完了
システム内更新日: 2022-05-05 14:05:51.094829
Title: The Isabelle ENIGMA
Title（参考訳）: イザベル・エニグマは
Authors: Zarathustra A. Goertzel, Jan Jakub\r{u}v, Cezary Kaliszyk, Miroslav Ol\v{s}\'ak, Jelle Piepenbrock, Josef Urban
Abstract要約: 我々は、Isabelle問題に対するENIGMAガイダンスのターゲットバージョン、ニューラル前提選択のターゲットバージョン、Eのためのターゲット戦略を開発する。我々の最後のベストシングルストラテジーENIGMAと前提選択システムは、Eのベストバージョンを15秒で25.3%改善する。
参考スコア（独自算出の注目度）: 3.7515646463759698
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance for the Isabelle problems, targeted versions of neural premise selection, and targeted strategies for E. The methods are trained in several iterations over hundreds of thousands untyped and typed first-order problems extracted from Isabelle. Our final best single-strategy ENIGMA and premise selection system improves the best previous version of E by 25.3% in 15 seconds, outperforming also all other previous ATP and SMT systems.
Abstract（参考訳）: 我々は、Isabelle Sledgehammer問題におけるE自動定理証明器の性能を、学習と定理証明を組み合わせることで改善する。特に、イザベル問題に対するenigmaガイダンスのターゲットバージョン、ニューラルネットワークの前提選択のターゲットバージョン、e.isabelleから抽出された数十万の非型および型付き1次問題に対して、いくつかのイテレーションでトレーニングされた方法のターゲット戦略を開発しました。我々の最後の最高のシングルストラテジーENIGMAと前提選択システムは、15秒でEのベストバージョンを25.3%改善し、他のATPやSMTシステムよりも優れています。

関連論文リスト

AdaS&S: a One-Shot Supernet Approach for Automatic Embedding Size Search in Deep Recommender System [15.119643144224021]
本稿では,AdaS&Sと呼ばれる新しい一発AESフレームワークを提案する。最初の段階では、トレーニングパラメータを埋め込みサイズから切り離し、適応サンプリング法を提案し、よく訓練されたスーパーネットを生成する。第2段階では、モデル効果の恩恵を受ける埋め込みサイズを得るために、以前に訓練されたスーパーネットを利用した強化学習探索プロセスを設計する。
論文参考訳（メタデータ） (2024-11-12T03:02:50Z)
On Exams with the Isabelle Proof Assistant [0.0]
本稿では,Isabelle証明アシスタントを用いた自動推論のコースにおいて,学生の学習結果をテストするためのアプローチを提案する。このアプローチにより、様々な論理的証明システムにおける形式的証明の一般的な理解と、イザベル/HOLの高階論理における証明の理解の両方をテストすることができる。
論文参考訳（メタデータ） (2023-03-10T11:37:09Z)
DivBO: Diversity-aware CASH for Ensemble Learning [26.18421492435029]
本稿では,多様性の明示的な探索をCASH問題に注入するダイバーシティ対応フレームワークであるDivBOを提案する。本フレームワークでは,2つの未知の構成のペアワイドな多様性を予測するために,ダイバーシティサロゲート(ダイバーシティサロゲート)を提案する。そこで,DivBOは10種類の比較手法の検証とテスト誤差の両面で,平均ランク(1.82と1.73)を達成していることを示す。
論文参考訳（メタデータ） (2023-02-07T04:53:21Z)
Learning To Cut By Looking Ahead: Cutting Plane Selection via Imitation Learning [80.45697245527019]
我々は、最良限の改善をもたらすカットを明示的に目指している欲求選択規則が、カット選択に対して強い決定を下すことを示す。本研究では,頭頂部の専門家を対象とした模擬学習のための新しいニューラルアーキテクチャ(NeuralCut)を提案する。
論文参考訳（メタデータ） (2022-06-27T16:07:27Z)
FOSTER: Feature Boosting and Compression for Class-Incremental Learning [52.603520403933985]
ディープニューラルネットワークは、新しいカテゴリーを学ぶ際に破滅的な忘れ方に悩まされる。本稿では,新たなカテゴリを適応的に学習するためのモデルとして,新しい2段階学習パラダイムFOSTERを提案する。
論文参考訳（メタデータ） (2022-04-10T11:38:33Z)
Robust Binary Models by Pruning Randomly-initialized Networks [57.03100916030444]
ランダムな二元ネットワークから敵攻撃に対して頑健なモデルを得る方法を提案する。ランダムな二元ネットワークを切断することにより、ロバストモデルの構造を学習する。本手法は, 敵攻撃の有無で, 強力な抽選券仮説を立証する。
論文参考訳（メタデータ） (2022-02-03T00:05:08Z)
The USYD-JD Speech Translation System for IWSLT 2021 [85.64797317290349]
本稿では,シドニー大学とJDが共同でIWSLT 2021低リソース音声翻訳タスクを提出したことを述べる。私たちは、公式に提供されたASRとMTデータセットでモデルをトレーニングしました。翻訳性能の向上を目的として, バック翻訳, 知識蒸留, 多機能再構成, トランスダクティブファインタニングなど, 最新の効果的な手法について検討した。
論文参考訳（メタデータ） (2021-07-24T09:53:34Z)
AutoBERT-Zero: Evolving BERT Backbone from Scratch [94.89102524181986]
そこで本稿では,提案するハイブリッドバックボーンアーキテクチャを自動検索するOP-NASアルゴリズムを提案する。提案するOP-NASの効率を向上させるために,探索アルゴリズムと候補モデルの評価を最適化する。実験の結果、検索されたアーキテクチャ(AutoBERT-Zero)は、様々な下流タスクにおいてBERTとそのバリエーションの異なるモデル容量を著しく上回っていることがわかった。
論文参考訳（メタデータ） (2021-07-15T16:46:01Z)
DSelect-k: Differentiable Selection in the Mixture of Experts with Applications to Multi-Task Learning [17.012443240520625]
最先端のMoEモデルは、トレーニング可能なスパースゲートを使用して、入力例ごとに専門家のサブセットを選択する。 DSelect-kは、新しいバイナリエンコーディングの定式化に基づいて、MoEのための最初の、連続的な差別化可能かつスパースゲートである。 DSelect-kに基づくMoEモデルは,予測および専門家の選択性能において統計的に有意な改善を達成できることを示す。
論文参考訳（メタデータ） (2021-06-07T16:25:27Z)
Deep Learning as a Competitive Feature-Free Approach for Automated Algorithm Selection on the Traveling Salesperson Problem [0.0]
我々は、有名なユークリッド旅行セールスマン問題(TSP)に焦点を当てる。私たちは1,000のノードでインスタンスを進化させ、そこではソルバがパフォーマンスプロファイルを強く示します。特徴のないディープニューラルネットワークに基づくアプローチは、インスタンスの視覚的表現のみに基づいており、すでに古典的なASモデルの結果と一致していることを示す。
論文参考訳（メタデータ） (2020-06-29T12:15:35Z)
RNN-T Models Fail to Generalize to Out-of-Domain Audio: Causes and Solutions [73.45995446500312]
ストリーミングおよび非ストリーミングリカレントニューラルネットワークトランスデューサ(RNN-T)のエンド・ツー・エンドモデルにおける一般化特性を解析した。トレーニング中に複数の正規化手法を組み合わせる方法と,動的重複推論を用いる方法を提案する。
論文参考訳（メタデータ） (2020-05-07T06:24:47Z)

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