Fugu-MT 論文翻訳(概要): Faster Smarter Induction in Isabelle/HOL

論文の概要: Faster Smarter Induction in Isabelle/HOL

arxiv url: http://arxiv.org/abs/2009.09215v4
Date: Sun, 9 May 2021 07:58:26 GMT
ステータス: 処理完了
システム内更新日: 2022-10-16 21:46:57.628511
Title: Faster Smarter Induction in Isabelle/HOL
Title（参考訳）: Isabelle/HOLにおけるより高速なスマート誘導
Authors: Yutaka Nagashima
Abstract要約: sem_indはインダクトメソッドに渡す引数を推奨する。定義量化器は、帰納的問題の構文構造だけでなく、ドメインに依存しないスタイルにおける関連する定数の定義も調べることができる。
参考スコア（独自算出の注目度）: 6.85316573653194
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science. To address this problem, we developed sem_ind. Given inductive problem, sem_ind recommends what arguments to pass to the induct method. To improve the accuracy of sem_ind, we introduced definitional quantifiers, a new kind of quantifiers that allow us to investigate not only the syntactic structures of inductive problems but also the definitions of relevant constants in a domain-agnostic style. Our evaluation shows that compared to its predecessor sem_ind improves the accuracy of recommendation from 20.1% to 38.2% for the most promising candidates within 5.0 seconds of timeout while decreasing the median value of execution time from 2.79 seconds to 1.06 seconds.
Abstract（参考訳）: 帰納的証明は形式的検証や数学全般において重要な役割を果たす。しかし、その自動化はコンピュータサイエンスにおける長年の課題の1つとして残っている。この問題に対処するため,我々はsem_indを開発した。帰納的問題が発生した場合、sem_indはインダクティブメソッドに渡す引数を推奨する。 sem_indの精度を向上させるために,帰納的問題の構文構造だけでなく,関連する定数の定義をドメインに依存しないスタイルで検討できる,新しい種類の量子化器であるdefinitional quantifiersを導入した。評価の結果,従来のsem_indと比較して5.0秒以内に最も有望な候補に対して20.1%から38.2%の推奨精度を向上し,実行時間の中央値が2.79秒から1.06秒に低下した。

関連論文リスト

Fast Ergodic Search with Kernel Functions [0.4915744683251149]
カーネルベースのエルゴード計量を開発し、ユークリッド空間からリー群へ一般化する。非線形システムに対するカーネルエルゴード計量の1次最適条件を導出する。総合的な数値ベンチマークにより、提案手法は最先端のアルゴリズムよりも少なくとも2桁高速であることが示された。
論文参考訳（メタデータ） (2024-03-03T15:30:31Z)
Improving Dual-Encoder Training through Dynamic Indexes for Negative Mining [61.09807522366773]
本稿では,ソフトマックスを証明可能な境界で近似し,木を動的に維持するアルゴリズムを提案する。我々は,2000万以上のターゲットを持つデータセットについて検討し,オラクル・ブルート力負の鉱業に関して,誤差を半分に削減した。
論文参考訳（メタデータ） (2023-03-27T15:18:32Z)
Deep Declarative Dynamic Time Warping for End-to-End Learning of Alignment Paths [54.53208538517505]
本稿では、動的時間ワープ(DTW)による時間的アライメントステップを含む時系列データのエンドツーエンド学習モデルについて述べる。そこで我々は,2レベル最適化とDecDTWと呼ばれる深層宣言ネットワークに基づくDTW層を提案する。この特性は、下流損失関数が最適アライメントパス自身で定義されるアプリケーションに特に有用であることを示す。
論文参考訳（メタデータ） (2023-03-19T21:58:37Z)
Accelerating Attention through Gradient-Based Learned Runtime Pruning [9.109136535767478]
自己認識は、トランスフォーマーベースの自然言語処理モデルにおいて、最先端の精度を実現する重要な手段である。本稿では、学習の損失関数に組み込まれたソフトな微分可能正規化器による探索を定式化する。我々は、ビットレベルの早期終了マイクロアーキテクチャ機構を持つトランスフォーマー言語モデルに対して、LeOPArdと呼ばれるビットシリアルアーキテクチャを考案した。
論文参考訳（メタデータ） (2022-04-07T05:31:13Z)
On the Second-order Convergence Properties of Random Search Methods [7.788439526606651]
本研究では,2次情報に依存しない標準的なランダム検索手法が2次定常点に収束することを証明する。本稿では,関数評価のみに依存する負曲率の新しい変種を提案する。
論文参考訳（メタデータ） (2021-10-25T20:59:31Z)
Train Short, Test Long: Attention with Linear Biases Enables Input Length Extrapolation [62.51758040848735]
本稿では,リニアバイアス(ALiBi)を用いた簡易かつ効率的な検査法を提案する。 ALiBiは、単語の埋め込みに位置埋め込みを加えるのではなく、クエリキーのアテンションスコアを、その距離に比例する用語でバイアスする。本手法では,長さ2048の入力シーケンスに外挿する長さ1024の入力シーケンスに対して,13億のパラメータモデルをトレーニングすることが可能であり,長さ2048の入力に基づいてトレーニングされた正弦波位置埋め込みモデルと同じ難易度を実現する。
論文参考訳（メタデータ） (2021-08-27T17:35:06Z)
A2P-MANN: Adaptive Attention Inference Hops Pruned Memory-Augmented Neural Networks [3.682712058535653]
A2P-MANNと呼ばれるオンラインアダプティブアプローチを提案し、メモリ拡張ニューラルネットワークで必要な注意推論ホップ数を制限する。この技術は、正しい解を抽出する際に不要な大量の計算を除去する。この手法の有効性は,bAbIデータセットの質問応答(QA)タスクを用いて評価する。
論文参考訳（メタデータ） (2021-01-24T12:02:12Z)
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction [6.85316573653194]
SeLFiEは、Isabelle/HOLにおけるインダクタンス戦術の適用方法に関するユーザの知識を表すクエリ言語である。評価のために,SeLFiEを用いた自動誘導証明器を開発した。新しい証明器は,1.0秒タイムアウトのベースライン証明よりも1.4×103%向上し,スピードアップの中央値が4.48倍となった。
論文参考訳（メタデータ） (2020-10-19T09:05:09Z)
PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文参考訳（メタデータ） (2020-10-06T15:47:53Z)
Single-Timescale Stochastic Nonconvex-Concave Optimization for Smooth Nonlinear TD Learning [145.54544979467872]
本稿では,各ステップごとに1つのデータポイントしか必要としない2つの単一スケールシングルループアルゴリズムを提案する。本研究の結果は, 同時一次および二重側収束の形で表される。
論文参考訳（メタデータ） (2020-08-23T20:36:49Z)
From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。 8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
論文参考訳（メタデータ） (2020-06-05T10:56:52Z)

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