Fugu-MT 論文翻訳(概要): Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning

論文の概要: Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning

arxiv url: http://arxiv.org/abs/2506.10903v1
Date: Thu, 12 Jun 2025 17:09:51 GMT
ステータス: 翻訳完了
システム内更新日: 2025-06-13 15:37:22.858835
Title: Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning
Title（参考訳）: 金標準を超える: フォーマルな数学的推論のためのLLM審査員のエピステマティクス・アンサンブル
Authors: Lan Zhang, Marco Valentino, Andre Freitas,
Abstract要約: 自動形式化タスクを評価するための,体系的かつ自動的な手法を提案する。提案手法は,論理的保存(LP),数学的整合性(MC),形式的妥当性(FV),形式的品質(FQ)を基準とした審査員のアンサンブルに基づく。全体としては,LLM審査員のEFGアンサンブルが評価に好適であることを示す。
参考スコア（独自算出の注目度）: 8.135142928659546
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Autoformalization plays a crucial role in formal mathematical reasoning by enabling the automatic translation of natural language statements into formal languages. While recent advances using large language models (LLMs) have shown promising results, methods for automatically evaluating autoformalization remain underexplored. As one moves to more complex domains (e.g., advanced mathematics), human evaluation requires significant time and domain expertise, especially as the complexity of the underlying statements and background knowledge increases. LLM-as-a-judge presents a promising approach for automating such evaluation. However, existing methods typically employ coarse-grained and generic evaluation criteria, which limit their effectiveness for advanced formal mathematical reasoning, where quality hinges on nuanced, multi-granular dimensions. In this work, we take a step toward addressing this gap by introducing a systematic, automatic method to evaluate autoformalization tasks. The proposed method is based on an epistemically and formally grounded ensemble (EFG) of LLM judges, defined on criteria encompassing logical preservation (LP), mathematical consistency (MC), formal validity (FV), and formal quality (FQ), resulting in a transparent assessment that accounts for different contributing factors. We validate the proposed framework to serve as a proxy for autoformalization assessment within the domain of formal mathematics. Overall, our experiments demonstrate that the EFG ensemble of LLM judges is a suitable emerging proxy for evaluation, more strongly correlating with human assessments than a coarse-grained model, especially when assessing formal qualities. These findings suggest that LLM-as-judges, especially when guided by a well-defined set of atomic properties, could offer a scalable, interpretable, and reliable support for evaluating formal mathematical reasoning.
Abstract（参考訳）: 自然言語文を形式言語に自動翻訳できるようにすることにより、形式的数学的推論において、オートフォーマル化は重要な役割を担っている。大規模言語モデル(LLM)を用いた最近の進歩は有望な結果を示しているが、自動形式化を自動評価する方法はまだ未検討である。より複雑な領域(例えば高度な数学)に移行するにつれて、人間の評価は、特に基礎となる文や背景知識の複雑さが増大するにつれて、かなりの時間と専門知識を必要とする。 LLM-as-a-judgeはそのような評価を自動化するための有望なアプローチを示す。しかし、既存の手法では一般に粗い粒度と総称的な評価基準を採用しており、より高度な形式的な数学的推論において、品質のヒンジはニュアンスドな多粒質次元に制限される。本研究は,自動形式化タスクを評価するための体系的,自動的な手法を導入することで,このギャップに対処するための一歩を踏み出した。提案手法は,論理的保存 (LP), 数学的整合性 (MC), 形式的妥当性 (FV), 形式的品質 (FQ) の基準に基づいて定義され, 様々な要因を考慮に入れた透明な評価を行う。本稿では,形式数学の領域内での自己形式化評価のプロキシとして,提案フレームワークを検証した。全体として,LLM審査員のEFGアンサンブルは,粗粒モデルよりも人的評価に強く関連し,特に形式的品質の評価において,評価に適していることを示す。これらの知見は, LLM-as-judges, 特に, 明確に定義された原子の性質によって導かれる場合, 形式的数学的推論を評価するためのスケーラブルで解釈可能で信頼性の高いサポートを提供する可能性が示唆された。

関連論文リスト

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文参考訳（メタデータ） (2025-05-05T15:37:00Z)
Multi-Agent LLM Judge: automatic personalized LLM judge design for evaluating natural language generation applications [0.0]
大規模言語モデル(LLM)は、さまざまなドメインにまたがって素晴らしいパフォーマンスを示しているが、ドメイン固有の知識の不足、バイアス、幻覚といった問題に直面している。単語重複やテキスト埋め込みに依存する従来の評価手法は、動的でオープンなテキスト生成を評価するのに必要なニュアンスドセマンティック情報を取得するには不十分である。本稿では,様々な自然言語生成アプリケーション向けにパーソナライズされたLLM判断器を自動設計する動的マルチエージェントシステムを提案する。
論文参考訳（メタデータ） (2025-04-01T09:36:56Z)
Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。 MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
論文参考訳（メタデータ） (2024-10-28T11:37:39Z)
Evaluating Mathematical Reasoning Beyond Accuracy [50.09931172314218]
推論ステップの品質を評価するための新しい方法論であるReasonEvalを紹介します。 ReasonEvalはメタ評価データセットのベースライン手法よりも一貫して優れていることを示す。我々は、ReasonEvalがデータ選択において重要な役割を果たすことを観察する。
論文参考訳（メタデータ） (2024-04-08T17:18:04Z)
HD-Eval: Aligning Large Language Model Evaluators Through Hierarchical Criteria Decomposition [92.17397504834825]
HD-Evalは、大規模な言語モデル評価ツールと人間の好みを反復的に調整するフレームワークである。 HD-Evalは、人間の専門家の評価思想から本質を継承し、LLMに基づく評価器のアライメントを強化する。 3つの評価領域に関する広範囲な実験は、HD-Evalのさらなる整合状態評価器の優位性を実証している。
論文参考訳（メタデータ） (2024-02-24T08:01:32Z)
PROXYQA: An Alternative Framework for Evaluating Long-Form Text Generation with Large Language Models [72.57329554067195]
ProxyQAは、長文生成を評価するための革新的なフレームワークである。さまざまなドメインにまたがる詳細なヒューマンキュレートされたメタクエストで構成されており、それぞれに事前にアノテートされた回答を持つ特定のプロキシクエストが伴っている。プロキシクエリに対処する際の評価器の精度を通じて、生成されたコンテンツの品質を評価する。
論文参考訳（メタデータ） (2024-01-26T18:12:25Z)
MR-GSM8K: A Meta-Reasoning Benchmark for Large Language Model Evaluation [60.65820977963331]
大規模言語モデル(LLM)のための新しい評価パラダイムを導入する。このパラダイムは、しばしば推論プロセスを無視する結果指向の評価から、より包括的な評価へと重点を移す。 GSM8Kデータセットにこのパラダイムを適用し,MR-GSM8Kベンチマークを開発した。
論文参考訳（メタデータ） (2023-12-28T15:49:43Z)
Post Turing: Mapping the landscape of LLM Evaluation [22.517544562890663]
本稿では,アラン・チューリングによる基礎的疑問からAI研究の現代まで,大規模言語モデル (LLM) 評価の歴史的軌跡を追究する。これらのモデルのより広範な社会的意味を考慮し、統一的な評価システムの必要性を強調した。この作業は、AIコミュニティがLLM評価の課題に協力して対処し、信頼性、公正性、社会的な利益を保証するために役立ちます。
論文参考訳（メタデータ） (2023-11-03T17:24:50Z)

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

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