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

arXiv: https://arxiv.org/abs/2506.10903 · HTML: https://mlsanity.com/paper/2506.10903/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 31 of its 53 references that are in the map.
- First posted on arXiv 12 Jun 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 30 of 31)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [A Survey on LLM-as-a-Judge](https://mlsanity.com/paper/2411.15594/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [LLMs instead of Human Judges? A Large Scale Empirical Study across 20 NLP Evaluation Tasks](https://mlsanity.com/paper/2406.18403/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Branch-Solve-Merge Improves Large Language Model Evaluation and Generation](https://mlsanity.com/paper/2310.15123/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [J1: Incentivizing Thinking in LLM-as-a-Judge via Reinforcement Learning](https://mlsanity.com/paper/2505.10320/) (2025)
- [Does BLEU Score Work for Code Migration?](https://mlsanity.com/paper/1906.04903/) (2019)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://mlsanity.com/paper/2405.01379/) (2024)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [Assessing Judging Bias in Large Reasoning Models: An Empirical Study](https://mlsanity.com/paper/2504.09946/) (2025)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning](https://mlsanity.com/paper/2505.23754/) (2025)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Crowd Comparative Reasoning: Unlocking Comprehensive Evaluations for LLM-as-a-Judge](https://mlsanity.com/paper/2502.12501/) (2025)
- [Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement](https://mlsanity.com/paper/2402.00745/) (2024)
- [ImProver: Agent-Based Automated Proof Optimization](https://mlsanity.com/paper/2410.04753/) (2024)

## Built on by (most cited first, 6 of 6)

- [Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization](https://mlsanity.com/paper/2606.31002/) (2026)
- [Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance](https://mlsanity.com/paper/2606.14000/) (2026)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [MathAtlas: A Benchmark for Autoformalization in the Wild](https://mlsanity.com/paper/2605.14061/) (2026)
- [Monotonic Reference-Free Refinement for Autoformalization](https://mlsanity.com/paper/2601.23166/) (2026)
- [Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization](https://mlsanity.com/paper/2606.09449/) (2026)

## Abstract (arXiv)

Statement 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 capability of autoformalization, methods for automatically evaluating autoformalization remain underexplored. 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 quality (FQ), and formal validity (FV), 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 more suitable emerging proxy for evaluation than a coarse-grained model. 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.