Pith. sign in

REVIEW 4 major objections 5 minor 51 references

Psychometric-Based Evaluation for Theorem Proving with Large Language Models

T0 review · 4 major / 5 minor · reviewed 2026-08-09 · deepseek-v4-flash

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

Pith's one-line read A psychometric adaptive-testing pipeline assigns miniF2F theorems difficulty and discrimination weights, produces ability scores that separate ten LLMs more finely than Pass@128, and cuts evaluation cost by 76%.

desk verdict A useful first pass at IRT-based adaptive testing for theorem-proving LLMs, with a released graded dataset and real out-of-sample evidence, but the validity claims outrun the evidence—worth a serious referee, not a desk reject. read the letter →

arxiv 2502.00855 v1 pith:EFBFVPDI submitted 2025-02-02 cs.AI

Jianyu Zhang , Yongwang Zhao , Long Zhang , Jilin Hu , Xiaokun Luan , Zhiwei Xu , Feng Yang This is my paper · ORCID
classification cs.AI
keywords theoremprovinglargelanguagemodelsitemresponsetheoryadaptiveevaluationminiF2F-GradeddifficultyanddiscriminationLean4passrate
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

Formal-theorem-proving LLMs are currently ranked by Pass@N on fixed datasets, which treats every theorem as equally important and hides real differences between models. This paper proposes replacing that practice with a psychometric adaptive test: each theorem in miniF2F is annotated with difficulty and discrimination from the proof attempts of four LLMs, and an item-response-theory update rule converts a model's successes and failures on a small, dynamically chosen subset of theorems into a single ability score. The authors claim these ability scores rank LLMs consistently with Pass@16/32/64 while revealing larger gaps than Pass@128, and that the procedure needs only 23% of the 488 theorems, an average 76.13% reduction in evaluation cost. A reader should care because it offers a cost-efficient, difficulty-aware way to tell which theorem-proving models are actually better, rather than which ones happened to get lucky within 128 attempts.

What carries the argument

The load-bearing mechanism is a two-parameter logistic item response theory model, $P(t_i,\theta)=\frac{1}{1+e^{-a_i(\theta-b_i)}}$, in which each theorem $t_i$ has a difficulty $b_i$ and discrimination $a_i$ estimated from four annotation models' 128-attempt pass rates. Around that model sits a Fisher-information selection rule $I(t_i,\theta)=a_i^f P(t_i,\theta)(1-P(t_i,\theta))$ with $f=0.49$ that chooses the five most informative theorems each round, and an update rule $\theta \leftarrow \theta + \eta a_i(r_i - P(t_i,\theta))$ with $\eta=0.004$ that moves the scalar ability estimate toward the model's observed success rate. The machinery converts an expensive full-dataset pass-rate sweep into a targeted, converging adaptive test.

What would settle it

Re-annotate miniF2F with a different set of, say, five open-source theorem-proving LLMs that span the same ability range, then run the adaptive evaluation on the same ten evaluation models; if any pair of models reverses order in ability score relative to the published ranking (for instance Qwen2.5-Coder-7B versus DeepSeek-Prover-V1.5-Base), the claim that the scores accurately reflect proof ability would fail. Alternatively, split miniF2F's 488 theorems by category, estimate ability on algebra and number-theory subsets separately, and check whether the scalar scores predict performance on the held-out half; strong divergence would indicate that single-ability is insufficient.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that theorem-proving ability can be measured like a latent trait in psychometrics, and that doing so exposes performance differences that Pass@128 misses. The method computes a difficulty value for each theorem from the average attempt success rate with a correction for which low-ability models succeeded, and a discrimination value from pairwise slopes of success rate vs ability across four annotation LLMs (Eqs. 1–3). It then selects the five most informative theorems per round using a Fisher-information score, tests the candidate model on them 128 times, and updates the ability estimate by $\theta \leftarrow \theta + \eta a_i(r_i - P(t_i,\theta))$ under the two-parameter logistic item response model until the estimate changes by less than 0.01 for ten consecutive rounds. The resulting ability scores align with Pass@16/32/64 rankings, separate DeepSeek-Prover-V1.5-RL from its SFT version by more than the 0.41% Pass@128 gap, and are claimed to accurately reflect the proof abilities of LLMs.

