論文の概要: Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation

• arxiv url: http://arxiv.org/abs/2411.00863v1
• Date: Wed, 30 Oct 2024 18:00:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-05 14:50:26.548432
• Title: Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation
• Title（参考訳）: 仮説生成におけるLCM学習のための最適データ順序付けを前提とした次世代予測タスク
• Authors: Chenyang An, Shima Imani, Feng Yao, Chengyu Dong, Ali Abbasi, Harsh Shrivastava, Samuel Buss, Jingbo Shang, Gayathri Mahalingam, Pramod Sharma, Maurice Diesendruck,
• Abstract要約: 1つのトレーニングデータサンプルの最適順序は、特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに発生すると論じる。 証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。
• 参考スコア（独自算出の注目度）: 27.60611509339328
• License:
• Abstract: In the field of large language model (LLM)-based proof generation, despite being trained on extensive corpora such as OpenWebMath and Arxiv, these models still exhibit only modest performance on proving tasks of moderate difficulty. We believe that this is partly due to the suboptimal order of each proof data used in training. Published proofs often follow a purely logical order, where each step logically proceeds from the previous steps based on the deductive rules. However, this order aims to facilitate the verification of the proof's soundness, rather than to help people and models learn the discovery process of the proof. In proof generation, we argue that the optimal order for one training data sample occurs when the relevant intermediate supervision for a particular proof step in the proof is always positioned to the left of that proof step. We call such order the intuitively sequential order. We validate our claims using two tasks: intuitionistic propositional logic theorem-proving and digit multiplication. Our experiments verify the order effect and provide support for our explanations. We demonstrate that training is most effective when the proof is in the intuitively sequential order. Moreover, the order effect and the performance gap between models trained on different data orders are substantial -- with an 11 percent improvement in proof success rate observed in the propositional logic theorem-proving task, between models trained on the optimal order compared to the worst order.
• Abstract（参考訳）: 大規模言語モデル(LLM)ベースの証明生成の分野では、OpenWebMathやArxivのような広範囲なコーパスで訓練されているにもかかわらず、これらのモデルは、適度な困難さを示すタスクに対して、まだ穏やかなパフォーマンスしか示さない。 これは、トレーニングで使用する各証明データの最適下順序によるものであると考えています。 公表された証明はしばしば純粋に論理的な順序に従っており、各ステップは導出規則に基づいて前のステップから論理的に進行する。 しかし、この命令は、人やモデルが証明の発見過程を学ぶのを助けるのではなく、証明の健全性を検証することを目的としている。 証明生成において、1つのトレーニングデータサンプルの最適順序は、その証明ステップの特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに生じると論じる。 このような順序を直感的に逐次順序と呼ぶ。 我々は直観論的命題論理定理の証明と桁乗算という2つのタスクを用いて主張を検証する。 本実験では, 注文効果を検証し, 説明支援を行う。 証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。 さらに、異なるデータ順序でトレーニングされたモデル間の順序効果とパフォーマンスギャップは、非常に大きい -- 命題論理定理証明タスクで観察された証明成功率を、最悪の順序よりも最適な順序でトレーニングされたモデル間で11%改善する。

関連論文リスト

• ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
  リーンの任意のユーザ定義メトリクスを最適化するために、証明を書き換える大規模な言語モデルエージェントであるImProverを紹介します。 我々は、現実世界の学部生、競争、研究レベルの数学定理の書き換えについてImProverをテストする。
  論文  参考訳（メタデータ） (2024-10-07T05:14:18Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving [41.23045212775232]
  探索経路の失敗から学習する訓練モデルの利点を実証する。 既存のオープンソース定理証明データセットにそのような試行錯誤データが欠如しているにもかかわらず、直観論的命題論理定理のデータセットをキュレートする。 比較的短いトライアル・アンド・エラー情報(TrialMaster)で訓練されたモデルと、正しい経路でのみ訓練されたモデルを比較し、前者が低いトライアル探索でより目に見えない定理を解くことを発見した。
  論文  参考訳（メタデータ） (2024-04-10T23:01:45Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Premise Order Matters in Reasoning with Large Language Models [57.18850969634412]
  大規模言語モデル (LLM) は,前提の順序に驚くほど脆弱であることを示す。 前提順序が中間的推論ステップで要求されるコンテキストと一致した場合, LLM が最高の性能を達成することを観察する。
  論文  参考訳（メタデータ） (2024-02-14T04:50:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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