論文の概要: 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能力のベンチマークだけでなく、将来的な自動形式化の強化のステージも設定する。

関連論文リスト

• Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions [8.135142928659546]
  我々は、ウィキペディア(Def_Wiki)とarXiv論文(Def_ArXiv)から定義を収集する、自動形式化のための2つの新しいリソースを紹介する。 我々は、Isabelle/HOLに定義を形式化する能力を解析し、LLMの範囲を評価した。 以上の結果から, miniF2Fのような既存のベンチマークと比較して, 定義がより困難であることが判明した。
  論文  参考訳（メタデータ） (2025-02-17T17:34:48Z)
• Truth or Mirage? Towards End-to-End Factuality Evaluation with LLM-Oasis [78.07225438556203]
  LLM-Oasisは、エンド・ツー・エンドの事実性評価をトレーニングするための最大のリソースである。 ウィキペディアからクレームを抽出し、これらのクレームのサブセットを偽造し、事実と非事実のテキストのペアを生成することで構築される。 次に、データセットの品質を検証し、事実性評価システムのための金の標準テストセットを作成するために、人間のアノテータに依存します。
  論文  参考訳（メタデータ） (2024-11-29T12:21:15Z)
• GIVE: Structured Reasoning of Large Language Models with Knowledge Graph Inspired Veracity Extrapolation [108.2008975785364]
  Graph Inspired Veracity Extrapolation (GIVE)は、パラメトリックメモリと非パラメトリックメモリを融合して、最小の外部入力で正確な推論を改善する新しい推論手法である。 GIVE は LLM エージェントをガイドして,最も関連する専門家データ (observe) を選択し,クエリ固有の発散思考 (reflect) に従事し,その情報を合成して最終的な出力 (speak) を生成する。
  論文  参考訳（メタデータ） (2024-10-11T03:05:06Z)
• DnA-Eval: Enhancing Large Language Model Evaluation through Decomposition and Aggregation [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)
• 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)

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

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