Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning

要約

オートフォーマル化は、自然言語声明の正式な言語への自動翻訳を可能にすることにより、正式な数学的推論において重要な役割を果たします。
大規模な言語モデル（LLM）を使用した最近の進歩は有望な結果を示していますが、自動体系化を自動的に評価する方法は露出していないままです。
より複雑なドメイン（例：高度な数学）に移動するにつれて、人間の評価には、特に基礎となる声明と背景知識の複雑さが増加するため、かなりの時間とドメインの専門知識が必要です。
LLM-as-a-a-judgeは、そのような評価を自動化するための有望なアプローチを提示します。
ただし、既存の方法は通常、粗粒の一般的な評価基準を採用しています。これにより、高度な正式な数学的推論に対する有効性が制限されます。
この作業では、オートフォーマル化タスクを評価するための体系的で自動的な方法を導入することにより、このギャップに対処するための一歩を踏み出します。
提案された方法は、LLM審査員の認識論的および正式に接地されたアンサンブル（EFG）に基づいており、論理保存（LP）、数学的一貫性（MC）、正式な妥当性（FV）、および正式な品質（FQ）を含む基準で定義され、異なる貢献要因の説明を透明な評価を得ることができます。
提案されたフレームワークを検証して、正式な数学のドメイン内で自己法的化評価のプロキシとして機能します。
全体として、我々の実験は、LLM審査員のEFGアンサンブルが評価に適した新興プロキシであり、特に正式な品質を評価する場合、粗粒モデルよりも人間の評価とより強く相関することを示しています。
これらの調査結果は、特に明確に定義された原子特性に導かれた場合、LLM-As-Judgesが、正式な数学的推論を評価するためのスケーラブルで解釈可能で信頼できるサポートを提供できることを示唆しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google