Load-bearing premise

The load-bearing premise is that the difficulty and discrimination numbers, computed from just four annotation models' 128-attempt pass rates, are stable properties of each theorem, and that a model's overall proving ability can be captured by a single scalar on the same scale.

Editorial extensions

If this is right

  • Ability scores give a single-number ranking that is more informative than Pass@128: for example, RL fine-tuning over SFT shows only a 0.41% Pass@128 difference but a 0.0239 ability-score gap.
  • Rankings from ability scores agree with Pass@16, Pass@32, and Pass@64 for the ten models tested, with only one inversion relative to Pass@128, and the paper argues that inversion is explained by higher-difficulty performance and attempt success rate.
  • Evaluating on 23% of miniF2F cuts average proof-generation cost by 76.13% while still separating models, making repeated evaluation of large models much cheaper.
  • The miniF2F-Graded difficulty labels are more aligned with LLM-perceived difficulty than the original human five-level MATH grading; every tested model's pass rate decreases monotonically from Level 1 to Level 4.
  • The method's item-parameter estimates and grading can be updated as SOTA models improve, so the benchmark can keep distinguishing models even as the easiest theorems saturate.

Reading between the lines

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

  • If theorem difficulty and discrimination are treated as stable item properties, the same adaptive-testing design could be ported to other formal-verification or code-generation benchmarks; the reported 76% savings would need to be re-validated on each new dataset because it depends on how concentrated information is among items.
  • The paper's own category statistics suggest ability may be multidimensional (IMO difficulty 0.978 vs MATH 0.646; number-theory discrimination 0.584 vs others 0.192), so a natural extension is to replace the single scalar $\theta$ with per-topic ability scores and test whether rankings change; the current method cannot distinguish 'good at algebra' from 'good at number theory'.
  • A testable refinement would be to let the adaptive procedure also choose the number of attempts per theorem rather than fixing 128, or to stop earlier using attempt-success data; this could cut cost further, but its validity against full-dataset scores is not established by this paper.
  • Because the annotation models and evaluation models overlap in the DeepSeek-Prover family, an external check would be to re-annotate miniF2F with an independent, newly released set of theorem-proving LLMs and confirm that the resulting ability-score leaderboard is unchanged.
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

4 major / 5 minor

Summary. The paper proposes a psychometric-based adaptive evaluation method for LLM theorem provers, consisting of a dataset annotation stage (miniF2F-Graded, with difficulty and discrimination metrics computed from four annotation LLMs) and an adaptive testing stage that selects the most informative theorems per model and updates a scalar ability score θ. The authors report that the method yields rankings largely consistent with Pass@16/32/64, highlights finer performance differences than Pass@128 (e.g., between DeepSeek-Prover-V1.5-RL and -SFT), and reduces the number of theorems needed by 76.13% on average. The dataset and code are released.

Significance. If the proposed ability scores are valid, the paper would make a useful contribution: it introduces a new evaluation axis for theorem-proving LLMs, provides a public difficulty/discrimination annotation of miniF2F, and demonstrates a large cost reduction while preserving (and possibly sharpening) model rankings. The out-of-sample Evaluation LLMs (disjoint from the Annotation LLMs) and the monotone decrease in Pass@128 across difficulty levels in Table 3 for those models are concrete positive evidence. The work also connects psychometrics with LLM evaluation in a domain where pass rates are the dominant but crude metric. However, the central validity claim rests on item parameters estimated from only four models; the paper itself documents a model-specific anomaly, and the tuning of the update rule is not fully disclosed. The significance is therefore conditional on additional robustness evidence.

