論文の概要: Experimental results from applying GPT-4 to an unpublished formal language

• arxiv url: http://arxiv.org/abs/2305.12196v1
• Date: Sat, 20 May 2023 14:00:08 GMT
• ステータス: 処理完了
• システム内更新日: 2023-05-23 23:57:24.640862
• Title: Experimental results from applying GPT-4 to an unpublished formal language
• Title（参考訳）: GPT-4を未発表の形式言語に適用した実験結果
• Authors: Gregor vom Scheidt
• Abstract要約: 最先端のシステムであるGPT-4は、未発表の形式システムのための簡潔な自然言語仕様を備えていた。 システムは全てのタスクを成功させ、広範なドメイン知識を示し、有用な新しい構文と意味論を発明し、一般化と推論能力を示した。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Can large language models be used to complete mathematical tasks that are traditionally performed either manually or with the aid of theorem provers? To answer this question, a state-of-the-art system, GPT-4, was provided with a concise natural language specification for a previously unpublished formal system and asked to complete a number of tasks, from stating function and type definitions to proving simple theorems and verifying user-supplied proofs. The system completed all tasks successfully, showed extensive domain knowledge, invented helpful new syntax and semantics, and exhibited generalization and inference abilities. So the answer seems to be: yes.
• Abstract（参考訳）: 大規模言語モデルは、手動または定理証明者の助けを借りて伝統的に実行される数学的なタスクを完遂するために使用できるか? この質問に答えるために、最先端のシステムであるGPT-4は、未発表の形式システムのための簡潔な自然言語仕様を備えており、関数や型定義の記述から単純な定理の証明、ユーザが提供する証明の検証まで、多くのタスクを完了するよう求められた。 システムは全てのタスクを成功させ、広範なドメイン知識を示し、有用な新しい構文と意味論を考案し、一般化と推論能力を示した。 だから答えは次のようだ。

関連論文リスト

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• 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)
• Large Language Models' Understanding of Math: Source Criticism and Extrapolation [0.0]
  GPT-4モデルの数学的理解を評価する。 GPT-4が基本的な数学的概念さえも理解したことを示す科学的証拠を見つけることは困難である。
  論文  参考訳（メタデータ） (2023-11-12T07:52:32Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。 研究論文は大量の背景と文脈を必要とする。 本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
  論文  参考訳（メタデータ） (2023-10-12T00:50:24Z)
• FIMO: A Challenge Formal Dataset for Automated Theorem Proving [31.695624833932577]
  FIMOは、IMOレベルでの高度な自動定理証明を容易にするように設計されている。 公式な問題文は149で、非公式な問題記述とそれに対応する非公式な証明の両方を伴っている。
  論文  参考訳（メタデータ） (2023-09-08T12:34:28Z)
• Lila: A Unified Benchmark for Mathematical Reasoning [59.97570380432861]
  LILAは、23の多様なタスクと4次元からなる統一的な数学的推論ベンチマークである。 我々は,Pythonプログラムの形式でタスク命令とソリューションを収集することにより,20のデータセットベンチマークを拡張してベンチマークを構築した。 LILAで訓練された汎用数学的推論モデルであるBHASKARAを紹介する。
  論文  参考訳（メタデータ） (2022-10-31T17:41:26Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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