Pith. sign in

REVIEW 3 major objections 5 minor 63 references

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

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A taxonomy-guided ensemble of LLM judges can automatically evaluate autoformalized mathematics more reliably than reference-based metrics.

desk verdict Useful new taxonomy for autoformalization evaluation, but the headline correlations are in-sample because the ensemble weights are fit to the same human ratings used for validation. read the letter →

arxiv 2506.10903 v1 pith:VL4XC7Z2 submitted 2025-06-12 cs.CL

Lan Zhang , Marco Valentino , Andre Freitas This is my paper
classification cs.CL
keywords autoformalizationLLM-as-a-judgeepistemicensembleformalmathematicsIsabelle/HOLLean4evaluationtaxonomyreference-basedmetrics
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that automatically evaluating autoformalization—the translation of natural-language mathematics into Isabelle/HOL or Lean4—can be made reliable without a human expert in the loop. The proposed approach replaces a single coarse LLM judgment with an epistemically and formally grounded (EFG) ensemble: four core criteria (logical preservation, mathematical consistency, formal validity, formal quality) broken into twelve atomic properties, judged separately by LLMs and synthesized into one score. The authors report that GPT-4.1-mini judging these atomic properties and averaging the results correlates with human assessments at 0.662 for Isabelle/HOL and 0.479 for Lean4, clearly surpassing BLEU, ChrF, and RUBY. If this holds, automatic benchmarking of autoformalization systems becomes scalable, interpretable, and much cheaper than expert annotation.

What carries the argument

The engine of the method is the EFG ensemble: a set of LLM judges each scored on twelve Operable Atomic Properties (OAPs) grouped into four core aspects, plus the theorem prover for formal validity, aggregated by a weighted linear model. The OAPs turn abstract criteria into concrete yes/no questions (e.g., 'Does the formal code reflect the predicate-argument structure?' and 'Are types correctly assigned?') designed to be both interpretable and computable, and the weights quantify the relative importance of each aspect for the overall assessment.

What would settle it

