論文の概要: Psychometric-Based Evaluation for Theorem Proving with Large Language Models

• arxiv url: http://arxiv.org/abs/2502.00855v1
• Date: Sun, 02 Feb 2025 17:00:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-05 14:59:57.222490
• Title: Psychometric-Based Evaluation for Theorem Proving with Large Language Models
• Title（参考訳）: 大規模言語モデルを用いた理論証明のための心理測定に基づく評価
• Authors: Jianyu Zhang, Yongwang Zhao, Long Zhang, Jilin Hu, Xiaokun Luan, Zhiwei Xu, Feng Yang,
• Abstract要約: 本研究では,大規模言語モデル(LLM)を用いた定理証明のための心理測定に基づく評価手法を提案する。 難易度と差別度でデータセットにアノテートする計量計算法を提案し,特に,各定理をミニF2Fデータセットにアノテートし,LLMの性能に応じて様々な難易度に分類する。 我々は,注釈付きメトリクスとLLMのリアルタイム性能に基づいて,テストに最適な定理を動的に選択する適応評価法を設計する。
• 参考スコア（独自算出の注目度）: 14.101509169786349
• License:
• Abstract: Large language models (LLMs) for formal theorem proving have become a prominent research focus. At present, the proving ability of these LLMs is mainly evaluated through proof pass rates on datasets such as miniF2F. However, this evaluation method overlooks the varying importance of theorems. As a result, it fails to highlight the real performance disparities between LLMs and leads to high evaluation costs. This study proposes a psychometric-based evaluation method for theorem proving with LLMs, comprising two main components: Dataset Annotation and Adaptive Evaluation. First, we propose a metric calculation method to annotate the dataset with difficulty and discrimination metrics. Specifically, we annotate each theorem in the miniF2F dataset and grade them into varying difficulty levels according to the performance of LLMs, resulting in an enhanced dataset: miniF2F-Graded. Experimental results show that the difficulty grading in miniF2F-Graded better reflects the theorem difficulty perceived by LLMs. Secondly, we design an adaptive evaluation method to dynamically select the most suitable theorems for testing based on the annotated metrics and the real-time performance of LLMs. We apply this method to evaluate 10 LLMs. The results show that our method finely highlights the performance disparities between LLMs. It also reduces evaluation costs by using only 23% of the theorems in the dataset.
• Abstract（参考訳）: 形式的定理証明のための大規模言語モデル(LLM)は、顕著な研究の焦点となっている。 現在、これらのLSMの証明能力は、miniF2Fのようなデータセットの証明パスレートによって評価されている。 しかし、この評価法は定理の様々な重要性を見落としている。 その結果、LCM間の実際の性能格差を浮き彫りにせず、高い評価コストにつながる。 本研究では,LLMを用いた定理証明のための心理測定に基づく評価手法を提案する。 まず,難易度と識別度でデータセットにアノテートするメトリクス計算手法を提案する。 具体的には、各定理をMiniF2Fデータセットに注釈付けし、LLMの性能に応じて様々な難易度に分類し、拡張されたデータセットであるminiF2F-Gradedを生成する。 実験結果から, miniF2F-Graded のグラデーションの難しさは LLM が認識する定理の難しさを反映していることがわかった。 第2に、アノテーション付きメトリクスとLLMのリアルタイム性能に基づいて、テストに最も適した定理を動的に選択する適応評価法を設計する。 10LLMの評価に本手法を適用した。 その結果,本手法はLLM間の性能格差を微妙に強調することがわかった。 また、データセットの定理の23%しか使用せず、評価コストを削減できる。

関連論文リスト

• Performance Law of Large Language Models [58.32539851241063]
  性能法則は、LLMアーキテクチャの選択と計算資源の効率的な割り当てを導くために用いられる。 性能法則は、LLMアーキテクチャの選択と計算資源の効率的な割り当てを広範な実験なしで導くのに利用できる。
  論文  参考訳（メタデータ） (2024-08-19T11:09:12Z)
