論文の概要: Magnushammer: A Transformer-based Approach to Premise Selection
- arxiv url: http://arxiv.org/abs/2303.04488v1
- Date: Wed, 8 Mar 2023 10:22:00 GMT
- ステータス: 処理完了
- システム内更新日: 2023-03-09 14:34:31.105354
- Title: Magnushammer: A Transformer-based Approach to Premise Selection
- Title(参考訳): Magnushammer: トランスフォーマーによる選択の最適化
- Authors: Maciej Miku{\l}a, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu
Jiang, Jin Peng Zhou, Christian Szegedy, {\L}ukasz Kuci\'nski, Piotr
Mi{\l}o\'s, Yuhuai Wu
- Abstract要約: 我々は、ニューラルトランスフォーマーに基づくアプローチであるMagnushammerが、従来のシンボルシステムよりも大きなマージンで優れていることを示す。
PISAベンチマークでテストされたMagnushammerは、Sledgehammerの38.3%の証明レートに比べて59.5%の証明レートを達成した。
- 参考スコア(独自算出の注目度): 12.31045685482995
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Premise selection is a fundamental problem of automated theorem proving.
Previous works often use intricate symbolic methods, rely on domain knowledge,
and require significant engineering effort to solve this task. In this work, we
show that Magnushammer, a neural transformer-based approach, can outperform
traditional symbolic systems by a large margin. Tested on the PISA benchmark,
Magnushammer achieves $59.5\%$ proof rate compared to a $38.3\%$ proof rate of
Sledgehammer, the most mature and popular symbolic-based solver. Furthermore,
by combining Magnushammer with a neural formal prover based on a language
model, we significantly improve the previous state-of-the-art proof rate from
$57.0\%$ to $71.0\%$.
- Abstract(参考訳): 事前選択は自動定理証明の基本的な問題である。
以前は複雑なシンボリックな手法を使用しており、ドメイン知識に依存しており、この課題を解決するにはかなりのエンジニアリング努力が必要である。
本研究では、ニューラルトランスフォーマーに基づくアプローチであるMagnushammerが、従来のシンボルシステムよりも大きなマージンで優れていることを示す。
PISAベンチマークでテストされたMagnushammerは、最も成熟し人気のある記号ベースの解法であるSledgehammerの証明レート38.3\%に対して59.5\%の証明レートを達成した。
さらに,magnushammerを言語モデルに基づく神経形式証明器と組み合わせることで,従来の証明率を57.0\%$から71.0\%$に大幅に改善する。
関連論文リスト
- Quantum computational finance: martingale asset pricing for incomplete
markets [69.73491758935712]
金融の価格問題に様々な量子技術を適用することができることを示す。
従来の研究と異なる3つの方法について議論する。
論文 参考訳(メタデータ) (2022-09-19T09:22:01Z) - Certifiably Robust Interpretation via Renyi Differential Privacy [77.04377192920741]
我々はRenyi差分プライバシー(RDP)の新しい視点から解釈堅牢性の問題を研究する。
まず、証明可能で証明可能なトップ$k$ロバスト性を提供する。
第二に、提案手法は既存の手法よりも実験的堅牢性を$sim10%$で提供する。
第3に,ロバスト性と計算効率のトレードオフを円滑に行うことができる。
論文 参考訳(メタデータ) (2021-07-04T06:58:01Z) - Scale Mixtures of Neural Network Gaussian Processes [22.07524388784668]
我々は、末層パラメータのスケールに先行する$mathrmNNGP$のスケール混合を導入する。
ある種のスケールの先行で重み付きプロセスが得られ、逆ガンマ分布の場合、学生の$t$プロセスが復元されることを示す。
さらに、ニューラルネットワークを事前設定で分析し、勾配降下を訓練し、$mathrmNNGP$と同じような結果を得る。
論文 参考訳(メタデータ) (2021-07-03T11:02:18Z) - What Are Bayesian Neural Network Posteriors Really Like? [63.950151520585024]
ハミルトニアンモンテカルロは、標準およびディープアンサンブルよりも大きな性能向上を達成できることを示す。
また,深部分布は標準SGLDとHMCに類似しており,標準変動推論に近いことが示された。
論文 参考訳(メタデータ) (2021-04-29T15:38:46Z) - Vampire With a Brain Is a Good ITP Hammer [0.0]
我々は,効率のよい神経誘導による飽和手順の強化により,完全なMizarライブラリ上でのハンティングにおけるヴァンパイアの性能を向上させる。
節の論理的内容を考慮した従来のニューラルメソッドと比較して、これはニューラルガイダンスの大きなリアルタイム高速化につながる。
得られたシステムは、優れた学習能力を示し、Mizarライブラリ上で最先端のパフォーマンスを達成する。
論文 参考訳(メタデータ) (2021-02-06T07:24:53Z) - Almost Tight L0-norm Certified Robustness of Top-k Predictions against
Adversarial Perturbations [78.23408201652984]
トップk予測は、マシンラーニング・アズ・ア・サービス、レコメンダ・システム、Web検索など、多くの現実世界のアプリケーションで使用されている。
我々の研究はランダム化平滑化に基づいており、入力をランダム化することで、証明可能なロバストな分類器を構築する。
例えば、攻撃者がテスト画像の5ピクセルを任意に摂動できる場合に、ImageNet上で69.2%の認定トップ3精度を達成する分類器を構築することができる。
論文 参考訳(メタデータ) (2020-11-15T21:34:44Z) - Online Learning of Non-Markovian Reward Models [2.064612766965483]
エージェントが進化する環境の力学をモデル化する非マルコフ報酬決定プロセス(MDP)を考える。
MDPはエージェントによって知られているが、報酬関数はエージェントに未知であり、学習されなければならない。
我々はAngluinの$L*$アクティブ学習アルゴリズムを用いて、基礎となる非マルコフ報酬マシンを表すMealyマシンを学習する。
論文 参考訳(メタデータ) (2020-09-26T13:54:34Z) - Provable Robust Classification via Learned Smoothed Densities [1.599072005190786]
雑音の測定値から、$widehatx(Y)$, $textitBayes estimator$$ $X$という、ロバストな分類の問題を定式化する。
学習されたスムーズなエネルギー関数と線形分類器により、経験的防御と競合する堅牢な精度の証明可能な$ellを達成できることが示される。
論文 参考訳(メタデータ) (2020-05-09T19:52:32Z) - Black-Box Certification with Randomized Smoothing: A Functional
Optimization Based Framework [60.981406394238434]
本稿では,非ガウス雑音とより一般的な攻撃に対する対向的認証の一般的な枠組みを提案する。
提案手法は,従来の手法よりも優れた認証結果を得るとともに,ランダム化スムーズな認証の新たな視点を提供する。
論文 参考訳(メタデータ) (2020-02-21T07:52:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。