論文の概要: EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages

• arxiv url: http://arxiv.org/abs/2402.16878v1
• Date: Mon, 12 Feb 2024 19:10:11 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-03 19:21:57.892100
• Title: EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages
• Title（参考訳）: EvoGPT-f:形式数学言語のベンチマークのための進化的GPTフレームワーク
• Authors: Johnathan Mercer
• Abstract要約: 形式数学は、数学をプログラミング言語に翻訳する分野である。 本稿では、5つの形式数学コーパスの微分機械学習性に関する最初の体系的定量的分析のための進化的枠組みを紹介する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Formal mathematics is the discipline of translating mathematics into a programming language in which any statement can be unequivocally checked by a computer. Mathematicians and computer scientists have spent decades of painstaking formalization efforts developing languages such as Coq, HOL, and Lean. Machine learning research has converged on these formal math corpora and given rise to an assortment of methodologies to aid in interactive and automated theorem proving. However, these papers have primarily focused on one method, for one proof task, in one language. This paper introduces EvoGPT-f: a novel evolutionary framework for the first systematic quantitative analysis of the differential machine learnability of five formal math corpora (Lean 3, Lean 4, Coq, HOL 4, HOL Light) using four tokenization methods (character, word-level, Byte Pair Encoding and StarCoder tokenizer). This paper does not put to rest the question of the "best" or "easiest" language to learn. Rather, this framework and preliminary findings begin to illuminate the differential machine learnability of these languages, offering a foundation to forge more systematic quantitative and qualitative comparative research across communities.
• Abstract（参考訳）: フォーマル数学(英: Formal mathematics)とは、任意の文をコンピュータで不当にチェックできるプログラミング言語に翻訳する分野である。 数学者やコンピュータ科学者は、coq、hol、leanといった言語の開発に数十年を費やしてきた。 機械学習の研究は、これらの形式的数学コーパスに収束し、対話的かつ自動化された定理証明を支援する方法論の多さを生み出した。 しかしながら、これらの論文は主に1つの証明課題のための1つの方法に焦点を当てている。 本稿では, 4つのトークン化手法(文字, 単語レベル, Byte Pair Encoding および StarCoder tokenizer)を用いて, 5つの形式数学コーパス(Lean, Lean 4, Coq, HOL 4, HOL Light)の微分機械学習性を, 初めて体系的に定量的に解析する進化的フレームワークであるEvoGPT-fを紹介する。 この論文は、学習すべき「最も良い」「最も簡単な」言語についての疑問を残さない。 むしろ、このフレームワークと予備的な発見は、これらの言語の微分機械学習可能性の照らし出し始め、コミュニティ全体でより体系的な量的および質的な比較研究を構築する基盤を提供する。

関連論文リスト

• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 以前、23のリーンリポジトリで人間が公式に証明していなかった155の定理の証明に成功した。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• 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 Workbook: A large-scale Lean problem set formalized from natural language math problems [50.22847430754973]
  大規模な言語モデルは、リーンのような形式言語を使って証明する数学の定理が得意ではありません。 この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。 本稿では,自然言語の数学的問題をリーン4文に変換するために,合成データを反復的に生成・フィルタリングするパイプラインを提案する。
  論文  参考訳（メタデータ） (2024-06-06T08:25:43Z)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。 我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
  論文  参考訳（メタデータ） (2023-10-25T23:54:04Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。 研究論文は大量の背景と文脈を必要とする。 本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
  論文  参考訳（メタデータ） (2023-10-12T00:50:24Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。 大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
  論文  参考訳（メタデータ） (2022-12-20T18:46:16Z)
• Lila: A Unified Benchmark for Mathematical Reasoning [59.97570380432861]
  LILAは、23の多様なタスクと4次元からなる統一的な数学的推論ベンチマークである。 我々は,Pythonプログラムの形式でタスク命令とソリューションを収集することにより,20のデータセットベンチマークを拡張してベンチマークを構築した。 LILAで訓練された汎用数学的推論モデルであるBHASKARAを紹介する。
  論文  参考訳（メタデータ） (2022-10-31T17:41:26Z)
• JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem Understanding [74.12405417718054]
  本稿では,中国初の数学的事前学習言語モデル(PLM)を提示することにより,機械の数学的知性向上を目指す。 他の標準のNLPタスクとは異なり、数学的テキストは問題文に数学的用語、記号、公式を含むため理解が難しい。 基礎課程と上級課程の両方からなる数学PLMの学習を改善するための新しいカリキュラム事前学習手法を設計する。
  論文  参考訳（メタデータ） (2022-06-13T17:03:52Z)
• Learning to Match Mathematical Statements with Proofs [37.38969121408295]
  このタスクは、研究レベルの数学的テキストの処理を改善するために設計されている。 我々は180k以上の文対からなるタスク用のデータセットをリリースする。 課題をグローバルに検討し,重み付き二部マッチングアルゴリズムを用いることで,課題に対処できることが示唆された。
  論文  参考訳（メタデータ） (2021-02-03T15:38:54Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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