論文の概要: 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は、未発表の形式システムのための簡潔な自然言語仕様を備えており、関数や型定義の記述から単純な定理の証明、ユーザが提供する証明の検証まで、多くのタスクを完了するよう求められた。
システムは全てのタスクを成功させ、広範なドメイン知識を示し、有用な新しい構文と意味論を考案し、一般化と推論能力を示した。
だから答えは次のようだ。
関連論文リスト
- Large Language Models' Understanding of Math: Source Criticism and
Extrapolation [0.0]
GPT-4モデルの数学的理解を評価する。
GPT-4が基本的な数学的概念さえも理解したことを示す科学的証拠を見つけることは困難である。
論文 参考訳(メタデータ) (2023-11-12T07:52:32Z) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳(メタデータ) (2023-10-16T08:42:39Z) - A New Approach Towards Autoformalization [8.176989532546632]
オートフォーマル化(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) - STREET: A Multi-Task Structured Reasoning and Explanation Benchmark [56.555662318619135]
マルチタスクとマルチドメインの自然言語推論と説明ベンチマークを統一的に導入する。
我々は、モデルが質問に答えるだけでなく、ある解の正しさを証明できる中間的な結論を生成するために、問題の前提がどのように使われているかを記述する、段階的に構造化された説明を生成することを期待している。
論文 参考訳(メタデータ) (2023-02-13T22:34:02Z) - 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) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。
Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。
現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文 参考訳(メタデータ) (2020-12-20T18:15:12Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。