major comments (4)
  1. [§3.1.2, Eq. (1)–(3), §4.2, E.2] The stability of the item parameters (difficulty and discrimination) is load-bearing for the entire adaptive pipeline, but the paper provides no uncertainty quantification. These parameters are computed from exactly four annotation LLMs, and Eq. (3) averages pairwise slopes (Pi−Pj)/(θi−θj). With ability differences as small as 0.123 vs. 0.178 (Table 1) and binomial noise in pass rates (SE ≈ 0.044 at p=0.5 with 128 attempts), the discrimination estimates are noisy. The paper itself reports in §4.2 and E.2 that 'some theorems in mathd_numbertheory exhibit high discrimination at lower difficulty levels due to one model's exceptional performance in this category,' which is direct evidence of model-specificity. I recommend a leave-one-annotation-model-out re-estimation (and, if feasible, bootstrap confidence intervals for difficulty and discrimination) to show that the item parameters and the resulting ability scores are not driven by a single model. Without this, the information-based selection (Eq. 4) and the update rule in Algorithm 1 may inherit the instability.
  2. [§3.2.2, Algorithm 1, §4.1] The hyperparameters [f, η] = [0.49, 0.004] are said to be selected through 'tuning experiments,' but the tuning protocol is not described: which models were used for tuning, what objective function was optimized, and whether the six Evaluation LLMs were excluded during tuning. If the same models whose rankings are later reported in Figure 3 were used to select f and η, then the ranking agreement and cost reduction are partly in-sample. Please specify the tuning procedure, the search space, and the criterion, and ideally confirm that the reported results hold for a held-out set of models.
  3. [§5.2, F.2] The main claim that 'ability scores accurately reflect the proof abilities of LLMs' is supported only by agreement of rankings with Pass@16/32/64 (Figure 3). This is not a strong validity check, because the ability score is itself a nonlinear transformation of the same 128-attempt data used to compute those pass rates; some agreement is expected by construction. The discussion in F.2 attempts to justify the Qwen2.5-Coder vs. DeepSeek-Prover-V1.5-Base reversal using Level 3 pass rates from Table 3, but those level assignments come from the same difficulty metric being validated, making the argument circular. The paper should define an external validity criterion (e.g., performance on a separate, harder suite, or training/FLOPS evidence) and test whether the ability score better predicts that criterion than Pass@128 does. Without such a criterion, the stronger claim of 'better reveal the performance disparities' is not established.
  4. [§5.1, Table 3] The validation of the difficulty grading in Table 3 includes the four Annotation LLMs, whose pass rates were used to define the difficulty levels in the first place. The monotone decrease across Levels 1–4 for those models is partly by construction; the genuinely informative evidence is the same monotonicity for the six disjoint Evaluation LLMs. The text says the decrease holds 'without exception' without separating the in-sample annotation models from the out-of-sample evaluation models. Please present the out-of-sample monotonicity separately, or at least note which rows are in-sample, so readers can assess the strength of the validation.
minor comments (5)
  1. [Abstract and Table 1] The abstract states the method 'uses only 23% of the theorems,' but Table 1 reports evaluation costs ranging from 55 to 195 theorems (11% to 40% of 488). Please clarify whether 23% is an average or a representative value, and report the variance.
  2. [§3.1.2 and Eq. (5)] The notation P(x) for the average success rate is easily confused with the IRT probability P(t_i, θ) in Eq. (5) and Algorithm 1. Using distinct symbols (e.g., p̄(x) and Pr(x | θ)) would improve readability.
  3. [Algorithm 1] The transformation 'ri ← log(ri + 1)' is applied to success rates in (0, 0.1) but not to the model prediction P(t_i, θ); the base of the logarithm is unspecified. The asymmetry and the choice of the 0.1 threshold are not justified.
  4. [Introduction, first paragraph] The phrase 'a 7B-metric model' should be 'a 7B-parameter model.'
  5. [Related Work] Given that [24] already proposes adaptive testing for LLM cognitive ability, the paper should explicitly contrast its method with [24] in terms of the item model, the update rule, and the specific challenges of theorem proving (e.g., formal verification, limited number of suitable models).

Circularity Check

1 steps flagged · score 4.0 of 10

