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

Summary

Large language models can now translate natural-language mathematical statements into formal code (autoformalization), but checking whether such translations are actually correct is still difficult. Theorem provers only confirm that the code compiles. Human checking is slow and needs expert knowledge. Reference-based metrics assume flawless gold formalizations, yet benchmarks such as ProofNet contain errors. The authors propose a reference-free evaluator whose taxonomy covers four aspects: LP, which asks whether the logic is preserved; MC, which concerns whether the mathematics stays consistent; FQ, which rates the quality of the formal code; and FV, which assesses its formal validity. LLM judges, all using one backend model, score LP, MC and FQ through atomic properties and explain their verdicts. A theorem prover (Isabelle/HOL or Lean4) checks FV. A weighted linear model then combines the four scores into an overall assessment (OA). The authors tested the framework against human rankings of human-written and model-generated formalizations from miniF2F and ProofNet. This fine-grained "EFG" ensemble agreed with humans better than a single coarse-grained judge. It also let smaller judge models outperform larger ones that used generic criteria. The result points toward scalable, interpretable evaluation for formal mathematics.

Key points

• Taxonomy structure. Tier 1 separates alignment faithfulness from formalization correctness. These split into LP, MC, FQ and FV, and the final score uses positive weights that sum to 1.
• GPT-4.1 results. With 8-shot prompting, GPT-4.1 formalizations scored OA 0.906 (miniF2F Isabelle/HOL), 0.891 (miniF2F Lean4) and 0.836 (ProofNet Lean4). FV was much lower on ProofNet (0.423), so the harder ProofNet statements remain challenging.
• 7B models. Among the 7B autoformalizers, Qwen2.5-7B performed best on miniF2F (OA 0.703). Deepseek-Math-7B led on ProofNet (OA 0.535).
• Judge bias check. Qwen2.5-Coder-7B gave lower absolute scores than GPT-4.1-mini, but both judges still ranked GPT-4.1 above Qwen2.5-7B. The authors found no sign that judges favor outputs from their own model family.
• Sampling stability. The authors ran GPT-4.1-mini three times at each of five temperatures (0.2–1.0) on 50 Isabelle/HOL formalizations. Some individual aspect scores fluctuated, but OA stayed stable. Code and data are published in the GitHub repository lanzhang128/autoformalization_evaluation.