Fugu-MT 論文翻訳(概要): Magnushammer: A Transformer-based Approach to Premise Selection

論文の概要: 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\%$に大幅に改善する。

関連論文リスト

Automatic Die Studies for Ancient Numismatics [3.384989790372139]
ダイス研究は古代の貨幣生産の定量化に不可欠である。このタスクを自動化しようとする作業はほとんどなく、コンピュータビジョンの観点から適切なリリースや評価が行われていない。提案手法は,従来の手法と比較して,いくつかの革新を取り入れた完全自動アプローチである。
論文参考訳（メタデータ） (2024-07-30T14:54:54Z)
Transfer Q Star: Principled Decoding for LLM Alignment [105.89114186982972]
Transfer $Q*$は、ベースラインモデルを通してターゲット報酬$r$の最適値関数を推定する。提案手法は, 従来のSoTA法で観測された準最適差を著しく低減する。
論文参考訳（メタデータ） (2024-05-30T21:36:12Z)
Monte Carlo Tree Search Boosts Reasoning via Iterative Preference Learning [55.96599486604344]
本稿では,Large Language Models (LLMs) の推論能力向上を目的とした,反復的な選好学習プロセスによるアプローチを提案する。我々は、MCTS(Monte Carlo Tree Search)を用いて好みデータを反復的に収集し、そのルックアヘッド機能を利用して、インスタンスレベルの報酬をよりきめ細かいステップレベルの信号に分解する。提案アルゴリズムはDPO(Direct Preference Optimization)を用いて,新たに生成されたステップレベルの優先度データを用いてLCMポリシーを更新する。
論文参考訳（メタデータ） (2024-05-01T11:10:24Z)
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
論文参考訳（メタデータ） (2023-12-20T09:55:21Z)
Online non-parametric likelihood-ratio estimation by Pearson-divergence functional minimization [55.98760097296213]
iid 観測のペア $(x_t sim p, x'_t sim q)$ が時間の経過とともに観測されるような,オンラインな非パラメトリック LRE (OLRE) のための新しいフレームワークを提案する。本稿では,OLRE法の性能に関する理論的保証と,合成実験における実証的検証について述べる。
論文参考訳（メタデータ） (2023-11-03T13:20:11Z)
Deep Active Ensemble Sampling For Image Classification [8.31483061185317]
アクティブラーニングフレームワークは、最も有益なデータポイントのラベル付けを積極的に要求することで、データアノテーションのコストを削減することを目的としている。提案手法には、不確実性に基づく手法、幾何学的手法、不確実性に基づく手法と幾何学的手法の暗黙の組み合わせなどがある。本稿では, サンプル選択戦略における効率的な探索・探索トレードオフを実現するために, 不確実性に基づくフレームワークと幾何学的フレームワークの両方の最近の進歩を革新的に統合する。本フレームワークは,(1)正確な後続推定,(2)計算オーバーヘッドと高い精度のトレードオフの2つの利点を提供する。
論文参考訳（メタデータ） (2022-10-11T20:20:20Z)
Supervised Graph Contrastive Pretraining for Text Classification [7.068680287596106]
本稿では,グラフに基づく教師付きコントラスト学習手法を用いて,関連タスクからのラベル付きデータを効果的に活用する方法を提案する。提案手法は,事前学習のスキームを2.5%,サンプルレベルのコントラスト学習に基づく定式化を平均1.8%で上回ることを示す。
論文参考訳（メタデータ） (2021-12-21T17:47:14Z)
Egocentric Hand-object Interaction Detection and Application [24.68535915849555]
本稿では,エゴセントリックな視点から手動物体の相互作用を検出する手法を提案する。我々は、手ポーズ、手動マスク、手動物体マスクを予測するネットワークを訓練し、手動物体の相互作用状態を共同で予測する。私たちのメソッドは、Shanの(textbf1simtextbf2$ FPS)よりもはるかに効率的な$textbf30$ FPSで実行できます。
論文参考訳（メタデータ） (2021-09-29T21:47:16Z)
Navigating to the Best Policy in Markov Decision Processes [68.8204255655161]
マルコフ決定過程における純粋探索問題について検討する。エージェントはアクションを逐次選択し、結果のシステム軌道から可能な限り早くベストを目標とする。
論文参考訳（メタデータ） (2021-06-05T09:16:28Z)
A Study on Efficiency, Accuracy and Document Structure for Answer Sentence Selection [112.0514737686492]
本稿では,単語関連エンコーダとともに,原語階の内在的構造を活用すれば,競争的な結果が得られることを論じる。私たちのモデルはWikiQAデータセットでトレーニングするのに9.5秒かかります。
論文参考訳（メタデータ） (2020-03-04T22:12:18Z)
Black-Box Certification with Randomized Smoothing: A Functional Optimization Based Framework [60.981406394238434]
本稿では,非ガウス雑音とより一般的な攻撃に対する対向的認証の一般的な枠組みを提案する。提案手法は,従来の手法よりも優れた認証結果を得るとともに,ランダム化スムーズな認証の新たな視点を提供する。
論文参考訳（メタデータ） (2020-02-21T07:52:47Z)

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