• Evaluating Human Alignment and Model Faithfulness of LLM Rationale [66.75309523854476]
  大規模言語モデル(LLM)が,その世代を理論的にどのように説明するかを考察する。 提案手法は帰属に基づく説明よりも「偽り」が少ないことを示す。
  論文  参考訳（メタデータ） (2024-06-28T20:06:30Z)
• MindStar: Enhancing Math Reasoning in Pre-trained LLMs at Inference Time [51.5039731721706]
  MindStarは、大言語モデルの純粋に推論に基づく探索手法である。 推論タスクを探索問題として定式化し、最適な推論経路を特定するための2つの探索アイデアを提案する。 Llama-2-13BやMistral-7Bのようなオープンソースモデルの推論能力を大幅に向上させ、GPT-3.5やGrok-1に匹敵する性能を実現している。
  論文  参考訳（メタデータ） (2024-05-25T15:07:33Z)
• DnA-Eval: Enhancing Large Language Model Evaluation through Decomposition and Aggregation [75.81096662788254]
  大規模言語モデル(LLM)はスケーラブルで経済的な評価指標である。 これらの評価者がどの程度信頼できるかという問題は、重要な研究課題として浮上している。 本稿では,デコンプリートとアグリゲートを提案し,その評価プロセスを教育実践に基づいて異なる段階に分解する。
  論文  参考訳（メタデータ） (2024-05-24T08:12:30Z)
• Large Language Models are Inconsistent and Biased Evaluators [2.136983452580014]
  我々は,Large Language Models (LLMs) が親しみの偏りを示し,評価の歪んだ分布を示すため,評価値の偏りを示すことを示した。 また, LLM は不整合性評価器であり, テキスト品質の人間の理解に欠かせない相違を誘発する「サンプル間合意」が低く, 感度が高いことがわかった。
  論文  参考訳（メタデータ） (2024-05-02T20:42:28Z)
• Do Large Language Models Rank Fairly? An Empirical Study on the Fairness of LLMs as Rankers [27.66626125248612]
  本稿では,TREC Fair Ranking データセットを用いて,Large Language Models (LLMs) の評価実験を行った。 本稿では, 歴史的に検索結果に乏しい, 性別や地理的位置などの二項保護属性の表現に焦点を当てる。 我々の分析は、これらのLCMがこれらの属性に関連するクエリやドキュメントをどのように扱うのかを考察し、ランキングアルゴリズムのバイアスを明らかにすることを目的としている。
  論文  参考訳（メタデータ） (2024-04-04T04:23:19Z)
• Evaluating the Factuality of Large Language Models using Large-Scale Knowledge Graphs [30.179703001666173]
  大規模言語モデル(LLM)にとって、ファクチュアリティの問題は重要な問題である 我々は,かなり大きなテストデータセットを用いて,LLMの性能を評価するためにGraphEvalを提案する。 テストデータセットは、高価な人的努力なしで1000万以上の事実を持つ大規模な知識グラフから取得される。
  論文  参考訳（メタデータ） (2024-04-01T06:01:17Z)
• Comprehensive Reassessment of Large-Scale Evaluation Outcomes in LLMs: A Multifaceted Statistical Approach [64.42462708687921]
  評価の結果、スケーリング、トレーニングタイプ、アーキテクチャなどの要因がLLMのパフォーマンスに大きな影響を与えていることが明らかになった。 本研究は, これらのLCMの徹底的な再検討に着手し, 現状評価手法における不整合性に着目した。 これには、ANOVA、Tukey HSDテスト、GAMM、クラスタリング技術などが含まれる。
  論文  参考訳（メタデータ） (2024-03-22T14:47:35Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  大規模言語モデル(LLM)は、知識探索タスクにおける高い性能のため、知識ベースとして扱われてきた。 LLMが実際に正しい答えを連続的に生成する能力をどのように評価するか。 LLMの信頼性を直接測定するための新しい指標であるMOdel kNowledge relIabiliTy score (MONITOR)を提案する。
  論文  参考訳（メタデータ） (2023-10-15T12:40:30Z)

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

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