論文の概要: MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
- arxiv url: http://arxiv.org/abs/2402.08957v2
- Date: Thu, 7 Mar 2024 13:02:58 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-08 16:56:00.523057
- Title: MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
- Title(参考訳): MUSTARD:理論と証明データの一様合成をマスターする
- Authors: Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin,
Haiming Wang, Zhenguo Li, Linqi Song, Xiaodan Liang
- Abstract要約: MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
- 参考スコア(独自算出の注目度): 88.72298746872396
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Recent large language models (LLMs) have witnessed significant advancement in
various tasks, including mathematical reasoning and theorem proving. As these
two tasks require strict and formal multi-step inference, they are appealing
domains for exploring the reasoning ability of LLMs but still face important
challenges. Previous studies such as Chain-of-Thought (CoT) have revealed the
effectiveness of intermediate steps guidance. However, such step-wise
annotation requires heavy labor, leading to insufficient training steps for
current benchmarks. To fill this gap, this work introduces MUSTARD, a data
generation framework that masters uniform synthesis of theorem and proof data
of high quality and diversity. MUSTARD synthesizes data in three stages: (1) It
samples a few mathematical concept seeds as the problem category. (2) Then, it
prompts a generative language model with the sampled concepts to obtain both
the problems and their step-wise formal solutions. (3) Lastly, the framework
utilizes a proof assistant (e.g., Lean Prover) to filter the valid proofs. With
the proposed MUSTARD, we present a theorem-and-proof benchmark MUSTARDSAUCE
with 5,866 valid data points. Each data point contains an informal statement,
an informal proof, and a translated formal proof that passes the prover
validation. We perform extensive analysis and demonstrate that MUSTARD
generates validated high-quality step-by-step data. We further apply the
MUSTARDSAUCE for fine-tuning smaller language models. The fine-tuned Llama 2-7B
achieves a 15.41% average relative performance gain in automated theorem
proving, and 8.18% in math word problems. Codes and data are available at
https://github.com/Eleanor-H/MUSTARD.
- Abstract(参考訳): 最近の大規模言語モデル(llm)は、数学的推論や定理証明を含む様々なタスクにおいて重要な進歩を遂げている。
これらの2つのタスクは厳密で形式的な多段階推論を必要とするため、LLMの推論能力を探究するドメインにアピールするが、それでも重要な課題に直面している。
先行研究であるchain-of-thought (cot) は、中間ステップ指導の有効性を明らかにしている。
しかし、このようなステップワイズアノテーションは多大な労力を必要とするため、現在のベンチマークのトレーニングステップは不十分である。
このギャップを埋めるため、本研究では、高品質と多様性の証明データと定理の均一な合成を習得するデータ生成フレームワークである mustard を紹介する。
mustardはデータを3つの段階に合成する:(1)いくつかの数学的概念の種を問題カテゴリとしてサンプリングする。
2) サンプル概念を用いた生成言語モデルを構築し,問題とステップワイドな形式的解の両立を図った。
(3) 最後に、このフレームワークは証明アシスタント(例:Lean Prover)を使って有効な証明をフィルタリングする。
提案するマスタードを用いて、5,866点の有効データ点を持つ定理と証明のベンチマークを示す。
各データポイントは、非公式なステートメント、非公式な証明、そして証明者検証を通した変換された形式的証明を含む。
広範囲な分析を行い,検証された高品質なステップバイステップデータを生成することを実証する。
さらに、より小型の言語モデルにMUSTARDSAUCEを適用する。
微調整されたllama 2-7bは、自動定理証明で平均15.41%、数学用語問題で8.18%のパフォーマンス向上を達成している。
コードとデータはhttps://github.com/eleanor-h/mustardで入手できる。
関連論文リスト
- CHAMP: A Competition-level Dataset for Fine-Grained Analyses of LLMs'
Mathematical Reasoning Capabilities [29.06174003306662]
概念とHint-Annotated Math Problems (CHAMP) は、高校数学の競争問題である。
このベンチマークは困難で、最高のモデルは標準設定で58.1%しか得点できない。
モデルはしばしば、間違った推論ステップを通じて、正しい最終回答に到達します。
論文 参考訳(メタデータ) (2024-01-13T03:18:16Z) - 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) - 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) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳(メタデータ) (2023-10-16T08:42:39Z) - Guiding Language Model Math Reasoning with Planning Tokens [128.57605860640948]
各推論ステップの開始時に計画トークンを導入し、モデルのガイドとして機能し、モデルパラメータにそれらの埋め込みを追加する。
提案手法では、トレーニング可能なパラメータ(わずか0.001%)の無視可能な増加が必要であり、完全な微調整か、よりパラメータ効率の良いスキームで適用することができる。
論文 参考訳(メタデータ) (2023-10-09T13:29:37Z) - Evaluating and Improving Tool-Augmented Computation-Intensive Math
Reasoning [75.74103236299477]
CoT(Chain-of- Thought prompting)とツール拡張は、大きな言語モデルを改善するための効果的なプラクティスとして検証されている。
ツールインターフェース,すなわち textbfDELI を用いた推論ステップを考慮に入れた新しい手法を提案する。
CARPと他の6つのデータセットの実験結果から、提案されたDELIは、主に競合ベースラインを上回っていることが示された。
論文 参考訳(メタデータ) (2023-06-04T17:02:59Z) - WeCheck: Strong Factual Consistency Checker via Weakly Supervised
Learning [40.5830891229718]
本稿では,複数のリソースを集約して,正確かつ効率的な実測値(WeCheck)をトレーニングする,弱教師付きフレームワークを提案する。
様々なタスクに関する総合的な実験は、平均してTRUEベンチマークにおける従来の最先端手法よりも3.4%の絶対的な改善を実現するWeCheckの強い性能を示す。
論文 参考訳(メタデータ) (2022-12-20T08:04:36Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳(メタデータ) (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。