Fugu-MT 論文翻訳(概要): MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data

論文の概要: MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data

arxiv url: http://arxiv.org/abs/2402.08957v3
Date: Thu, 23 May 2024 03:13:23 GMT
ステータス: 処理完了
システム内更新日: 2024-05-25 06:50:03.316641
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が検証された高品質なステップバイステップデータを生成することを示す。
参考スコア（独自算出の注目度）: 85.50740598523818
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の推論能力を探究するドメインにアピールするが、それでも重要な課題に直面している。 CoT(Chain-of-Thought)のような従来の研究は、中間ステップガイダンスの有効性を明らかにしている。しかし、このようなステップワイズアノテーションは多大な労力を必要とするため、現在のベンチマークのトレーニングステップは不十分である。このギャップを埋めるために、この研究はMUSTARDという、高品質で多様性の高い定理と証明データの統一的な合成をマスターするデータ生成フレームワークを導入している。 MUSTARDは、(1)問題カテゴリとしていくつかの数学的概念種をサンプリングする。 2) 次に,サンプル概念を用いた生成言語モデルを作成し,その問題とステップワイドな形式的解を求める。 (3) 最後に、このフレームワークは証明アシスタント(例:Lean Prover)を使用して、有効な証明をフィルタリングします。提案したMUSTARDでは、5,866個の有効なデータポイントを持つMUSTARDSAUCEの定理と安全性を示すベンチマークを提示する。各データポイントは、非公式なステートメント、非公式な証明、そして証明者検証に合格する翻訳された公式な証明を含む。我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。さらに、より小型の言語モデルにMUSTARDSAUCEを適用する。微調整されたLlama 2-7Bは、自動定理の証明において平均相対的な性能が15.41%、数学用語の問題では8.18%に達する。コードとデータはhttps://github.com/Eleanor-H/MUSTARD.comで公開されている。

関連論文リスト

MindStar: Enhancing Math Reasoning in Pre-trained LLMs at Inference Time [51.5039731721706]
MindStarは、大言語モデルの純粋に推論に基づく探索手法である。推論タスクを探索問題として定式化し、最適な推論経路を特定するための2つの探索アイデアを提案する。 Llama-2-13BやMistral-7Bのようなオープンソースモデルの推論能力を大幅に向上させ、GPT-3.5やGrok-1に匹敵する性能を実現している。
論文参考訳（メタデータ） (2024-05-25T15:07:33Z)
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。この合成データセットでDeepSeekMath 7Bモデルを微調整します。我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文参考訳（メタデータ） (2024-05-23T09:03:42Z)
General Purpose Verification for Chain of Thought Prompting [16.381123651223763]
大規模言語モデル(LLM)の推論能力を改善する方法について検討する。我々は、モデルが推論中に従うべき3つの一般的な原則を提案する。これらの制約をLLMが生成する推論ステップに適用し、最終生成の精度を向上させる。
論文参考訳（メタデータ） (2024-04-30T21:15:17Z)
Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code [0.0]
Coqの証明アシスタントは、数学的アサーションとソフトウェアの正確性を検証するための厳格なアプローチで際立っている。人工知能と機械学習の進歩にもかかわらず、Coq構文と意味論の特殊性は大規模言語モデル(LLM)に固有の課題をもたらす。このデータセットは、10,000以上のCoqソースファイルのコレクションから派生したもので、幅広い命題、証明、定義を含んでいる。
論文参考訳（メタデータ） (2024-03-19T10:53:40Z)
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)
PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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