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

TL;DR

This paper introduces an epistemic ensemble of LLM judges that systematically evaluates autoformalization in formal mathematics across multiple nuanced criteria, outperforming coarse-grained methods and aligning more closely with human judgment.

Contribution

It proposes a novel, multi-criteria LLM ensemble framework for automatic evaluation of formal mathematical reasoning, enhancing accuracy and interpretability.

Findings

The ensemble correlates better with human assessments than coarse models.

It effectively evaluates logical preservation, mathematical consistency, and formal validity.

The method offers a scalable and transparent evaluation approach.

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.