{"id":"c4f3bfd4-11c3-43c5-b58f-46db0995d06c","arxiv_id":"2502.00855","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"The authors annotate miniF2F theorems with LLM-computed difficulty and discrimination scores, then use adaptive testing to rank 10 theorem-proving LLMs using only about 23% of the theorems.","lead":"This paper builds a smarter test for AI math provers: it grades each problem in the standard miniF2F benchmark by how likely AI models are to solve it, then gives each new model only the most informative problems. The authors claim this spot check uses about 23% of the problems and still shows real differences between models, cutting evaluation cost by about 76%.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Item parameters are computed from only four annotation models; a leave-one-out re-estimation could show they are unstable, invalidating the adaptive ability scores.","rationale":"The reader's weakest_assumption correctly identifies the stability of item parameters and the unidimensional IRT model as the load-bearing premise. My analysis agrees and sharpens the concern: the paper contains internal evidence of model-specific item behavior (Section 4.2, E.2), and the small number of annotation models makes the parameters statistically fragile, especially given the small discrimination denominators. The concrete test—a leave-one-out stability analysis—directly targets this premise and would settle whether the adaptive selection and ability scores can be trusted. Since the paper already shows partial validity evidence (ranking agreement, monotone difficulty grading), the result should remain CONDITIONAL pending this check rather than being rejected outright. I therefore recommend UNCHANGED, with the caveat that the suggested test is a necessary condition for the central claim to hold.","tokens_in":19780,"tokens_out":2776,"duration_ms":31795,"concrete_test":"Leave-one-annotation-model-out stability check: re-estimate Difficulty(x) with Eq. (1)–(2) and Discrimination(x) with Eq. (3) for each of the four triples of annotation models. For each theorem, compute the difference between the full-model and leave-one-out estimates. If the mean absolute shift in difficulty exceeds 0.1, or the Spearman correlation between the original and any leave-one-out difficulty ranking falls below 0.9, the item parameters are not stable across annotation models, directly undermining the claimed validity. A second, complementary check is to bootstrap the ability score by resampling the 128 attempts per theorem and re-running the adaptive algorithm; if the 95% confidence interval for a model's ability score is wider than the observed gap between adjacent models (e.g., Qwen2.5-Coder 0.2344 vs.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim—that ability scores accurately reflect theorem-proving ability—depends on the item parameters (difficulty and discrimination) being stable, model-independent properties of theorems. These parameters are computed from exactly four annotation models via Eq. (1)–(3). The paper itself documents a violation of this assumption in Section 4.2 and Appendix E.2: 'some theorems in mathd_numbertheory exhibit high discrimination at lower difficulty levels due to one model's exceptional performance in this category.' This is direct evidence that a single model's idiosyncratic skill inflates discrimination and shifts difficulty estimates. The discrimination formula Eq. (3) averages pairwise slopes (Pi−Pj)/(θi−θj); with ability differences as small as 0.12 (e.g., CodeLlama 0.123 vs. Qwen 0.178, from Table 1), binomial noise in pass rates (SE≈0.044 at p=0.5 with 128 attempts) is amplified by the small denominator. If the parameters are noisy or model-specific, both the information-based item selection (Eq. 4) and the ability update rule (θ←θ+η·a·(r−P(θ))) inherit the bias. Furthermore, the 127 theorems with difficulty=1 and discrimination=0 are never selected (information=0), so the method cannot distinguish among high-ability models; the stable-looking ranking agreement with Pass@16–64 does not establish that the scores are valid on an absolute scale. This is not an external philosophical objection: the paper's own reported anomaly is the canary in the coal mine.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":20073,"tokens_out":3394,"duration_ms":34835,"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":[{"comment":"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.","section":"§3.1.2, Eq. (1)–(3), §4.2, E.2"},{"comment":"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.","section":"§3.2.2, Algorithm 1, §4.1"},{"comment":"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.","section":"§5.2, F.2"},{"comment":"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.","section":"§5.1, Table 3"}],"minor_comments":[{"comment":"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.","section":"Abstract and Table 1"},{"comment":"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.","section":"§3.1.2 and Eq. (5)"},{"comment":"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.","section":"Algorithm 1"},{"comment":"The phrase 'a 7B-metric model' should be 'a 7B-parameter model.'","section":"Introduction, first paragraph"},{"comment":"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).","section":"Related Work"}],"recommendation":"major_revision","confidential_remarks":"The paper addresses a timely problem and the empirical setup (disjoint annotation/evaluation LLMs, released dataset) is a step in the right direction. The main risk is the validity of the item parameters; the authors' own E.2 anomaly indicates that a single model can distort discrimination. I would encourage the editor to request a leave-one-out stability analysis and a clearly specified tuning protocol as a condition for further consideration. If those checks are favorable, the contribution could be a solid addition to the LLM-evaluation literature."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is a credible first attempt to bring item response theory and computerized adaptive testing to LLM theorem-proving evaluation. The genuinely new pieces are miniF2F-Graded (the annotated dataset) and the adaptive protocol that gets to a stable ability score using only about a quarter of the theorems. The released data and the clean split between the four annotation models and the six evaluation models are real assets: Table 3 shows monotonic pass-rate decrease across difficulty levels for the held-out models, which is genuine out-of-sample evidence that the difficulty grading transfers.\n\nThe main weakness is that the validity of the ability scores as an absolute measure is not established. Item parameters are computed from only four annotation models, and the paper itself documents a number-theory category where one model's exceptional performance inflates discrimination at low difficulty. That is a red flag: if discrimination is partly model-specific, the item selection and the score updates inherit that bias. The stress-test suggestion of leave-one-out re-estimation is exactly the right check. Relatedly, the four annotation models are also scored in-sample, so their ability scores and the ranking agreement with Pass@16-64 for those models are partly circular. The hyperparameters [f, eta] are tuned but the procedure is not disclosed; if tuning used the same ten models, that is another leak.\n\nThe claim that ability scores 'accurately reflect' proof ability is too strong. What they show is that the scores rank models consistently with pass-rate rankings on the independent evaluation models (modulo one near-tie), and that the scores spread out the RL-vs-SFT gap that Pass@128 compresses. That is useful, but it is not validity on an absolute scale. There are also no error bars; binomial noise in pass rates, amplified by small discrimination denominators, means the fine-grained differences (e.g., 0.2344 vs 0.2353) are unlikely to be meaningful. The hardest 127 theorems are never selected because they have zero information, so the method structurally cannot distinguish among near-SOTA models on the hardest content. Finally, the 76% cost saving is real for each new model once the annotation exists, but the amortized cost of running four models on all 488 theorems with 128 attempts each should be acknowledged.\n\nNone of this is fatal. The paper is honest about the limited number of annotation models and the anomaly in number theory. The released dataset and the adaptive protocol are reusable. A serious referee should ask for leave-one-out stability analysis, error bars, disclosed tuning, and softer claims. With those, it would be a solid contribution to LLM evaluation methodology.","headline":"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.","tokens_in":20678,"tokens_out":3149,"would_cite":false,"duration_ms":31408,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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%.","keywords":["theorem proving","large language models","item response theory","adaptive evaluation","miniF2F-Graded","difficulty and discrimination","Lean 4","pass rate evaluation"],"falsifier":"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.","tokens_in":19513,"feed_emoji":"📐","tokens_out":6833,"duration_ms":60189,"temperature":0.7,"pith_summary":"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.","feed_headline":"Adaptive psychometrics ranks theorem-proving LLMs on 23% of miniF2F","feed_subtitle":"Difficulty-weighted ability scores expose gaps Pass@128 hides while testing 77% fewer theorems.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the miniF2F dataset of 488 formal Olympiad-level theorems, including the original human five-level difficulty grading that the new grading is compared against.","marker":"[32]"},{"why":"DeepSeek-Prover-V1.5 is the strongest annotation model and the motivating example where Pass@128 understates differences between SFT and RL versions.","marker":"[5]"},{"why":"Provides the adaptive-testing viewpoint for measuring LLM cognitive ability that the method adapts to theorem proving.","marker":"[24]"},{"why":"Source of the two-parameter item response theory model (Eq. 5) used to define the probability $P(t_i,\\theta)$ in selection and updating.","marker":"[31]"},{"why":"Supplies the item response theory framework and Fisher information concepts used for the theorem-selection information score.","marker":"[36]"},{"why":"The Fisher information function on which the modified information score in Eq. 4 is based.","marker":"[37]"},{"why":"Provides the Lean-4 re-formalization of miniF2F with informal prefixes that the paper uses for annotation and evaluation.","marker":"[34]"},{"why":"DeepSeek-Prover-V1 is one of the evaluation models and the prior benchmark pass rate that the adaptive scores are compared with.","marker":"[33]"}],"fun_headline_variants":["Psychometric grading exposes LLM proving gaps on 23% of miniF2F","Adaptive test ranks theorem provers on 77% fewer examples","Difficulty-weighted scores reveal ability hidden by Pass@128","MiniF2F-Graded: adaptive psychometrics cuts evaluation cost by 77%","Adaptive theorem-proving evaluation: 23% data, sharper rankings"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Psychometric grading exposes LLM proving gaps on 23% of miniF2F","Adaptive test ranks theorem provers on 77% fewer examples","Difficulty-weighted scores reveal ability hidden by Pass@128","MiniF2F-Graded: adaptive psychometrics cuts evaluation cost by 77%","Adaptive theorem-proving evaluation: 23% data, sharper rankings"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000293,"raw_usage":{"total_tokens":1739,"prompt_tokens":1010,"completion_tokens":729,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":626,"completion_tokens_details":{"reasoning_tokens":632}},"tokens_in":626,"tokens_out":729,"duration_ms":7879,"temperature":1.0,"reasoning_tokens":632,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T17:32:14.361254+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"DeepSeek-Prover-V1.5 is the strongest annotation model and the motivating example where Pass@128 understates differences between SFT and RL versions."},{"cited_title":"Item response theory for psychologists, 2004","cited_arxiv_id":null,"evidence_quote":"Source of the two-parameter item response theory model (Eq. 5) used to define the probability $P(t_i,\\theta)$ in selection and updating."},{"cited_title":"A tutorial on fisher information","cited_arxiv_id":null,"evidence_quote":"The Fisher information function on which the modified information score in Eq. 4 is based."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the Lean-4 re-formalization of miniF2F with informal prefixes that the paper uses for annotation and evaluation."}],"review_version":1}