Ability-score validation is partly in-sample: the four annotation models that calibrate difficulty/discrimination are themselves scored and used to certify ranking agreement; hyperparameter tuning is undisclosed.

  1. fitted input called prediction [Section 3.1.2 (Eqs. 1-3), Section 4.1, Section 4.2 / Table 1]
    "We use the pass rate across the entire dataset ( P ass@128) to represent the prior ability values of the models. The models used for annotation are denoted as M1, M2, M3, M4 ... we evaluated six Evaluation LLMs and four Annotation LLMs. ... While the Ability Score and P ass@128 are measured in different units and have numerical differences, their rankings are largely the same."

    The difficulty and discrimination of every theorem are computed from the same four Annotation LLMs (codegeex4, llemma, TheoremLlama, DeepSeek-Prover-V1.5-RL) via Eqs. (1)-(3), using their per-theorem pass rates P_Mi(x) and their Pass@128 as prior ability θ(Mi). Table 1 then reports ability scores for these exact four models, and Section 5.2 uses the resulting ranking agreement with Pass@16-128 as evidence that 'the ability scores obtained through this evaluation method accurately reflect the proof abilities of LLMs.' For the annotation subset, the adaptive score is a re-expression of the data that fixed the item parameters: the update rule θ ← θ + η·ai·(ri − P(θ)) consumes ri from the same model whose P_Mi defined ai and bi.

full rationale

The derivation chain is not globally circular. Item parameters are computed once from four annotation models and then applied to six external Evaluation LLMs, so the adaptive scores for the external models are genuine out-of-sample measurements. The difficulty grading of miniF2F-Graded is also validated on models outside the annotation set, giving the central method independent content. However, the paper weakens this by also scoring the four annotation models with item parameters derived from those same models and by citing the resulting ranking agreement as validity evidence; for that subset the agreement is essentially a monotone transform of the calibration data. Additionally, the hyperparameters [f, η] = [0.49, 0.004] are selected through 'tuning experiments' without disclosing the objective, so the reported agreement could be partly a tuned artifact; this is a methodological opacity rather than a demonstrated circular step. The paper's own observation of unstable discrimination for number-theory theorems (one model's exceptional performance) further undermines parameter stability, but that is a correctness risk, not a definitional circularity. Overall, the central claim still has independent support from the external models, but the in-sample validation and undisclosed tuning justify a moderate circularity score rather than a clean one.

Assumptions & free parameters 4 free parameters · 5 assumptions · 1 invented entities

The central claim rests on item parameters computed from four LLMs' noisy 128-attempt pass rates (Eq. 1-3), a 2PL response model assumed without fit checks (Eq. 5), a unidimensional ability scale that the paper's own category analysis (Table 4, E.2) contradicts, and hand-tuned hyperparameters. The load-bearing free parameters are ε (correction weight), f (information exponent), η (update step), and the undisclosed clamping bounds θmin/θmax. The invented 'ability score' latent trait has no external validation. No new physical or mathematical entities are introduced.

