論文の概要: Large Language Models' Understanding of Math: Source Criticism and Extrapolation

• arxiv url: http://arxiv.org/abs/2311.07618v1
• Date: Sun, 12 Nov 2023 07:52:32 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-15 16:57:12.117324
• Title: Large Language Models' Understanding of Math: Source Criticism and Extrapolation
• Title（参考訳）: 大言語モデルによる数学の理解--情報源批判と外挿
• Authors: Roozbeh Yousefzadeh and Xuenan Cao
• Abstract要約: GPT-4モデルの数学的理解を評価する。 GPT-4が基本的な数学的概念さえも理解したことを示す科学的証拠を見つけることは困難である。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: It has been suggested that large language models such as GPT-4 have acquired some form of understanding beyond the correlations among the words in text including some understanding of mathematics as well. Here, we perform a critical inquiry into this claim by evaluating the mathematical understanding of the GPT-4 model. Considering that GPT-4's training set is a secret, it is not straightforward to evaluate whether the model's correct answers are based on a mathematical understanding or based on replication of proofs that the model has seen before. We specifically craft mathematical questions which their formal proofs are not readily available on the web, proofs that are more likely not seen by the GPT-4. We see that GPT-4 is unable to solve those problems despite their simplicity. It is hard to find scientific evidence suggesting that GPT-4 has acquired an understanding of even basic mathematical concepts. A straightforward way to find failure modes of GPT-4 in theorem proving is to craft questions where their formal proofs are not available on the web. Our finding suggests that GPT-4's ability is to reproduce, rephrase, and polish the mathematical proofs that it has seen before, and not in grasping mathematical concepts. We also see that GPT-4's ability to prove mathematical theorems is continuously expanding over time despite the claim that it is a fixed model. We suggest that the task of proving mathematical theorems in formal language is comparable to the methods used in search engines such as Google while predicting the next word in a sentence may be a misguided approach, a recipe that often leads to excessive extrapolation and eventual failures. Prompting the GPT-4 over and over may benefit the GPT-4 and the OpenAI, but we question whether it is valuable for machine learning or for theorem proving.
• Abstract（参考訳）: gpt-4のような大規模言語モデルは、数学の理解を含むテキスト中の単語間の相関以上の何らかの理解を得たと示唆されている。 本稿では,GPT-4モデルの数学的理解を評価することによって,この主張に対する批判的な考察を行う。 GPT-4のトレーニングセットが秘密であることを考えると、モデルの正しい答えが数学的理解に基づいているか、あるいはモデルが以前に見た証明の複製に基づいているかを簡単に評価することはできない。 我々は、その形式的証明がweb上では容易に利用できない数学的問題や、gpt-4では見られないであろう証明を特に作成する。 GPT-4は単純さにもかかわらずこれらの問題を解決することができない。 GPT-4が基本的な数学的概念さえも理解していることを示す科学的証拠を見つけるのは難しい。 定理証明において GPT-4 の失敗モードを見つけるための簡単な方法は、公式な証明が Web 上で利用できないような質問を作ることである。 我々の発見は, GPT-4の能力は, これまでに見た数学的証明を再現し, 表現し, 洗練することであり, 数学的概念を把握できないことを示唆している。 また、GPT-4の数学的定理を証明する能力は、固定モデルであるという主張にもかかわらず、時間とともに継続的に拡大している。 形式言語での数学的定理の証明のタスクは、googleのような検索エンジンで使われている手法に匹敵するものであり、文中の次の単語を予測することは誤った方法である可能性があり、しばしば過剰な外挿や結果の失敗をもたらすレシピである。 GPT-4 を何度も試すことは GPT-4 や OpenAI の恩恵を受けるかもしれないが,機械学習や定理証明に有用かどうか疑問視する。

関連論文リスト

• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。 目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
  論文  参考訳（メタデータ） (2024-09-09T18:21:28Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
  GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。 TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
  論文  参考訳（メタデータ） (2023-05-21T17:51:35Z)
• Experimental results from applying GPT-4 to an unpublished formal language [0.0]
  最先端のシステムであるGPT-4は、未発表の形式システムのための簡潔な自然言語仕様を備えていた。 システムは全てのタスクを成功させ、広範なドメイン知識を示し、有用な新しい構文と意味論を発明し、一般化と推論能力を示した。
  論文  参考訳（メタデータ） (2023-05-20T14:00:08Z)
• Sparks of Artificial General Intelligence: Early experiments with GPT-4 [66.1188263570629]
  OpenAIが開発したGPT-4は、前例のない規模の計算とデータを使って訓練された。 我々は, GPT-4が数学, コーディング, ビジョン, 医学, 法学, 心理学などにまたがる, 新規で困難な課題を解くことを実証した。 我々は、GPT-4を人工知能(AGI)システムの早期(まだ未完成)版と見なすことができると信じている。
  論文  参考訳（メタデータ） (2023-03-22T16:51:28Z)
• Mathematical Capabilities of ChatGPT [35.71603158908465]
  GHOSTSとminiGHOSTSの2つの新しいデータセットをリリースしています。 これらは、数学の研究者によって計算された最初の自然言語データセットである。 モデルを、詳細なパフォーマンス指標でベンチマークします。
  論文  参考訳（メタデータ） (2023-01-31T18:59:03Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Noisy Deductive Reasoning: How Humans Construct Math, and How Math Constructs Universes [0.5874142059884521]
  本稿では,数学が基本的な過程である数学的推論の計算モデルを提案する。 この枠組みが数学的実践のいくつかの側面について説得力のある説明を与えることを示す。
  論文  参考訳（メタデータ） (2020-10-28T19:43:14Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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