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

• URL: http://arxiv.org/abs/2506.10903v1
• Date: Thu, 12 Jun 2025 17:09:51 GMT
• Title: Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning
• Abstract summary: We introduce a systematic, automatic method to evaluate autoformalization tasks.<n>The proposed method is based on an ensemble of judges, defined on criteria encompassing logical preservation (LP), mathematical consistency (MC), formal validity (FV), and formal quality (FQ)<n>Overall, our experiments demonstrate that the EFG ensemble of LLM judges is a suitable emerging proxy for evaluation.
• Score: 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.

Related papers

• From Atomic to Agentic: Towards Interpretable Evaluation of LLMs' Agentic Mathematical Capabilities [103.60384544335072]
  Large Language Models (LLMs) are evolving from performing end-to-end mathematical reasoning to integrating agentic intelligence.<n>Our framework aligns problem-solving agentic behaviors with a structured taxonomy of reusable mathematical atomic capabilities.<n> Experiments reveal that models with similar end-to-end accuracy can exhibit markedly different agentic capability profiles.
  arXiv  Detail & Related papers  (2026-08-27T10:52:06Z)
• GDPR Auto-Formalization with AI Agents and Human Verification [2.103620138032182]
  We study the overall process of automatic formalization of provisions using large language models.<n>We adopt a role-specialized workflow in which AI components generate legal scenarios, formal rules, and atomic facts.<n>Our results show that structured verification and targeted human oversight are essential for reliable legal formalization.
  arXiv  Detail & Related papers  (2026-04-16T04:26:18Z)
• Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy [62.32144504442516]
  It is unknown whether SOTA LLMs can grasp the structured, hierarchical complexity of formal languages.<n>ChomskyBench is a benchmark for systematically evaluating LLMs through the lens of Chomsky Hierarchy.<n>ChomskyBench is composed of a comprehensive suite of language recognition and generation tasks designed to test capabilities at each level.
  arXiv  Detail & Related papers  (2026-04-03T04:06:39Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Conjecturing: An Overlooked Step in Formal Mathematical Reasoning [10.398167568549924]
  Many mathematical problems cannot be formalised directly without first conjecturing a conclusion.<n>We develop ConjectureBench to measure the conjecturing capabilities of Large Language Models.<n>We show that our method achieves the first successful end-to-end autoformalisation of 13 PutnamBench problems with GPT-4.1 and 7 with DeepSeek-V3.1.
  arXiv  Detail & Related papers  (2025-10-13T22:29:49Z)
• Expert Preference-based Evaluation of Automated Related Work Generation [54.29459509574242]
  We propose GREP, a multi-turn evaluation framework that integrates classical related work evaluation criteria with expert-specific preferences.<n>For better accessibility, we design two variants of GREP: a more precise variant with proprietary LLMs as evaluators, and a cheaper alternative with open-weight LLMs.
  arXiv  Detail & Related papers  (2025-08-11T13:08:07Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  We present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems.<n>We introduce a novel human-in-the-loop autoformalization pipeline that integrates statement autoformalization, semantic verification, and negation-based disproof filtering strategies.<n>Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations.
  arXiv  Detail & Related papers  (2025-05-05T15:37:00Z)
• Multi-Agent LLM Judge: automatic personalized LLM judge design for evaluating natural language generation applications [0.0]
  Large Language Models (LLMs) have demonstrated impressive performance across diverse domains, yet they still encounter challenges such as insufficient domain-specific knowledge, biases, and hallucinations.<n>Traditional evaluation methods, which rely on word overlap or text embeddings, are inadequate for capturing the nuanced semantic information necessary to evaluate dynamic, open-ended text generation.<n>We propose a novel dynamic multi-agent system that automatically designs personalized LLM judges for various natural language generation applications.
  arXiv  Detail & Related papers  (2025-04-01T09:36:56Z)
• Decoding AI Judgment: How LLMs Assess News Credibility and Bias [33.7054351451505]
  Large Language Models (LLMs) are increasingly embedded in that involve evaluative processes.<n>This raises the need to examine how such evaluations are built, what assumptions they rely on, and how their strategies diverge from those of humans.<n>We benchmark six LLMs against expert ratings--NewsGuard and Media Bias/Fact Check (MBFC)--and against human judgments collected through a controlled experiment.
  arXiv  Detail & Related papers  (2025-02-06T18:52:10Z)
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  We introduce a novel framework that scores and selects the best result from k autoformalization candidates based on symbolic equivalence and semantic consistency.<n>Our experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy.
  arXiv  Detail & Related papers  (2024-10-28T11:37:39Z)
• Auto-PRE: An Automatic and Cost-Efficient Peer-Review Framework for Language Generation Evaluation [52.76508734756661]
  Auto-PRE is an automatic evaluation framework inspired by the peer review process.<n>Unlike previous approaches that rely on human annotations, Auto-PRE automatically selects evaluators based on three core traits.<n> Experiments on three representative tasks, including summarization, non-factoid QA, and dialogue generation, demonstrate that Auto-PRE achieves state-of-the-art performance.
  arXiv  Detail & Related papers  (2024-10-16T06:06:06Z)
• Evaluating Human Alignment and Model Faithfulness of LLM Rationale [66.75309523854476]
  We study how well large language models (LLMs) explain their generations through rationales. We show that prompting-based methods are less "faithful" than attribution-based explanations.
  arXiv  Detail & Related papers  (2024-06-28T20:06:30Z)
• MR-Ben: A Meta-Reasoning Benchmark for Evaluating System-2 Thinking in LLMs [55.20845457594977]
  Large language models (LLMs) have shown increasing capability in problem-solving and decision-making.<n>We present a process-based benchmark MR-Ben that demands a meta-reasoning skill.<n>Our meta-reasoning paradigm is especially suited for system-2 slow thinking.
  arXiv  Detail & Related papers  (2024-06-20T03:50:23Z)
• Evaluating Mathematical Reasoning Beyond Accuracy [50.09931172314218]
  We introduce ReasonEval, a new methodology for evaluating the quality of reasoning steps.<n>We show that ReasonEval consistently outperforms baseline methods in the meta-evaluation datasets.<n>We observe that ReasonEval can play a significant role in data selection.
  arXiv  Detail & Related papers  (2024-04-08T17:18:04Z)
• Aligning with Human Judgement: The Role of Pairwise Preference in Large Language Model Evaluators [48.54465599914978]
  Large Language Models (LLMs) have demonstrated promising capabilities as automatic evaluators in assessing the quality of generated natural language.<n>LLMs still exhibit biases in evaluation and often struggle to generate coherent evaluations that align with human assessments.<n>We introduce Pairwise-preference Search (PAIRS), an uncertainty-guided search-based rank aggregation method that employs LLMs to conduct pairwise comparisons locally and efficiently ranks candidate texts globally.
  arXiv  Detail & Related papers  (2024-03-25T17:11:28Z)
• HD-Eval: Aligning Large Language Model Evaluators Through Hierarchical Criteria Decomposition [92.17397504834825]
  HD-Eval is a framework that iteratively aligns large language models evaluators with human preference. HD-Eval inherits the essence from the evaluation mindset of human experts and enhances the alignment of LLM-based evaluators. Extensive experiments on three evaluation domains demonstrate the superiority of HD-Eval in further aligning state-of-the-art evaluators.
  arXiv  Detail & Related papers  (2024-02-24T08:01:32Z)
• PROXYQA: An Alternative Framework for Evaluating Long-Form Text Generation with Large Language Models [72.57329554067195]
  ProxyQA is an innovative framework dedicated to assessing longtext generation. It comprises in-depth human-curated meta-questions spanning various domains, each accompanied by specific proxy-questions with pre-annotated answers. It assesses the generated content's quality through the evaluator's accuracy in addressing the proxy-questions.
  arXiv  Detail & Related papers  (2024-01-26T18:12:25Z)
• MR-GSM8K: A Meta-Reasoning Benchmark for Large Language Model Evaluation [60.65820977963331]
  We introduce a novel evaluation paradigm for Large Language Models (LLMs) This paradigm shifts the emphasis from result-oriented assessments, which often neglect the reasoning process, to a more comprehensive evaluation. By applying this paradigm in the GSM8K dataset, we have developed the MR-GSM8K benchmark.
  arXiv  Detail & Related papers  (2023-12-28T15:49:43Z)
• Post Turing: Mapping the landscape of LLM Evaluation [22.517544562890663]
  This paper traces the historical trajectory of Large Language Models (LLMs) evaluations, from the foundational questions posed by Alan Turing to the modern era of AI research. We emphasize the pressing need for a unified evaluation system, given the broader societal implications of these models. This work serves as a call for the AI community to collaboratively address the challenges of LLM evaluation, ensuring their reliability, fairness, and societal benefit.
  arXiv  Detail & Related papers  (2023-11-03T17:24:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.