論文の概要: An Evaluation Benchmark for Autoformalization in Lean4

• arxiv url: http://arxiv.org/abs/2406.06555v1
• Date: Sat, 1 Jun 2024 07:06:57 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-23 13:55:28.385738
• Title: An Evaluation Benchmark for Autoformalization in Lean4
• Title（参考訳）: Lean4におけるオートフォーマライゼーションの評価ベンチマーク
• Authors: Aryan Gulati, Devanshu Ladsaria, Shubhra Mishra, Jasdeep Sidhu, Brando Miranda,
• Abstract要約: 大規模言語モデル(LLM)は、自己形式化に革命をもたらす可能性を秘めている。 数学的プログラミング言語であるLean4の導入は、LLMの自動形式化機能を厳格に評価する前例のない機会を提供する。 本稿では,GPT-3.5,GPT-4,Gemini Proなどの最先端LLMの能力をテストするために,Lean4用に設計された新しい評価ベンチマークを提案する。
• 参考スコア（独自算出の注目度）: 1.2564343689544843
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) hold the potential to revolutionize autoformalization. The introduction of Lean4, a mathematical programming language, presents an unprecedented opportunity to rigorously assess the autoformalization capabilities of LLMs. This paper introduces a novel evaluation benchmark designed for Lean4, applying it to test the abilities of state-of-the-art LLMs, including GPT-3.5, GPT-4, and Gemini Pro. Our comprehensive analysis reveals that, despite recent advancements, these LLMs still exhibit limitations in autoformalization, particularly in more complex areas of mathematics. These findings underscore the need for further development in LLMs to fully harness their potential in scientific research and development. This study not only benchmarks current LLM capabilities but also sets the stage for future enhancements in autoformalization.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、自己形式化に革命をもたらす可能性を秘めている。 数学的プログラミング言語であるLean4の導入は、LLMの自動形式化機能を厳格に評価する前例のない機会を提供する。 本稿では,GPT-3.5,GPT-4,Gemini Proなどの最先端LLMの能力をテストするために,Lean4用に設計された新しい評価ベンチマークを提案する。 我々の包括的分析は、最近の進歩にもかかわらず、これらのLSMは、特により複雑な数学領域において、自己形式化の限界をまだ示していることを示している。 これらの知見は、科学研究と開発においてその可能性を完全に活用するために、LLMのさらなる開発の必要性を浮き彫りにしている。 この研究は、現在のLLM能力のベンチマークだけでなく、将来的な自動形式化の強化のステージも設定する。

関連論文リスト

• Robust Planning with LLM-Modulo Framework: Case Study in Travel Planning [19.79128776490271]
  本稿では,大規模言語モデルの多種多様な計画・推論活動への統合を促進する枠組みを提案する。 我々は,OSU NLPグループによる旅行計画ベンチマークを用いて,有効な旅程作成におけるLLMの性能評価を行う。 LLM-Modulo framework for TravelPlanning Domainの運用により、GPT4-Turboの4.6倍、GPT3.5-Turboのような古いモデルでは0%から5%のベースライン性能が向上した。
  論文  参考訳（メタデータ） (2024-05-31T05:23:35Z)
• Decompose and Aggregate: A Step-by-Step Interpretable Evaluation Framework [75.81096662788254]
  大規模言語モデル(LLM)はスケーラブルで経済的な評価指標である。 これらの評価者がどの程度信頼できるかという問題は、重要な研究課題として浮上している。 本稿では,デコンプリートとアグリゲートを提案し,その評価プロセスを教育実践に基づいて異なる段階に分解する。
  論文  参考訳（メタデータ） (2024-05-24T08:12:30Z)
• Toward Self-Improvement of LLMs via Imagination, Searching, and Criticizing [56.75702900542643]
  大規模言語モデルの自己改善のためのAlphaLLMを紹介する。 モンテカルロ木探索(MCTS)とLLMを統合し、自己改善ループを確立する。 実験の結果,AlphaLLM は付加アノテーションを使わずに LLM の性能を大幅に向上することがわかった。
  論文  参考訳（メタデータ） (2024-04-18T15:21:34Z)
