論文の概要: Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

• arxiv url: http://arxiv.org/abs/2205.10893v1
• Date: Sun, 22 May 2022 18:03:03 GMT
• ステータス: 処理完了
• システム内更新日: 2022-05-29 19:55:55.688837
• Title: Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
• Title（参考訳）: Thor: 言語モデルと自動定理プロデューサを統合するためのWielding Hammer
• Authors: Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzyg\'o\'zd\'z, Piotr Mi{\l}o\'s, Yuhuai Wu, Mateja Jamnik
• Abstract要約: 本稿では,言語モデルと自動定理証明器を統合するフレームワークであるThorを紹介する。 Thorは、PISAデータセットにおける言語モデルの成功率を39%から57%に引き上げる。 計算予算が大幅に小さくなると、Torは最高の既存のメソッドと同等のMiniF2Fデータセットで成功率を達成することができる。
• 参考スコア（独自算出の注目度）: 14.840914284796778
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In theorem proving, the task of selecting useful premises from a large library to unlock the proof of a given conjecture is crucially important. This presents a challenge for all theorem provers, especially the ones based on language models, due to their relative inability to reason over huge volumes of premises in text form. This paper introduces Thor, a framework integrating language models and automated theorem provers to overcome this difficulty. In Thor, a class of methods called hammers that leverage the power of automated theorem provers are used for premise selection, while all other tasks are designated to language models. Thor increases a language model's success rate on the PISA dataset from $39\%$ to $57\%$, while solving $8.2\%$ of problems neither language models nor automated theorem provers are able to solve on their own. Furthermore, with a significantly smaller computational budget, Thor can achieve a success rate on the MiniF2F dataset that is on par with the best existing methods. Thor can be instantiated for the majority of popular interactive theorem provers via a straightforward protocol we provide.
• Abstract（参考訳）: 定理証明において、大きなライブラリから有用な前提を選択して与えられた予想の証明を解く作業は極めて重要である。 これは、すべての定理証明者、特に言語モデルに基づくものにとって、テキスト形式の膨大な前提を相対的に推論できないため、課題となる。 本稿では,この難易度を克服するために,言語モデルと自動定理証明器を統合するフレームワークであるThorを紹介する。 Thorでは、自動定理プローバーの力を利用するハンマーと呼ばれる手法のクラスが前提選択に使用され、他の全てのタスクは言語モデルに指定される。 Thor は PISA データセットにおける言語モデルの成功率を 39 %$ から 57 %$ に引き上げる一方で、言語モデルも自動定理証明者も自分では解けない問題の 8.2 %$ を解決している。 さらに、計算予算を大幅に小さくすることで、Torは、最高の既存のメソッドと同等のMiniF2Fデータセットで成功率を達成することができる。 Thorは、我々が提供する単純なプロトコルを通じて、人気のある対話的定理証明者の大半に対してインスタンス化することができる。

関連論文リスト

• Scaling up Test-Time Compute with Latent Reasoning: A Recurrent Depth Approach [70.44265766483633]
  本稿では,潜在空間における暗黙的推論によるテスト時間計算のスケールアップが可能な,新しい言語モデルアーキテクチャについて検討する。 我々のモデルは繰り返しブロックを繰り返すことで動作し、テスト時に任意の深さに展開する。 結果のモデルが推論ベンチマークの性能を劇的に改善できることが示される。
  論文  参考訳（メタデータ） (2025-02-07T18:55:02Z)
• ProofWala: Multilingual Proof Data Synthesis and Theorem-Proving [53.67926215943612]
  $rm P Small ROOFW Small ALA$は、ニューラル定理プローサと2つの確立された対話的証明アシスタント(ITP)間の相互作用を可能にする 私たちは、$rm P Small ROOFWsmall ALA$生成のCoqとLeanのデータの組み合わせでトレーニングされたモデルが、標準のprov-at-k$メトリック上で、Lean-onlyとCoq-onlyのモデルを上回っていることを示します。
  論文  参考訳（メタデータ） (2025-02-07T05:35:46Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• Coupling Large Language Models with Logic Programming for Robust and General Reasoning from Text [5.532477732693001]
  大規模言語モデルは, 意味論的に非常に効果的な数ショットとして機能することを示す。 自然言語文を論理形式に変換し、応答集合プログラムの入力として機能する。 本手法は,bAbI, StepGame, CLUTRR, gSCAN など,いくつかのベンチマークにおいて最先端性能を実現する。
  論文  参考訳（メタデータ） (2023-07-15T03:29:59Z)
• Magnushammer: A Transformer-Based Approach to Premise Selection [20.445974111113223]
  我々は、(保護状態、関連する前提)ペアのテキスト表現を含む、前提選択のための新しいデータセットを開発し、オープンソース化する。 我々の手法であるMagnushammerは、Sledgehammerと呼ばれるインタラクティブな定理の証明において、最も先進的で広く使われている自動化ツールより優れています。 さらに、PISAベンチマークでは、最先端の証明成功率を57.0%から71.0%に改善し、パラメータを4ドル減らした。
  論文  参考訳（メタデータ） (2023-03-08T10:22:00Z)
• Zemi: Learning Zero-Shot Semi-Parametric Language Models from Multiple Tasks [77.90900650816046]
  ゼロショットセミパラメトリック言語モデルである$textZemi$を紹介します。 私たちは、新しいセミパラメトリックマルチタスクによるトレーニングパラダイムで、textZemi$をトレーニングします。 具体的には、大規模タスクに依存しない未ラベルコーパスからの検索により、マルチタスクトレーニングとゼロショット評価を強化する。
  論文  参考訳（メタデータ） (2022-10-01T04:08:50Z)
• An Application of Pseudo-Log-Likelihoods to Natural Language Scoring [5.382454613390483]
  比較的少ないパラメータとトレーニングステップを持つ言語モデルは、最近の大規模なデータセットでそれを上回るパフォーマンスを得ることができる。 二項選択タスクにおける常識推論のための絶対的最先端結果を生成する。 より小さなモデルの堅牢性は、構成性の観点から理解されるべきである。
  論文  参考訳（メタデータ） (2022-01-23T22:00:54Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。 我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
  論文  参考訳（メタデータ） (2021-02-11T18:59:24Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。