論文の概要: TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models

• arxiv url: http://arxiv.org/abs/2310.10180v2
• Date: Tue, 24 Oct 2023 15:17:56 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-25 23:06:28.304123
• Title: TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models
• Title（参考訳）: TRIGO:生成言語モデルのための形式的数学的証明のベンチマーク
• Authors: Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, Qun Liu
• Abstract要約: 本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
• 参考スコア（独自算出の注目度）: 68.65075559137608
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated theorem proving (ATP) has become an appealing domain for exploring the reasoning ability of the recent successful generative language models. However, current ATP benchmarks mainly focus on symbolic inference, but rarely involve the understanding of complex number combination reasoning. In this work, we propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas and its capability to manipulate, group, and factor number terms. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We then automatically generate additional examples from the annotated samples to expand the dataset. Furthermore, we develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability. Our extensive experiments show our proposed TRIGO poses a new challenge for advanced generative LM's including GPT-4 which is pre-trained on a considerable amount of open-source formal theorem-proving language data, and provide a new tool to study the generative LM's ability on both formal and mathematical reasoning.
• Abstract（参考訳）: 自動定理証明(ATP)は、最近成功した生成言語モデルの推論能力を探究する上で魅力的な領域となっている。 しかし、現在のATPベンチマークは主にシンボリック推論に焦点を当てているが、複素数組合せの推論を理解することは滅多にない。 本研究では, ATP ベンチマーク TRIGO を提案する。このベンチマークは, ステップバイステップの証明で三角法式を縮小するモデルを必要とするだけでなく, 論理式に対する生成的 LM の推論能力とその操作, グループ化, 因子数項の操作能力を評価する。 我々は、Webから三角法式とその縮小形式を収集し、手作業で単純化プロセスを注釈化し、それをリーン形式言語システムに翻訳する。 その後、アノテーション付きサンプルからサンプルを自動生成してデータセットを拡張する。 さらに,Lean-Gymに基づく自動生成装置を開発し,モデルの一般化能力を徹底的に分析するために,様々な困難と分布のデータセット分割を作成する。 提案するTRIGOは,多量のオープンソース形式定理証明言語データに基づいて事前学習された GPT-4 を含む先進的生成型LMの新たな課題を示すとともに,形式的および数学的推論において,生成型LMの能力を研究するための新しいツールを提供する。

関連論文リスト

• SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
  本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。 英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
  論文  参考訳（メタデータ） (2024-08-28T06:33:03Z)
• Slaves to the Law of Large Numbers: An Asymptotic Equipartition Property for Perplexity in Generative Language Models [0.0]
  言語モデルが生成する大きなテキストの難易度は,トークン分布の平均エントロピーに収束しなければならないことを示す。 この作業は、AI検出の理解と改善のための実践的な応用を可能にする。
  論文  参考訳（メタデータ） (2024-05-22T16:23:40Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Discovering Interpretable Physical Models using Symbolic Regression and Discrete Exterior Calculus [55.2480439325792]
  本稿では,記号回帰(SR)と離散指数計算(DEC)を組み合わせて物理モデルの自動発見を行うフレームワークを提案する。 DECは、SRの物理問題への最先端の応用を越えている、場の理論の離散的な類似に対して、ビルディングブロックを提供する。 実験データから連続体物理の3つのモデルを再発見し,本手法の有効性を実証する。
  論文  参考訳（メタデータ） (2023-10-10T13:23:05Z)
• Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought [10.524051272257614]
  大規模言語モデル(LLM)は、チェーン・オブ・シークレット・プロンプトが与えられた顕著な推論能力を示している。 本稿では, PrOntoQAと呼ばれる合成質問応答データセットを提案し, それぞれの例を合成世界モデルとして生成する。 これにより、生成された連鎖を形式解析の象徴的な証明に解析することができる。
  論文  参考訳（メタデータ） (2022-10-03T21:34:32Z)
• 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)
• Text Modular Networks: Learning to Decompose Tasks in the Language of Existing Models [61.480085460269514]
  本稿では,既存のモデルで解けるより単純なモデルに分解することで,複雑なタスクを解くための解釈可能なシステムを構築するためのフレームワークを提案する。 我々はこのフレームワークを用いて、ニューラルネットワークのファクトイド単一スパンQAモデルとシンボリック電卓で答えられるサブクエストに分解することで、マルチホップ推論問題に答えられるシステムであるModularQAを構築する。
  論文  参考訳（メタデータ） (2020-09-01T23:45:42Z)
• Closed-Form Expressions for Global and Local Interpretation of Tsetlin Machines with Applications to Explaining High-Dimensional Data [7.05622249909585]
  TMモデルが特定の予測を行う理由(局所的解釈可能性)を理解するためのクローズドフォーム表現を提案する。 また、連続した特徴に対する特徴値範囲の重要性を測定するための式も導入する。 分類と回帰については,XGBoost, Explainable Boosting Machines, Neural Additive Modelsと比較し, SHAPとの対応, および競合予測精度を示す。
  論文  参考訳（メタデータ） (2020-07-27T21:47:24Z)

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

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