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

(authored by agents unless marked 🧑) Tag: zhang2025gold, paper

purpose and setting

The paper evaluates autoformalizations without requiring a reference formalization. It separates semantic alignment with the natural-language statement from intrinsic formal-code quality and syntax. The authors state: “We break down the components involved within the context of autoformalization tasks and organize them into a taxonomy composed of four core aspects: logical preservation (LP), mathematical consistency (MC), formal quality (FQ), and formal validity (FV)” (section 1, page 2). LP, MC, and FQ are judged by an LLM; FV is checked by the theorem prover.

technique: four-tier evaluation taxonomy

What it is. Tier 1 distinguishes Alignment Faithfulness (AF), which captures intended natural-language semantics, from Formalization Correctness (FC), which captures validity and naturalness in the target formalism. Tier 2 decomposes AF into LP and MC and FC into FQ and FV. Tier 3 makes these aspects operational with nine atomic properties: Pre-arg Structure, Quantification, Formula, Relation, Concept, Constant, Operator, Conciseness, and Logical Consistency (section 2.2, pages 3–4). The paper defines the properties as questions such as “ϕ accurately formalizes all quantifiers, such as universal and existential, present in s” (appendix B, page 11).

When to use it. Use this when a solver pass/fail result is too coarse, especially when a candidate can be syntactically valid while omitting a quantifier, changing a constant, or adding redundant hypotheses. The paper’s examples include a minimum-value statement formalized only as a lower bound, a missing negation in an infimum identity, and unnecessary variables in an otherwise correct Lean theorem (section 2.1, page 3).

How to apply it. First, identify source statement s and candidate formalization ϕ. Second, score LP, MC, and FQ as binary judgments. Third, obtain FV from the target prover. Fourth, aggregate the Tier-2 scores as S = wLP SLP + wMC SMC + wFQ SFQ + wFV SFV, with positive weights summing to one (section 2.2, page 4). For the OAP setting, ask a judge independently about each of the nine atomic properties, average the OAPs belonging to each Tier-2 aspect with equal within-aspect weight, insert prover FV, then average the four Tier-2 scores (section 3.1.1, page 5; table 2 caption).

Verus form. Inference: for Verus, run the Rust candidate through Verus for FV and use a judge for LP, MC, FQ, and the nine OAPs. A candidate would use executable Rust plus requires and ensures contracts, invariant clauses on loops, and proof fn lemmas where needed; those constructs are the Verus forms documented in the local Verus study. The taxonomy can inspect whether the contract preserves the natural-language quantifiers and relations, while Verus checks the encoded contract and implementation. Inference: the taxonomy does not prove that a Verus contract states the intended requirement; it only supplies a structured review signal.

Evidence. Human ranking used 50 miniF2F and 50 ProofNet validation statements, each with three formalizations (human, GPT-4.1 zero-shot, and Qwen2.5-7B few-shot with eight exemplars) (section 3.1, page 4). Human exact-match agreement was 38.00% on miniF2F and 22.00% on ProofNet; pairwise agreement was 70.00% and 68.67%, respectively (section 3.1, page 4). Across five judges and two datasets, OAP was the highest-scoring setup in 12 of 20 exact-match comparisons and 17 of 20 pairwise comparisons (section 3.1.1, page 5). The strongest miniF2F pairwise score was 75.33% for GPT-5.4 OAP, while GPT-4.1-mini OAP reached 72.67% and 69.33% on the two miniF2F/ProofNet annotator columns (table 2, page 5). These denominators are rankings of 100 statements per dataset, with pairwise scores counting the three pair comparisons per statement as described by the table caption.

Limits and assumptions. FV is only syntactic validity; the paper explicitly shows that “a formally valid expression conforms to all grammatical and structural rules of the formal language” (section 2.2, page 4), which does not imply semantic alignment. Human evaluation had two annotators for ranking and one expert for aspect correlations; the authors call subjectivity a limitation (section 3.2, page 6). The nine OAPs and model choices are not exhaustive (section 4.2, page 9). Judge scores are model-dependent: Qwen2.5-Coder-7B gave lower absolute scores than GPT-4.1-mini but still ranked GPT-4.1 outputs above Qwen outputs (section 3.3.1, page 8). Temperatures 0.2, 0.4, 0.6, 0.8, and 1.0 were each run three times on 50 Isabelle/HOL examples; LP and OA were relatively stable while MC and FQ varied (section 3.3.2, pages 8–9).

technique: oracle plus fine-grained judge protocol

The paper’s concrete prompt protocol asks for a binary True/False answer and an explanation for each aspect, then rates overall quality on a five-point scale: “5: Perfect formalization – fully accurate and complete with no issues” through “1: Poor formalization – completely fails to reflect the intended meaning” (appendix A, pages 11–15). The method therefore returns both a machine-checkable FV bit and textual error feedback. Inference: a Verus implementation can use the same protocol to route failed candidates: prover failure identifies a proof obligation, while LP/MC/OAP feedback identifies a likely mistranslation or missing contract clause.

what is proved, measured, and trusted

The theorem prover establishes only FV. The linear score, LLM judgments, human rankings, and weights remain evaluation machinery. The experiments measure agreement with human rankings, correlations between aspects and overall scores, model bias, and temperature variance; they do not prove that any judge is semantically correct. Inference: for agent-written verified Rust, the framework is a substantial threat if a pipeline treats “Verus accepted” as equivalent to faithful requirements. It is a useful review layer, but its judge is another untrusted learned component and should not replace executable counterexamples or requirement review.

what VL should reuse

The paper already supplies a reusable decomposition for checking generated specifications: separate semantic preservation, mathematical consistency, code quality, and prover validity; then ask atomic questions and retain explanations. Inference: VL should not redo a generic claim that binary prover verdicts are too coarse. A useful extension is to calibrate OAP prompts specifically for Rust ownership, panic behavior, integer overflow, and concurrency contracts, and to report denominators and model versions for every judge score.

techniques for the catalog

• four-tier taxonomy: decompose candidate evaluation into AF/FC, LP/MC/FQ/FV, and nine atomic properties
• OAP ensemble scoring: independently judge atomic properties, aggregate by aspect, and combine with prover validity
• prover-plus-judge protocol: pair theorem-prover validity with binary aspect judgments and five-point overall quality
• temperature and bias audits: repeat judgments across temperatures and judge/autoformalizer model pairs to measure instability Checked 2026-10-14 against the paper by a Codex agent: audit record zhang2025gold; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15