free parameters (4)
  • ε (correction weight) = 0.005
    Eq. 1; hand-chosen weight for the difficulty correction term; chosen because without it the difficulty distribution is too concentrated (Appendix B.2).
  • f (discrimination influence exponent) = 0.49
    Eq. 4; tuned hyperparameter; the prose says it amplifies discrimination influence, but a fractional exponent on a in (0,1) dampens it.
  • η (ability update step size) = 0.004
    Algorithm 1; tuned hyperparameter controlling score convergence speed; the tuning protocol and tuning set are not disclosed.
  • θmin, θmax (ability clamping bounds) = not disclosed
    Algorithm 1 clamps θ into [θmin, θmax]; the bounds are never specified, yet they determine the scores of extreme-ability models (e.g., codegeex4's 0.1038 likely sits near the lower clamp).
assumptions (5)
  • domain assumption Two-parameter logistic IRT model (Eq. 5): P(X=1|θ) = 1/(1+e^{-a(θ-b)}) holds for LLM theorem-proving responses
    Used in Eq. 4 and Algorithm 1 for item information and ability updates; no goodness-of-fit or item-characteristic-curve check is reported.
  • domain assumption Unidimensionality of theorem-proving ability: a single scalar θ suffices
    A single scalar ability is assumed; Table 4 shows large category differences (IMO difficulty 0.978 vs MATH 0.646), and Section 4.2/E.2 report a category-specific anomaly (mathd_numbertheory), both suggesting multidimensional profiles.
  • domain assumption 128 proof attempts per model-theorem pair give stable success-rate estimates
    Eq. 1-3 feed binomial estimates into difficulty and discrimination; for P near 0.5 the SE is about 0.044, and discrimination denominators θ(Mi)-θ(Mj) are as small as 0.123, amplifying noise.
  • domain assumption Pass@128 is a valid prior ability anchor θ(Mi) for the annotation models
    Used in the Eq. 1 correction and Eq. 3 discrimination denominators; the paper reproduces these values itself (e.g., 58.61% for DeepSeek-Prover-V1.5-RL, not the cited 60.2%).
  • ad hoc to paper The hand-designed correction term form in Eq. 1 (weight 1/θ(Mi), scale ε) is appropriate
    Introduced to spread the difficulty distribution (Appendix B.2); its algebraic effect (raising difficulty for theorems solved by weak models) contradicts its prose rationale.
invented entities (1)
  • ability score θ (latent trait)
    purpose: Summarizes each LLM's theorem-proving ability on a single scale, used for model ranking and for selecting test theorems during adaptive evaluation.
    No external criterion validates this construct: the only support is ranking agreement with Pass@N on the same miniF2F benchmark, and for 4 of the 10 models the scores are computed from items calibrated on their own responses.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Psychometric-Based Evaluation for Theorem Proving with Large Language Models." pith.science (2026). https://pith.science/paper/EFBFVPDI

@misc{pith2026250200855,
  author       = {Pith},
  title        = {Pith review of: Psychometric-Based Evaluation for Theorem Proving with Large Language Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EFBFVPDI}},
  note         = {Machine review of arXiv:2502.00855}
}
read the original abstract

Large language models (LLMs) for formal theorem proving have become a prominent research focus. At present, the proving ability of these LLMs is mainly evaluated through proof pass rates on datasets such as miniF2F. However, this evaluation method overlooks the varying importance of theorems. As a result, it fails to highlight the real performance disparities between LLMs and leads to high evaluation costs. This study proposes a psychometric-based evaluation method for theorem proving with LLMs, comprising two main components: Dataset Annotation and Adaptive Evaluation. First, we propose a metric calculation method to annotate the dataset with difficulty and discrimination metrics. Specifically, we annotate each theorem in the miniF2F dataset and grade them into varying difficulty levels according to the performance of LLMs, resulting in an enhanced dataset: miniF2F-Graded. Experimental results show that the difficulty grading in miniF2F-Graded better reflects the theorem difficulty perceived by LLMs. Secondly, we design an adaptive evaluation method to dynamically select the most suitable theorems for testing based on the annotated metrics and the real-time performance of LLMs. We apply this method to evaluate 10 LLMs. The results show that our method finely highlights the performance disparities between LLMs. It also reduces evaluation costs by using only 23% of the theorems in the dataset.

Figures

Figures reproduced from arXiv: 2502.00855 by the authors.