Take the same 200 formalizations, have several independent expert annotators rate them with the same criteria, and measure agreement; if inter-annotator agreement (e.g., Cohen's kappa) is low, or if EFG scores correlate no better with a consensus human rating than with the original single annotator, the claimed proxy status fails.

Watch

Extended reading notes

Core claim

The central claim is that fine-grained, taxonomy-guided LLM judgments are a viable proxy for human evaluation of formal mathematical formalizations. Instead of asking a judge for a single overall verdict, the method decomposes quality into logical preservation, mathematical consistency, formal validity, and formal quality; the first three are assessed by LLM judges through twelve Operable Atomic Properties such as quantification, type-match, and conciseness, while formal validity is checked by the theorem prover itself. A linear model with weights $w_{LP}=0.25$, $w_{MC}=0.19$, $w_{FV}=0.32$, $w_{FQ}=0.24$, fitted by constrained quadratic programming on human ratings, combines the four aspects into one score. In their experiments, GPT-4.1-mini with OAPs and weighted averaging yields overall scores correlating with human assessments at 0.662 (Isabelle/HOL) and 0.479 (Lean4), outperforming direct judgment and all reference-based metrics tested, with no evidence of same-model-family bias and stable overall scores under generation randomness.

Load-bearing premise

The entire comparison rests on a single annotator's binary and 5-point ratings of 200 formalizations, selected from statements GPT-4.1 flagged as potentially incorrect, being a valid, unbiased gold standard; if those human ratings are noisy or skewed, every reported correlation and every fitted weight inherits that distortion.

Editorial extensions

If this is right

  • Automatic evaluation of autoformalization can be run at scale without expert annotators for each dataset or domain.
  • Reference-based metrics understate performance and cannot diagnose why a formalization fails, while EFG scores provide aspect-level feedback.
  • Smaller and cheaper LLMs can serve as reliable judges when guided by fine-grained properties, making evaluation cost-effective.
  • LLM judges should not replace theorem provers for syntactic validity; the two complement each other.
  • EFG scores reveal that few-shot prompting mainly boosts formal validity and that 7B open models still lag by more than 10% in overall assessment on complex benchmarks, offering a concrete target for autoformalization research.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural extension, not tested here, is whether the same OAP taxonomy transfers to other proof assistants (Coq, Agda) and to evaluating proofs rather than just statements.
  • Feeding the OAP explanations back to the autoformalization model as fine-grained feedback could improve generated formalizations beyond what a single overall score can guide.
  • The fitted weights come from only 100 human-rated statements; refitting on a larger, multi-annotator set would show whether the weighting is stable or dataset-specific.
  • If LLM judges keep improving with model size, the gap between GPT-4.1-mini OAP weighted-average and human ratings may narrow further, making full automation of evaluation benchmarks feasible while raising a risk of evaluator overfitting to judge preferences.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. This paper proposes EFG, an automatic evaluation framework for autoformalization in Isabelle/HOL and Lean4. It defines a taxonomy with four core aspects—logical preservation, mathematical consistency, formal validity, and formal quality—operationalized through 12 operable atomic properties; uses LLM judges for the first three and a theorem prover for formal validity; and aggregates aspect scores into a linear overall score whose weights are estimated from human ratings. Human evaluation is conducted on 100 statements (200 formalizations) from miniF2F and ProofNet with one annotator. Experiments report correlations of LLM-judge scores with human overall assessments, compare direct versus OAP-based judgment, and compare against BLEU, ChrF, and RUBY, concluding that GPT-4.1-mini with OAP weighted average gives the strongest correlations (0.662 for Isabelle/HOL, 0.479 for Lean4) and that EFG ensembles are a promising proxy for human evaluation.

Significance. The taxonomy and OAP decomposition are thoughtful and potentially useful: they make evaluation interpretable, separate syntactic validity from semantic alignment, and are instantiated with concrete prompts and detailed annotation criteria. The inclusion of theorem-prover checks for formal validity is a sensible design choice, and the authors test across two proof assistants and multiple models. If the empirical claims held out-of-sample, the framework would be a valuable cost-efficient complement to human evaluation. However, the current validation has a central methodological weakness—in-sample weight fitting and model selection on the same human ratings used for evaluation—and relies on a very small, single-annotator gold standard. These issues must be addressed before the headline correlation claims can be accepted.

major comments (3)
  1. [§3.1 / Eq. (2) / Table 4] The headline correlations in Table 4 (0.662 and 0.479) are computed on the same human ratings used to fit the weights in Eq. (2): the weights wLP, wMC, wFV, and wFQ are obtained by minimizing squared error against the normalized human overall-assessment labels on the whole annotated set, and Table 4 reports correlations on the 'whole set of human annotated samples' with no held-out split or cross-validation. In addition, the equal OAP weights in the OAP-WA variant are selected because 'this setting yields the best performance' (§4.1.1) on the same data, which is a second round of model selection on the test set. The direct-judgment and reference-based baselines involve no fitted parameters, so the comparison is not apples-to-apples. Please report cross-validated or held-out correlations with confidence intervals, and either fit the linear weights on a separate development set or compare all methods under the same resampling protocol.
  2. [§3 / Appendix A] The human gold standard consists of a single annotator judging 100 statements (50 Isabelle/HOL, 25+25 Lean4), with no inter-annotator agreement reported. The sample is also conditioned on GPT-4.1 flagging the ground-truth formalization as potentially incorrect, so the evaluation set is not representative of the underlying dataset and any annotator-specific or filter-induced systematic bias propagates into every fitted weight and correlation. The assertion in Appendix A that any human with sufficient knowledge 'should be able to apply these criteria consistently' needs empirical support (e.g., a second annotator on a subset, or at minimum a detailed adjudication protocol). Without it, the reported correlation magnitudes cannot be interpreted as measuring agreement with a stable gold standard.
  3. [§4.2 / §4.3 / Figure 3] The claim that EFG ensembles 'significantly surpass' BLEU, ChrF, and RUBY is not backed by significance tests or confidence intervals: Figure 3 reports point correlations on the ZS subset of the human-annotated samples, which is small, and no p-values or bootstrap intervals are given. Similarly, §4.3 concludes 'no evidence of cross-model family bias' from comparing only two judge models (GPT-4.1-Mini and Qwen2.5-Coder-7B) on one test set; this is at most a preliminary observation. Please add uncertainty quantification for the correlation comparisons and either broaden the bias analysis or soften the claim.
minor comments (5)
  1. [§4.1] There is a typo in 'temprature=0.2'; it should be 'temperature=0.2'.
  2. [Table 10 caption] The caption contains a typo: 'Percentge' should be 'Percentage'.
  3. [§3.1 / Eq. (2)] The normalization of the 5-point human ratings to [0,1] is not specified; please state the formula (e.g., (rating-1)/4) and clarify whether the weights in Eq. (2) are fitted separately for each formal language or pooled across languages.
  4. [§3.1 / Table 4] Section 3.1 reports a correlation coefficient Coef = 0.785 for the fitted linear model, but Table 4 reports OAP-WA correlations of 0.662 and 0.479; the discrepancy should be explained, since the former is based on human-scored core properties while the latter uses LLM judgments.
  5. [§4.2] For reproducibility of the BLEU, ChrF, and RUBY baselines, please specify the tokenization, n-gram order, smoothing, and any language-specific preprocessing used.

Circularity Check

2 steps flagged · score 6.0 of 10

Headline correlations are in-sample: the Eq. (2) weights are fit to the same human OA labels that Table 4 correlates with, so the 0.662/0.479 EFG advantage is partly a fitted value, not an out-of-sample prediction.

  1. fitted input called prediction [Section 3.1, Eq. (2); Section 4.1.1 and Table 4 caption]
    "To estimate the optimal component weights, we construct a feature matrix X using binary justifications of the core properties, and normalize the 5-point human assessment ratings to the range [0, 1], forming the target vector y. The optimal weights w are then obtained by solving ... min ∥Xw − y∥2 subject to wi ≥ 0, Σ wi = 1 (2). ... [Table 4 caption] Results are calculated on whole set of human annotated samples."

    The target vector y in Eq. (2) is the normalized 5-point human overall-assessment ratings from the annotated sample. Table 4 then computes correlations with human assessments 'on whole set of human annotated samples'—the same labels used to fit y. The linear weights in Eq. (1) are therefore least-squares calibrated to the very human ratings that the reported correlations treat as ground truth. The direct-judge baselines and BLEU/ChrF/RUBY involve no such fitted parameters, so the comparison is not apples-to-apples; the headline 0.662/0.479 figures are partly an in-sample fit statistic rather than a demonstrated out-of-sample prediction.

  2. other [Section 4.1.1 (Table 4 and surrounding text)]
    "One possible approach is to assign equal weights to all relevant OAPs for each core property. This setting yields the best performance across both formal languages, achieving positive correlations of 0.662 and 0.479 with human assessments for Isabelle/HOL and Lean4, respectively."

    The synthesis choice (OAP-And vs. OAP-W A) is selected by comparing correlations on the same human-annotated samples that are then reported in Table 4. The reported 0.662/0.479 values are therefore selected maxima over configurations evaluated against the target labels, not independent confirmations of a pre-specified design. This adds a second in-sample selection layer on top of the Eq. (2) weight fitting, further inflating the apparent advantage of the EFG ensemble over unfitted baselines.

full rationale

The central empirical claim is that GPT-4.1-mini OAP-W A scores correlate with human assessments at 0.662 (Isabelle/HOL) and 0.479 (Lean4), outperforming direct judgment and reference-based metrics. The derivation chain is: (i) collect human binary aspect judgments and human OA ratings y on the annotated sample; (ii) fit the four linear weights in Eq. (1) by minimizing squared error against y (Eq. 2); (iii) use those weights with LLM OAP judgments and theorem-prover validity to compute SOA; (iv) report the correlation of SOA with y on the 'whole set of human annotated samples' in Table 4. Because the weights are calibrated to the same y that Table 4 correlates with, the reported correlations are in-sample with respect to the fitted linear model. The LLM OAP judgments themselves are not fitted, so the framework retains independent content and the circularity is partial rather than total; a held-out split or nested validation would materially repair the evaluation. The additional selection of OAP-W A because 'this setting yields the best performance' on the same data compounds the optimism. Other concerns—single annotator, GPT-4.1-filtered statement selection, small sample, subjective ratings—are gold-standard validity issues rather than circularity, and are partly acknowledged in the Limitations section. I found no load-bearing self-citation chain or imported uniqueness theorem; self-citations such as [12] and [13] support background claims only. The score of 6 reflects one or more predictions that are partly fitted values while the underlying LLM judgments are not.

Assumptions & free parameters 2 free parameters · 4 assumptions · 0 invented entities

No new physical or mathematical entities are introduced; the taxonomy and OAPs are evaluation constructs, not entities with falsifiable handles. The ledger is dominated by modeling choices and the human-rating gold standard, plus the fitted linear weights that drive the reported correlations.

free parameters (2)
  • Component weights wLP, wMC, wFV, wFQ = 0.25, 0.19, 0.32, 0.24
    Solved via constrained quadratic program (Eq. 2) against human overall-assessment ratings on the same 100-statement sample later used for validation; makes reported correlations partly in-sample.
  • OAP aggregation weights for core aspects (OAP-WA) = equal weights across relevant OAPs
    Chosen by hand in Sec. 4.1.1; the best-performing synthesis setting uses equal OAP weights, a free modeling choice not derived from data.
assumptions (4)
  • domain assumption Human annotation of LP, MC, FQ, and OA is a reliable ground truth.
    Single annotator, no inter-annotator reliability; Appendix A asserts consistency should be achievable by any expert. All correlations are anchored to these labels.
  • ad hoc to paper GPT-4.1's pre-filter for 'potentially incorrect' ground-truth formalizations does not bias the human sample.
    Section 3 selects only statements where GPT-4.1 estimated the ground truth as potentially incorrect, skewing LP and MC distributions and potentially favoring the same model family used as judge.
  • domain assumption A nonnegative linear combination of the four aspect scores with weights summing to 1 adequately represents overall formalization quality.
    Adopted in Eq. 1 without an alternative functional form; the linearity is not tested against nonlinear aggregations.
  • ad hoc to paper LLM binary judgments on atomic properties can be synthesized by logical AND or equal-weighted average into core-aspect scores.
    Section 4.1 defines AND synthesis and weighted average; this is an untested modeling choice.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning." pith.science (2026). https://pith.science/paper/VL4XC7Z2

@misc{pith2026250610903,
  author       = {Pith},
  title        = {Pith review of: Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VL4XC7Z2}},
  note         = {Machine review of arXiv:2506.10903}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2506.10903 by the authors.

Figure 1
Figure 1. Overview of the proposed framework for evaluating autoformalization. Our method [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Correlation coeffi￾cients between aspects based on human evaluation. lower average formal validity (not exceeding 20%) and generally lower overall ratings in the latter. Furthermore, we report the correlation coefficients from human eval￾uations across various formalization aspects in [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Correlation coefficients between met￾rics calculated on the ZS subset of human an￾notated samples. (OATP): GPT-4.1 OA-TP; (GD): GPT-4.1 Direct; (MD): GPT-4.1-Mini Di￾rect; (MOA): GPT-4.1-Mini OAP-And; (MOW): GPT-4.1-Mini OAP-WA. 4.2.1 Results & Discussion All LLM-as-judges approaches show higher correlations (above 0.5) with human assessments than the reference-based metrics (below 0.25). This is expected, as there … view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Error bars of GPT-4.1-mini OAP-WA with different temperature across multiple runs. guages, indicating a degree of robustness in the indicative power of our evaluation approach. The score differences between the two judges are more pronounced on Lean4 than on Isabelle/H…
Figure 5
Figure 5. Figure 5: Cohen’s kappa between judgment from different sources. ( [PITH_FULL_IMAGE:figures/full_fig_p017_5.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

63 extracted references · 34 canonical work pages

  1. [1]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023. URL https://openreview.net/forum?id=SMa9EAovKMC

    2023

  2. [2]

    Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F

    Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. In The Thirteenth Internat...

    work page 2025

  3. [3]

    Goedel-prover: A frontier model for open-source automated theorem proving, 2025

    Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover: A frontier model for open-source automated theorem proving, 2025. URL https://arxiv.org/abs/2502.07640

    arXiv 2025

  4. [4]

    Improver: Agent-based auto- mated proof optimization

    Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, and Sean Welleck. Improver: Agent-based auto- mated proof optimization. In The Thirteenth International Conference on Learning Representa- tions, 2025. URL https://openreview.net/forum?id=dWsdJAXjQD

    work page 2025

  5. [5]

    Learning formal mathematics from intrinsic motivation

    Gabriel Poesia, David Broman, Nick Haber, and Noah Goodman. Learning formal mathematics from intrinsic motivation. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024. URL https://openreview.net/forum?id=uNKlTQ8mBD

    work page 2024

  6. [6]

    Formalmath: Benchmarking formal mathematical reasoning of large language models, 2025

    Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, and Weiyang Liu. Formalmath: Benchmarking formal mathematical reasoning of large language models, 2025. URL https://arxiv.org/abs/2505.02735

    arXiv 2025

  7. [7]

    Formal mathematical reasoning: A new frontier in ai, 2024

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai, 2024. URL https: //arxiv.org/abs/2412.16075

    arXiv 2024

  8. [8]

    Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning

    Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806–3824, Singapore, December 2023. Association for Computational 11...

    doi:10.18653/v1/2023.findings-emnlp.248 2023

Show all 63 references
  1. [9]

    Faithful and robust llm-driven theorem proving for nli explanations

    Xin Quan, Marco Valentino, Louise A Dennis, and André Freitas. Faithful and robust llm-driven theorem proving for nli explanations. arXiv preprint arXiv:2505.24264, 2025

    2025 arXiv

  2. [10]

    Dennis, and Andre Freitas

    Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. Verification and refinement of natural language explanations through LLM-symbolic theorem proving. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors, Proceedings of the 2024 Conference on Empirical Met...

    2024

  3. [11]

    Autoformalization with large language models

    Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances in Neural Informa- tion P...

    2022

  4. [12]

    Consistent autoformalization for constructing mathematical libraries

    Lan Zhang, Xin Quan, and Andre Freitas. Consistent autoformalization for constructing mathematical libraries. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors, Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 4020–4033,...

    2024

  5. [13]

    Formalizing complex mathematical statements with llms: A study on mathematical definitions, 2025

    Lan Zhang, Marco Valentino, and Andre Freitas. Formalizing complex mathematical statements with llms: A study on mathematical definitions, 2025. URL https://arxiv.org/abs/2502. 12065

    2025

  6. [14]

    Lawrence C. Paulson. Isabelle: The next 700 theorem provers, 2000

    2000

  7. [15]

    The lean theorem prover (system description)

    Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, edi- tors, Automated Deduction - CADE-25, pages 378–388, Cham, 2015. Springer International Publishing

    2015

  8. [16]

    Gonzalez, and Ion Stoica

    Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. Judging LLM-as-a-judge with MT-bench and chatbot arena. In Thirty-seventh Conference on Neural Infor...

    2023

  9. [17]

    minif2f: a cross-system benchmark for formal olympiad-level mathematics

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations,

  10. [18]

    Ayers, Dragomir Radev, and Jeremy Avigad

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics, 2023

    2023

  11. [19]

    Bleu: a method for automatic evaluation of machine translation

    Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Pierre Isabelle, Eugene Charniak, and Dekang Lin, editors, Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics , ...

    2002

  12. [20]

    chrF: character n-gram F-score for automatic MT evaluation

    Maja Popovi´c. chrF: character n-gram F-score for automatic MT evaluation. In Ond ˇrej Bojar, Rajan Chatterjee, Christian Federmann, Barry Haddow, Chris Hokamp, Matthias Huck, Varvara Logacheva, and Pavel Pecina, editors,Proceedings of the Tenth Workshop on Statistical Machine...

    2015 doi

  13. [21]

    Ngoc Tran, Hieu Tran, Son Nguyen, Hoan Nguyen, and Tien N. Nguyen. Does bleu score work for code migration? In Proceedings of the 27th International Conference on Program Comprehension, ICPC ’19, page 165–176. IEEE Press, 2019. doi: 10.1109/ICPC.2019.00034. URL https://doi.org...

    2019

  14. [22]

    Gpt-4 technical report, 2024

    OpenAI. Gpt-4 technical report, 2024. URL https://arxiv.org/abs/2303.08774

    2024 arXiv

  15. [23]

    Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas ...

    2023

  16. [24]

    Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y . K. Li, Y . Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models, 2024. URL https://arxiv.org/abs/ 2402.03300

    2024 arXiv

  17. [25]

    Qwen2.5 technical report, 2025

    Qwen Team. Qwen2.5 technical report, 2025. URL https://arxiv.org/abs/2412.15115

    2025 arXiv

  18. [26]

    Enhancing ethical explanations of large language models through iterative symbolic refinement

    Xin Quan, Marco Valentino, Louise Dennis, and Andre Freitas. Enhancing ethical explanations of large language models through iterative symbolic refinement. In Yvette Graham and Matthew Purver, editors, Proceedings of the 18th Conference of the European Chapter of the Associati...

  19. [27]

    Jiang, Daniel Raggi, Wenda Li, and Mateja Jamnik

    Guillem Tarrach, Albert Q. Jiang, Daniel Raggi, Wenda Li, and Mateja Jamnik. More details, please: Improving autoformalization with more detailed proofs. In AI for Math Workshop @ ICML 2024, 2024. URL https://openreview.net/forum?id=AkJvzpYMvK

    2024

  20. [28]

    Towards autoformalization of mathe- matics and code correctness: Experiments with elementary proofs

    Garett Cunningham, Razvan Bunescu, and David Juedes. Towards autoformalization of mathe- matics and code correctness: Experiments with elementary proofs. In Deborah Ferreira, Marco Valentino, Andre Freitas, Sean Welleck, and Moritz Schubotz, editors,Proceedings of the 1st Work...

    2022 doi

  21. [29]

    URL https://aclanthology.org/2024

    Association for Computational Linguistics. URL https://aclanthology.org/2024. eacl-long.1/

    2024

  22. [30]

    Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach

    Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations , 2025. URL https: //openrevie...

    2025

  23. [31]

    Process-driven autoformalization in lean 4, 2024

    Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. Process-driven autoformalization in lean 4, 2024. URL https://arxiv.org/abs/2406. 01940

    2024

  24. [32]

    Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

    Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with retrieval- augmented language models, 2023. URL https://arxiv.org/abs/2306.15626

    2023 arXiv

  25. [33]

    Jiang, Wenda Li, and Mateja Jamnik

    Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multi-language diversity benefits autoformaliza- tion. In A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Paquet, J. Tomczak, and C. Zhang, editors, Advances in Neural Information Processing Systems, volume 37, pages 83600–83626. ...

    2024

  26. [34]

    Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data,

    Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data,

  27. [35]

    Autoformalize mathematical statements by symbolic equivalence and semantic consistency

    Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024. URL https://openrev...

    2024

  28. [36]

    Formalalign: Automated alignment evaluation for autoformalization, 2024

    Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, and Zhijiang Guo. Formalalign: Automated alignment evaluation for autoformalization, 2024. URL https: //arxiv.org/abs/2410.10135

    2024 arXiv

  29. [37]

    Branch-solve-merge improves large language model evaluation and generation

    Swarnadeep Saha, Omer Levy, Asli Celikyilmaz, Mohit Bansal, Jason Weston, and Xian Li. Branch-solve-merge improves large language model evaluation and generation. In Kevin Duh, Helena Gomez, and Steven Bethard, editors, Proceedings of the 2024 Conference of the North American ...

    2024 doi

  30. [38]

    Self-taught evaluators, 2024

    Tianlu Wang, Ilia Kulikov, Olga Golovneva, Ping Yu, Weizhe Yuan, Jane Dwivedi-Yu, Richard Yuanzhe Pang, Maryam Fazel-Zarandi, Jason Weston, and Xian Li. Self-taught evaluators, 2024. URL https://arxiv.org/abs/2408.02666

    2024 arXiv

  31. [39]

    Improving autoformaliza- tion using type checking, 2025

    Auguste Poiroux, Gail Weiss, Viktor Kunˇcak, and Antoine Bosselut. Improving autoformaliza- tion using type checking, 2025. URL https://arxiv.org/abs/2406.07222

    2025

  32. [40]

    J1: Incentivizing thinking in llm-as-a-judge via reinforcement learning, 2025

    Chenxi Whitehouse, Tianlu Wang, Ping Yu, Xian Li, Jason Weston, Ilia Kulikov, and Swar- nadeep Saha. J1: Incentivizing thinking in llm-as-a-judge via reinforcement learning, 2025. URL https://arxiv.org/abs/2505.10320

    2025

  33. [41]

    Anna Bavaresco, Raffaella Bernardi, Leonardo Bertolazzi, Desmond Elliott, Raquel Fernández, Albert Gatt, Esam Ghaleb, Mario Giulianelli, Michael Hanna, Alexander Koller, André F. T. Martins, Philipp Mondorf, Vera Neplenbroek, Sandro Pezzelle, Barbara Plank, David Schlangen, Al...

    2024 arXiv

  34. [42]

    A survey on llm-as-a-judge, 2025

    Jiawei Gu, Xuhui Jiang, Zhichao Shi, Hexiang Tan, Xuehao Zhai, Chengjin Xu, Wei Li, Yinghan Shen, Shengjie Ma, Honghao Liu, Saizhuo Wang, Kun Zhang, Yuanzhuo Wang, Wen Gao, Lionel Ni, and Jian Guo. A survey on llm-as-a-judge, 2025. URL https://arxiv.org/abs/ 2411.15594

    2025 arXiv

  35. [43]

    Crowd comparative reasoning: Unlocking comprehensive evaluations for llm-as-a-judge, 2025

    Qiyuan Zhang, Yufei Wang, Yuxin Jiang, Liangyou Li, Chuhan Wu, Yasheng Wang, Xin Jiang, Lifeng Shang, Ruiming Tang, Fuyuan Lyu, and Chen Ma. Crowd comparative reasoning: Unlocking comprehensive evaluations for llm-as-a-judge, 2025. URL https://arxiv.org/ abs/2502.12501

    2025 arXiv

  36. [44]

    Deeptheorem: Advancing llm reasoning for theorem proving through natural language and reinforcement learning, 2025

    Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, Zhenwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, and Dong Yu. Deeptheorem: Advancing llm reasoning for theorem proving through natural language and reinforcement learning, 2025....

    2025 arXiv

  37. [47]

    Assessing judging bias in large reasoning models: An empirical study,

    Qian Wang, Zhanzhi Lou, Zhenheng Tang, Nuo Chen, Xuandong Zhao, Wenxuan Zhang, Dawn Song, and Bingsheng He. Assessing judging bias in large reasoning models: An empirical study,

  38. [48]

    URL https://arxiv.org/abs/2504.09946

    arXiv

  39. [50]

    Pre-arg Structure: ϕ reflects the inherent predicate-argument structure of the statement s

  40. [51]

    Quantification: ϕ accurately formalizes all quantifiers, such as universal and existential, present in s

  41. [52]

    Formula: All mathematical formulas and expressions in s, such as equations and inequali- ties, are correctly and completely represented in ϕ

  42. [53]

    Relation: The logical and mathematical relationships between propositions in s are pre- served in ϕ

  43. [54]

    Concept: All mathematical concepts mentioned in s, such as integers, fractions, real or complex numbers, derivatives, integrals, vectors, matrices, probabilities, expectations, and variances, are correctly formalized in ϕ

  44. [55]

    Constant: All mathematical constants mentioned in s, such as 1, 2 3, π, e, are properly included in ϕ

  45. [56]

    Operator: All mathematical operators used in s, such as addition, subtraction, multi- plication, division, summation, exponentiation, and product, are correctly represented in ϕ

  46. [57]

    Syntax Validity: ϕ contains no syntax or structural errors within the target formal language

  47. [58]

    Referential Completeness: All symbols and terms used in ϕ are properly defined or imported, ensuing that nothing is left undefined or unreferenced

  48. [59]

    Type-Match: The types of variables and expressions in ϕ are correctly and consistently assigned, in accordance with the rules of modern type-theoretic systems such as Isabelle or Lean

  49. [60]

    Conciseness: ϕ is expressed in a minimal, non-redundant form, avoiding unnecessary repetition or complexity

  50. [61]

    15 Purpose Content Basic You are an expert in formal language {formal_language}

    Logical Consistency: ϕ is internally coherent and contains no contradictions under the logical rules of the formal system. 15 Purpose Content Basic You are an expert in formal language {formal_language}. You will be given a mathematical statement written in natural language an...

  51. [62]

    True" or

    the judgement of whether the formal code satisfies this aspect. This should be a binary value in "True" or "False"

  52. [63]

    real ⇒ real

    the detailed explanation of your judgement. You should wrap your final results in a way illustrated as the following: %%%%%%%%%% Explanation: Your Detailed Explanation Judgement: Your Binary Judgement %%%%%%%%%% Strictly follow the instructions that have been claimed. Overall ...

  53. [2022]

    URL https://openreview.net/forum?id=9ZPegFuFTFv

  54. [2024]

    doi: 10.18653/v1/2024.emnlp-main.172

    Association for Computational Linguistics. doi: 10.18653/v1/2024.emnlp-main.172. URL https://aclanthology.org/2024.emnlp-main.172/

    2024 doi

  55. [2025]

    URL https://arxiv.org/abs/2502.05567

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.