論文の概要: Magnushammer: A Transformer-Based Approach to Premise Selection
- arxiv url: http://arxiv.org/abs/2303.04488v3
- Date: Mon, 18 Mar 2024 14:16:22 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-21 01:40:47.407494
- Title: Magnushammer: A Transformer-Based Approach to Premise Selection
- Title（参考訳）: Magnushammer: 選択を前提としたトランスフォーマーベースのアプローチ
- Authors: Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, Yuhuai Wu,
- Abstract要約: 我々は、(保護状態、関連する前提)ペアのテキスト表現を含む、前提選択のための新しいデータセットを開発し、オープンソース化する。
我々の手法であるMagnushammerは、Sledgehammerと呼ばれるインタラクティブな定理の証明において、最も先進的で広く使われている自動化ツールより優れています。
さらに、PISAベンチマークでは、最先端の証明成功率を57.0%から71.0%に改善し、パラメータを4ドル減らした。
- 参考スコア（独自算出の注目度）: 20.445974111113223
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: This paper presents a novel approach to premise selection, a crucial reasoning task in automated theorem proving. Traditionally, symbolic methods that rely on extensive domain knowledge and engineering effort are applied to this task. In contrast, this work demonstrates that contrastive training with the transformer architecture can achieve higher-quality retrieval of relevant premises, without the engineering overhead. Our method, Magnushammer, outperforms the most advanced and widely used automation tool in interactive theorem proving called Sledgehammer. On the PISA and miniF2F benchmarks Magnushammer achieves $59.5\%$ (against $38.3\%$) and $34.0\%$ (against $20.9\%$) success rates, respectively. By combining \method with a language-model-based automated theorem prover, we further improve the state-of-the-art proof success rate from $57.0\%$ to $71.0\%$ on the PISA benchmark using $4$x fewer parameters. Moreover, we develop and open source a novel dataset for premise selection, containing textual representations of (proof state, relevant premise) pairs. To the best of our knowledge, this is the largest available premise selection dataset, and the first one for the Isabelle proof assistant.
- Abstract（参考訳）: 本稿では,自動定理証明における重要な推論課題である前提選択に対する新しいアプローチを提案する。
伝統的に、このタスクには広範なドメイン知識とエンジニアリングの努力に依存するシンボリックメソッドが適用される。
対照的に、この研究は、トランスフォーマーアーキテクチャによる対照的なトレーニングが、エンジニアリングオーバーヘッドを伴わずに、関連する前提の高品質な検索を実現することを実証している。
我々の手法であるMagnushammerは、Sledgehammerと呼ばれるインタラクティブな定理の証明において、最も先進的で広く使われている自動化ツールより優れています。
PISA と miniF2F のベンチマークでは、Magnushammer は59.5 %$(それぞれ38.3 %$)と34.0 %$(それぞれ20.9 %$)を達成している。
言語モデルに基づく自動定理証明器と<method</methodを併用することにより、PISAベンチマークにおいて4ドル未満のパラメータを用いて、最先端の証明成功率を57.0\%から71.0\%に改善する。
さらに,本研究では,(保護状態,関連する前提)ペアのテキスト表現を含む,前提選択のための新しいデータセットを開発し,オープンソース化する。
私たちの知る限りでは、これは利用可能な最大の前提選択データセットであり、Isabelle証明アシスタントの最初のものである。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。