• SciAssess: Benchmarking LLM Proficiency in Scientific Literature Analysis [26.111514038691837]
  SciAssessは、科学文献分析におけるLarge Language Models(LLM)の総合的な評価のためのベンチマークである。 記憶機能評価(L1)、記憶機能評価(L2)、分析・推論機能評価(L3)により,LLMの有効性を徹底的に評価することを目的とする。 それは、生物学、化学、材料、医学など、様々な科学分野から引き出された様々なタスクを含んでいる。
  論文  参考訳（メタデータ） (2024-03-04T12:19:28Z)
• Benchmarking LLMs via Uncertainty Quantification [91.72588235407379]
  オープンソースのLarge Language Models(LLM)の普及は、包括的な評価方法の緊急の必要性を強調している。 我々は不確実性定量化を統合した LLM のための新しいベンチマーク手法を提案する。 以上の結果より, 精度の高いLSMでは, 精度が低下する可能性があり, II) より大規模なLSMでは, より小型のLSMに比べて不確実性が高いこと, III) 命令ファインタニングではLCMの不確実性が高くなる傾向が示唆された。
  論文  参考訳（メタデータ） (2024-01-23T14:29:17Z)
• Supervised Knowledge Makes Large Language Models Better In-context Learners [94.89301696512776]
  大規模言語モデル(LLM)は、素早い工学を通して、文脈内学習能力の出現を示す。 自然言語理解と質問応答におけるLLMの一般化性と事実性の向上という課題は、まだ未解決のままである。 本研究では, LLM の信頼性を高める枠組みを提案する。1) 分布外データの一般化,2) 差別モデルによる LLM のメリットの解明,3) 生成タスクにおける幻覚の最小化。
  論文  参考訳（メタデータ） (2023-12-26T07:24:46Z)
• Benchmarking Generation and Evaluation Capabilities of Large Language Models for Instruction Controllable Summarization [132.25202059478065]
  命令制御可能なテキスト要約の大規模言語モデル(LLM)をベンチマークする。 本研究は,LLMにおいて,命令制御可能なテキスト要約が依然として困難な課題であることを示す。
  論文  参考訳（メタデータ） (2023-11-15T18:25:26Z)
• Are Large Language Models Reliable Judges? A Study on the Factuality Evaluation Capabilities of LLMs [8.526956860672698]
  大きな言語モデル(LLM)は、その顕著な能力のために注目を集めている。 本研究では,テキスト生成モデルにより生成された要約における事実整合性の信頼性評価としてのLCMの可能性について検討する。
  論文  参考訳（メタデータ） (2023-11-01T17:42:45Z)
• A Large Language Model Approach to Educational Survey Feedback Analysis [0.0]
  本稿では,大規模言語モデル(LLM) GPT-4 と GPT-3.5 が教育フィードバック調査から洞察を得るのに役立つ可能性について検討する。
  論文  参考訳（メタデータ） (2023-09-29T17:57:23Z)
• Through the Lens of Core Competency: Survey on Evaluation of Large Language Models [27.271533306818732]
  大規模言語モデル(LLM)は優れた性能と幅広い実用性を持っている。 既存の評価タスクは、現実世界のシナリオにおける幅広いアプリケーションに追いつくのは難しい。 LLMの4つのコア能力は、推論、知識、信頼性、安全性などである。 この能力アーキテクチャの下では、類似したタスクを組み合わせて対応する能力を反映し、新しいタスクをシステムに簡単に追加することができる。
  論文  参考訳（メタデータ） (2023-08-15T17:40:34Z)
• Large Language Models are Not Yet Human-Level Evaluators for Abstractive Summarization [66.08074487429477]
  抽象的な要約のための自動評価器として,大規模言語モデル(LLM)の安定性と信頼性について検討する。 また、ChatGPTとGPT-4は、一般的に使われている自動測定値よりも優れていますが、人間の代替品として準備ができていません。
  論文  参考訳（メタデータ） (2023-05-22T14:58:13Z)

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

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