Figure 1
Figure 1. The method consists of two parts. In Part 1: Dataset Annotation, difficulty and discrimination metrics are [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The scatter plot of the dataset annotation results illustrates the relationship between theorem difficulty (x-axis) [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Confusion matrix of model rankings. the grading system. Future work will extend this method to larger datasets and models, providing a scalable benchmark for LLM evaluation in theorem proving. References [1] Humza Naveed, Asad Ullah Khan, Shi Qiu, Muhammad Saqib, Saeed Anwar, Muhammad Usman, Naveed Akhtar, Nick Barnes, and Ajmal Mian. A comprehensive overview of large language models. arXiv preprint arXiv:2307.06435… view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: The scatter plot of the dataset annotation results when the correction term is not used in the difficulty metric [PITH_FULL_IMAGE:figures/full_fig_p015_4.png]
Figure 5
Figure 5. Figure 5: Difficulty Distribution Chart for Theorems in Various Categories.. [PITH_FULL_IMAGE:figures/full_fig_p018_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

51 extracted references · 17 canonical work pages

  1. [1]

    A comprehensive overview of large language models

    Humza Naveed, Asad Ullah Khan, Shi Qiu, Muhammad Saqib, Saeed Anwar, Muhammad Usman, Naveed Akhtar, Nick Barnes, and Ajmal Mian. A comprehensive overview of large language models. arXiv preprint arXiv:2307.06435, 2023

    arXiv 2023

  2. [2]

    A survey of large language models

    Wayne Xin Zhao, Kun Zhou, Junyi Li, Tianyi Tang, Xiaolei Wang, Yupeng Hou, Yingqian Min, Beichen Zhang, Junjie Zhang, Zican Dong, et al. A survey of large language models. arXiv preprint arXiv:2303.18223, 2023

    arXiv 2023

  3. [3]

    Formal mathematical reasoning: A new frontier in ai

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075, 2024

    arXiv 2024

  4. [4]

    Large language models for mathematical reasoning: Progresses and challenges

    Janice Ahn, Rishu Verma, Renze Lou, Di Liu, Rui Zhang, and Wenpeng Yin. Large language models for mathematical reasoning: Progresses and challenges. arXiv preprint arXiv:2402.00157, 2024

    arXiv 2024

  5. [5]

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

    work page 2024

  6. [6]

    Lego-prover: Neural theorem proving with growing libraries

    Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656, 2023

    arXiv

  7. [7]

    Evaluating mathematical reasoning beyond accuracy

    Shijie Xia, Xuefeng Li, Yixin Liu, Tongshuang Wu, and Pengfei Liu. Evaluating mathematical reasoning beyond accuracy. arXiv preprint arXiv:2404.05692, 2024

    arXiv 2024

  8. [8]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer, 2021

    2021

Show all 51 references
  1. [9]

    Isabelle: A generic theorem prover

    Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994

    1994

  2. [10]

    The coq proof assistant a tutorial

    Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant a tutorial. Rapport Technique, 178, 1997

    1997

  3. [11]

    Leandojo: Theorem proving with retrieval-augmented language models

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024

    2024

  4. [12]

    Thor: Wielding hammers to integrate language models and automated theorem provers

    Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygó´ zd´ z, Piotr Miło´s, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35:836...

    2022

  5. [13]

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

    Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022

    arXiv

  6. [14]

    Baldur: Whole-proof generation and repair with large language models

    Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 1229–1241, 2023

    2023

  7. [15]

    Theoremllama: Transforming general-purpose llms into lean4 experts

    Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203, 2024

    2024 arXiv

  8. [16]

    Metamath: Bootstrap your own mathematical questions for large language models

    Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models. arXiv preprint arXiv:2309.12284, 2023

    2023 arXiv

  9. [17]

    Mathverse: Does your multi-modal llm truly see the diagrams in visual math problems? In European Conference on Computer Vision, pages 169–186

    Renrui Zhang, Dongzhi Jiang, Yichi Zhang, Haokun Lin, Ziyu Guo, Pengshuo Qiu, Aojun Zhou, Pan Lu, Kai-Wei Chang, Yu Qiao, et al. Mathverse: Does your multi-modal llm truly see the diagrams in visual math problems? In European Conference on Computer Vision, pages 169–186. Sprin...

    2025

  10. [18]

    Llm reasoners: New evaluation, library, and analysis of step-by-step reasoning with large language models

    Shibo Hao, Yi Gu, Haotian Luo, Tianyang Liu, Xiyan Shao, Xinyuan Wang, Shuhua Xie, Haodi Ma, Adithya Samavedhi, Qiyue Gao, et al. Llm reasoners: New evaluation, library, and analysis of step-by-step reasoning with large language models. arXiv preprint arXiv:2404.05221, 2024

    2024 arXiv

  11. [19]

    An empirical evaluation of llms for solving offensive security challenges

    Minghao Shao, Boyuan Chen, Sofija Jancheska, Brendan Dolan-Gavitt, Siddharth Garg, Ramesh Karri, and Muhammad Shafique. An empirical evaluation of llms for solving offensive security challenges. arXiv preprint arXiv:2402.11814, 2024

    2024 arXiv

  12. [20]

    Cladder: Assessing causal reasoning in language models

    Zhijing Jin, Yuen Chen, Felix Leeb, Luigi Gresele, Ojasv Kamal, LYU Zhiheng, Kevin Blin, Fernando Gonzalez Adauto, Max Kleiman-Weiner, Mrinmaya Sachan, et al. Cladder: Assessing causal reasoning in language models. In Thirty-seventh conference on neural information processing ...

    2023

  13. [21]

    Using llms to facilitate formal verification of rtl

    Marcelo Orenes-Vera, Margaret Martonosi, and David Wentzlaff. Using llms to facilitate formal verification of rtl. arXiv e-prints, pages arXiv–2309, 2023

    2023

  14. [22]

    Stuck in the quicksand of numeracy, far from agi summit: Evaluating llms’ mathematical competency through ontology-guided perturbations

    Pengfei Hong, Deepanway Ghosal, Navonil Majumder, Somak Aditya, Rada Mihalcea, and Soujanya Poria. Stuck in the quicksand of numeracy, far from agi summit: Evaluating llms’ mathematical competency through ontology-guided perturbations. arXiv preprint arXiv:2401.09395, 2024

    2024 arXiv

  15. [23]

    Evaluating llms’ mathematical reasoning in financial document question answering

    Pragya Srivastava, Manuj Malik, Vivek Gupta, Tanuja Ganu, and Dan Roth. Evaluating llms’ mathematical reasoning in financial document question answering. In Findings of the Association for Computational Linguistics ACL 2024, pages 3853–3878, 2024

    2024

  16. [24]

    Efficiently measuring the cognitive ability of llms: An adaptive testing perspective

    Yan Zhuang, Qi Liu, Yuting Ning, Weizhe Huang, Rui Lv, Zhenya Huang, Guanhao Zhao, Zheng Zhang, Qingyang Mao, Shijin Wang, et al. Efficiently measuring the cognitive ability of llms: An adaptive testing perspective. arXiv preprint arXiv:2306.10512, 2023. 12 Running Title for Header

    2023 arXiv

  17. [25]

    tinybench- marks: evaluating llms with fewer examples

    Felipe Maia Polo, Lucas Weber, Leshem Choshen, Yuekai Sun, Gongjun Xu, and Mikhail Yurochkin. tinybench- marks: evaluating llms with fewer examples. arXiv preprint arXiv:2402.14992, 2024

    2024 arXiv

  18. [26]

    S-eval: Automatic and adaptive test generation for benchmarking safety evaluation of large language models

    Xiaohan Yuan, Jinfeng Li, Dongxia Wang, Yuefeng Chen, Xiaofeng Mao, Longtao Huang, Hui Xue, Wenhai Wang, Kui Ren, and Jingyi Wang. S-eval: Automatic and adaptive test generation for benchmarking safety evaluation of large language models. arXiv preprint arXiv:2405.14191, 2024

    2024 arXiv

  19. [27]

    Psychometrics: an introduction

    R Michael Furr. Psychometrics: an introduction. SAGE publications, 2021

    2021

  20. [28]

    Diagnostic measurement: Theory, methods, and applications

    Jonathan Templin, Robert A Henson, et al. Diagnostic measurement: Theory, methods, and applications. Guilford press, 2010

    2010

  21. [29]

    A brief introduction to evidence-centered design

    Robert J Mislevy, Russell G Almond, and Janice F Lukas. A brief introduction to evidence-centered design. ETS Research Report Series, 2003(1):i–29, 2003

    2003

  22. [30]

    The basics of item response theory

    Frank B Baker. The basics of item response theory. ERIC, 2001

    2001

  23. [31]

    Item response theory for psychologists, 2004

    Peter Fayers. Item response theory for psychologists, 2004

    2004

  24. [32]

    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. arXiv preprint arXiv:2109.00110, 2021

    2021 arXiv

  25. [33]

    Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024

    2024 arXiv

  26. [34]

    K. Yang. minif2f-lean4, 2023

    2023

  27. [35]

    Measuring mathematical problem solving with the math dataset

    Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03874, 2021

    2021 arXiv

  28. [36]

    Item response theory

    Li Cai, Kilchan Choi, Mark Hansen, and Lauren Harrell. Item response theory. Annual Review of Statistics and Its Application, 3(1):297–321, 2016

    2016

  29. [37]

    A tutorial on fisher information

    Alexander Ly, Maarten Marsman, Josine Verhagen, Raoul PPP Grasman, and Eric-Jan Wagenmakers. A tutorial on fisher information. Journal of Mathematical Psychology, 80:40–55, 2017

    2017

  30. [38]

    Codegeex: A pre-trained model for code generation with multilingual benchmarking on humaneval-x

    Qinkai Zheng, Xiao Xia, Xu Zou, Yuxiao Dong, Shan Wang, Yufei Xue, Zihan Wang, Lei Shen, Andi Wang, Yang Li, Teng Su, Zhilin Yang, and Jie Tang. Codegeex: A pre-trained model for code generation with multilingual benchmarking on humaneval-x. In Proceedings of the 29th ACM SIGK...

    2023

  31. [39]

    Jiang, Jia Deng, Stella Biderman, and Sean Welleck

    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics, 2023

    2023

  32. [40]

    Theoremllama: Transforming general-purpose llms into lean4 experts, 2024

    Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts, 2024

    2024

  33. [41]

    Code llama: Open foundation models for code

    Baptiste Roziere, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Romain Sauvestre, Tal Remez, et al. Code llama: Open foundation models for code. arXiv preprint arXiv:2308.12950, 2023

    2023 arXiv

  34. [42]

    Qwen2 technical report

    An Yang, Baosong Yang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Zhou, Chengpeng Li, Chengyuan Li, Dayiheng Liu, Fei Huang, Guanting Dong, Haoran Wei, Huan Lin, Jialong Tang, Jialin Wang, Jian Yang, Jianhong Tu, Jianwei Zhang, Jianxin Ma, Jin Xu, Jingren Zhou, Jinze Bai, Jinzheng...

    2024 arXiv

  35. [43]

    Binyuan Hui, Jian Yang, Zeyu Cui, Jiaxi Yang, Dayiheng Liu, Lei Zhang, Tianyu Liu, Jiajun Zhang, Bowen Yu, Kai Dang, et al. Qwen2. 5-coder technical report. arXiv preprint arXiv:2409.12186, 2024

    2024 arXiv

  36. [44]

    Lisa: Language models of isabelle proofs

    Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pages 378–392, 2021

    2021

  37. [45]

    Proofnet: Autoformalizing and formally proving undergraduate-level mathematics

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

    2023 arXiv

  38. [46]

    Qihao Zhu Runxin Xu Junxiao Song Mingchuan Zhang Y .K. Li Y . Wu Daya Guo Zhihong Shao, Peiyi Wang. Deepseekmath: Pushing the limits of mathematical reasoning in open language models, 2024. 13 Running Title for Header A MiniF2F Dataset and Theorem Categories. A.1 Introduction ...

    2024

  39. [47]

    A.2 Theorem Categories The theorems in miniF2F are classified using multiple criteria

    and ProofNet [45], miniF2F is widely recognized for its high-quality data and extensive adoption, making it an ideal benchmark dataset for this study. A.2 Theorem Categories The theorems in miniF2F are classified using multiple criteria. By purpose, they are divided into a tes...

    1974

  40. [48]

    For all the theorems, excluding those with a difficulty value of 1, the difficulty of the remaining theorems roughly follows a normal distribution centered around 0.6

  41. [49]

    This is because, in the miniF2F design, the test set is reserved for evaluation, while the validation set may have been used during model training [32]

    When the theorems are divided into the test set and the validation set, it is evident that the overall difficulty of the test set is higher than that of the validation set, which aligns with our expectations. This is because, in the miniF2F design, the test set is reserved for...

  42. [50]

    This is because competition problems tend to be more complex, but their higher complexity also leads to a lower discrimination

    When the theorems are categorized by source, it is clear that the average difficulty of the IMO, AIME, and AMC competitions is significantly higher than that of MATH and CUSTOM. This is because competition problems tend to be more complex, but their higher complexity also lead...

  43. [51]

    When classified by problem type, we can observe that induction problems are the most difficult for the models, while number theory problems are the easiest. Theorems in the "OTHERS" category, most of which originate from competitions, may involve algebra, number theory, and ot...

    1967

Pith tools

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