Pith. sign in

REVIEW 4 major objections 6 minor 3 cited by

QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs

T0 review · 4 major / 6 minor · reviewed 2026-08-02 · deepseek-v4-flash

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

Pith's one-line read Standard LLM-as-a-Judge protocols systematically over-score university-level mathematical proofs, a new benchmark demonstrates.

desk verdict The qualitative evidence makes the alignment-gap claim believable; the quantitative magnitudes are on shakier ground. read the letter →

arxiv 2602.20629 v3 pith:QWKVSIJI submitted 2026-02-24 cs.LG

Santiago Gonzalez , Alireza Amiri Bavandpour , Peter Ye , Edward Zhang , Ruslans Aleksejevs , Todor Antić , Polina Baron , Sujeet Bhalerao
show 43 more authors
Shubhrajit Bhattacharya Zachary Burton John Byrne Hyungjun Choi Nujhat Ahmed Disha Koppany István Encz Yuchen Fang Robert Joseph George Ebrahim Ghorbani Alan Goldfarb Jing Guo Meghal Gupta Stefano Huber Annika Kanckos Minjung Kang Hyun Jong Kim Dino Lorenzini Levi Lorenzo Tianyi Mao Giovanni Marzenta Ariane M. Masuda Lukas Mauth Ana Mickovic Andres Miniguano-Trujillo Antoine Moulin Wenqi Ni Tomos Parry Kevin Ren Hossein Roodbarani Mathieu Rundström Manjil Saikia Detchat Samart Rebecca Steiner Connor Stewart Dhara Thakkar Jeffrey Tse Vasiliki Velona Yunhai Xiang Sibel Yalç{i}n Jun Yan Ji Zeng Arman Cohan Quanquan C. Liu
This is my paper
classification cs.LG
keywords LLM-as-a-JudgemathematicalproofevaluationalignmentgaprubricinsensitivityQEDBenchautomatedgradinguniversity-levelmathematicssycophancy
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

QEDBench is a benchmark of 272 upper-undergraduate and early-graduate proof problems with expert human scores, built to test the evaluators rather than the solvers. The paper's central claim is that off-the-shelf LLM judges do not grade proofs the way human experts do: they are systematically lenient, with score inflation up to +0.36 on a 0-1 scale, and this leniency varies by mathematical domain. It also finds a discrete-continuous divide in solver performance and a 'rubric insensitivity' in which stricter grading instructions barely change judge behavior. The upshot, if correct, is that current automated judges cannot be trusted alone to evaluate university-level proofs, and that reward models trained on such judgments would reinforce superficial plausibility over rigorous logic.

What carries the argument

The central mechanism is a dual-rubric evaluation matrix: every generated proof is graded against both a course-specific rubric (pedagogical definitions) and an expert-domain rubric (research-level logical soundness), and by seven LLM judges as well as human experts. Comparing AI scores with human scores on the same proofs quantifies the Alignment Gap (AI score minus human score). The tiered expert rubric uses a granular six-level scale to distinguish expository oversights from logical errors, and the decomposition of judge errors into leniency rates and harshness rates exposes a systematic false-positive pattern.

What would settle it

Take a random subset of the 272 problems, have several independent PhD mathematicians grade the same solutions using the same tiered rubric, and compute inter-annotator agreement (for example, score variance or weighted kappa). If human-human disagreement on identical proofs is comparable to the average AI-human delta, the central claim of systematic judge bias collapses; if human graders largely agree, the alignment gap is real.

Watch

Extended reading notes

Core claim

The paper establishes an Alignment Gap: the difference between what LLM judges score and what PhD-level human experts score, measured across a fully crossed matrix of seven judge models and five solver models on 272 proof problems. The headline quantitative claims are that several frontier evaluators systematically inflate scores (up to +0.18 to +0.36 mean inflation depending on judge and domain), that even the strongest judge still has a 38% leniency rate under the expert rubric, and that one evaluator passes 90.2% of solutions where human experts pass 67.7%. The paper also finds that solver performance collapses in discrete constructive domains (Combinatorics, Graph Theory) relative to con

Load-bearing premise

The paper treats the expert human scores as stable ground truth, but it never reports how much the human graders agree with each other; if different PhD experts diverge as much as the LLM judges do, the measured alignment gap would be partly just noise.

Editorial extensions

If this is right

  • If LLM judges are used to select or rank proofs in university-level settings, they will systematically over-credit flawed arguments, so human review remains necessary.
  • Reward models trained on LLM judge scores would inherit the leniency and reinforce 'hallucinated rigor'; process supervision is needed instead.
  • The discrete-continuous divide implies evaluation and training should treat constructive search domains separately from template-retrieval domains instead of regarding mathematical reasoning as a single skill.
  • Rubric insensitivity means prompt engineering with stricter instructions has diminishing returns; alignment must come from model-level changes rather than context-window instructions.
  • QEDBench provides a reusable benchmark for measuring the alignment of future automated judges against a verified expert ground truth.

Reading between the lines

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

  • A natural next test is to measure inter-annotator agreement among expert graders: if independent PhD mathematicians disagree with each other as much as LLM judges diverge from the recorded human scores, part of the measured alignment gap is grading noise rather than judge bias.
  • The findings suggest proof evaluation should be framed as global logical-dependency tracking rather than style or texture matching, pointing toward structure-aware verification systems as a candidate direction.
  • The sycophancy trap predicts that LLM-based process reward models will select verbose, plausible-sounding proofs over concise correct ones; this is testable by comparing reward-model rankings on paired correct and persuasive-but-flawed proofs.
  • The benchmark's online-versus-offline contamination analysis could be extended to check whether 'near-miss' proofs correspond to memorized fragments of textbook solutions, which would sharpen the interpretation of the discrete-continuous gap.
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 / 6 minor

Summary. The paper introduces QEDBench, a benchmark of 272 upper-undergraduate/early-graduate proof problems with 1,300+ model-generated solutions, evaluated by 48 PhD-level human experts over 1,000+ hours, and scored by seven LLM judges under two rubrics (course-specific and expert). The central claim is that standard LLM-as-a-Judge protocols exhibit a systematic 'Alignment Gap': compared with human experts, LLM judges inflate scores on university-level mathematical proofs, the inflation is domain-dependent (largest in discrete areas such as Combinatorics, Discrete Math, and Graph Theory), and top evaluators such as Llama 4 Maverick show extreme leniency. The paper also reports a discrete/continuous reasoning gap among solvers, rubric insensitivity in LLM judges, and no measurable data contamination. Qualitative logs provide concrete examples of LLM judges awarding partial credit to empty API error messages, irrelevant proofs, and hallucinated proofs of false statements.

Significance. If the findings hold, QEDBench would be a valuable resource and the alignment-gap result would be an important warning for automated evaluation of advanced mathematics. The paper's strengths are substantial: a large dual-rubric human-annotated dataset, a fully crossed evaluator-solver matrix, a serious contamination check, and public release of data and logs. The qualitative evidence (Section 5) is particularly compelling: LLM judges systematically reward superficial formatting, irrelevant text, and even false statements, and this makes the existence claim of an alignment gap credible. However, the quantitative magnitudes and the claimed domain-dependence are not yet statistically established because the paper reports no inter-annotator reliability for the human ground truth and no confidence intervals or significance tests for the headline bias deltas. The central contribution is therefore defensible, but the precision of the headline numbers needs strengthening.

major comments (4)
  1. [§3.2 (Expert Evaluator Selection)] The human scores are used as stable ground truth, but no inter-annotator reliability is reported. The paper states that 48 PhD-level evaluators spent 1,000+ hours grading, but does not state whether any solution was graded by more than one expert. With a coarse 0.25-step scale and per-category sample sizes as small as 6 (Complex Analysis, Appendix L), a single expert's idiosyncrasy can shift a category mean by more than several of the reported bias deltas. Please report the grading design (number of experts per solution) and, on a double-graded subsample, Cohen's kappa or ICC and the standard error of the human consensus. Without this, the measured bias magnitudes cannot be separated from annotation noise.
  2. [§4.2, Figure 5] The headline bias deltas (Δ = AI score − human score) are presented without confidence intervals or significance tests, in contrast with the contamination analysis in §4.3, which does include Welch's t and Mann–Whitney U tests. Per-category samples are small (e.g., 19 Graph Theory problems, 6 Complex Analysis problems), and a coarse scale further increases variance. The values +0.18 to +0.36 may be within sampling noise for several cells. Report bootstrap confidence intervals or a mixed-effects model with judge and category as factors, and account for multiple comparisons. This is needed to support the 'systematic, domain-dependent bias' claim at the reported magnitudes.
  3. [§3.3 (Dual-Rubric Strategy) and Limitations] The initial rubrics were synthesized by GPT-5.2 Pro and verified by Gemini 3.0 Pro, and GPT-5.2 Pro is also one of the seven judges. Although human experts iteratively refined the rubrics, the extent and nature of the human edits are not documented. The paper's own Limitations paragraph acknowledges a potential self-preference bias. This is not circularity in the human ground truth, but it is a threat to the calibration claims: if the human experts were anchored to LLM-generated criteria, the measured alignment gap could be partly an artifact of rubric provenance. Please report the degree of human modification and, if feasible, test judge rankings against human-drafted rubrics.
  4. [§4.3 / Appendix L] The contamination analysis is more rigorous than the bias analysis, but the aggregate significance test uses N=1070 model-problem pairs without accounting for clustering by problem: the five solver scores for the same problem share the same online/offline status. Additionally, the online/offline classification relies on o3-deep-research judgments, and 58 of 272 problems were excluded as ambiguous. Report a cluster-robust or by-problem analysis, and consider sensitivity of the conclusion to uncertain classifications. This does not undermine the main alignment-gap claim, but it affects the secondary claim of contamination-freedom.
minor comments (6)
  1. [Figures 7 and 19] Labels inconsistently use 'DeepSeek-V2' instead of 'DeepSeek-Prover-V2'; please make the model names consistent throughout.
  2. [Figure 6 and Section 4.2] The 'Agreement (Accuracy)' metric for binary pass/fail is sensitive to class imbalance. Reporting balanced accuracy or Matthews correlation would make the reliability ceiling claim more robust.
  3. [§4.4 / Appendix J] The rubric-insensitivity conclusion is based mainly on GPT-5.2 Pro correlation values (r=0.69 vs 0.67) without confidence intervals or a test of the difference. Appendix J shows similar patterns for other judges, but the main text should state that the differences are not statistically tested.
  4. [§4.1 and Figure 4] The pass-rate threshold of 0.9 is used throughout without sensitivity analysis. Since the leniency/harshness decomposition in Figure 6 depends directly on this threshold, report robustness for thresholds 0.75 and 1.0.
  5. [Appendix O] The inserted note stating that LLM-generated citations in the evaluation logs 'are not hallucinated phantom papers' is unsupported by the manuscript. Either verify and list these references, or label them as unverified LLM-generated text; the current note is confusing and out of place.
  6. [Section 5.1] The phrase 'evaluate proofs as a bag of valid mathematical statements' is a useful qualitative summary, but it should be explicitly framed as an interpretive summary of the examples, not a formal measurement, to avoid overstatement.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the alignment-gap claim rests on independent human expert scores, and the acknowledged rubric self-preference is not a reduction-by-construction.

full rationale

The paper's central derivation chain is: generate solutions with five solver models; obtain expert human ground-truth scores; compare seven LLM judges to that ground truth under two rubrics. The human scores are not derived from the LLM judges' outputs, and no parameter is fitted to a subset and then 'predicted' on a closely related quantity. The only potentially circular element is that the initial rubrics were drafted by GPT-5.2 Pro and verified by Gemini 3.0 Pro, models that also appear as judges. The paper explicitly flags this in Section 6 (Limitations): 'We also acknowledge a potential "self-preference bias," as GPT-5.2 Pro was utilized in synthesizing the final expert rubric criteria, which may positively skew its own evaluation scores.' This is a real validity caveat for GPT-5.2 Pro's relative ranking, but it is not circularity: the rubrics were iteratively refined by 48 PhD-level experts, and the headline inflation results concern Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max, and Llama 4 Maverick, none of which authored the rubrics. The comparison is not equivalent to its inputs by construction; it is an empirical measurement that could have come out differently. No load-bearing self-citation, uniqueness theorem, or ansatz-smuggling chain appears. The lack of inter-annotator reliability statistics is a data-quality concern, not a circularity.

Assumptions & free parameters 1 free parameters · 3 assumptions · 0 invented entities

The paper introduces no new mathematical entities. The central assumptions are the reliability of human expert grading and the contamination-checking tooling. The pass-rate threshold is the only hand-chosen parameter affecting headline metrics.

free parameters (1)
  • Pass-rate threshold = 0.9
    Binary pass rate (score >= 0.9) is used to define leniency/harshness rates and strictness; a hand-chosen modeling choice that affects headline numbers like Llama 4 Maverick's 74.8% leniency.
assumptions (3)
  • domain assumption PhD-level expert evaluation is an accurate, low-noise ground truth for proof correctness.
    The benchmark defines alignment as agreement with human expert scores; no inter-annotator reliability is reported, so the ground truth's own variance is unmeasured (Section 3.2).
  • domain assumption The o3-deep-research web audit correctly identifies whether each problem has a publicly available solution.
    The contamination analysis (Section 4.3) relies entirely on a single automated LLM agent's search results; 58 problems were excluded due to ambiguous classification, including all 19 Graph Theory problems.
  • domain assumption The curated problems are correctly stated and solvable as intended, apart from deliberate false-statement traps.
    Sections 5.3-5.4 describe problems with false statements or impossible constructions; for those, the human ground truth relies on the evaluator recognizing the issue. If any other problems are mis-stated, the corresponding grades are unreliable.

how reviews work

0 comments
Cite this review

Pith. "Pith review of QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs." pith.science (2026). https://pith.science/paper/QWKVSIJI

@misc{pith2026260220629,
  author       = {Pith},
  title        = {Pith review of: QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QWKVSIJI}},
  note         = {Machine review of arXiv:2602.20629}
}
read the original abstract

As Large Language Models (LLMs) saturate elementary benchmarks, the research frontier has shifted from generation to the reliability of automated evaluation. We demonstrate that standard "LLM-as-a-Judge" protocols suffer from a systematic Alignment Gap when applied to upper-undergraduate to early graduate level mathematics. To quantify this, we introduce QEDBench, the first large-scale dual-rubric alignment benchmark to systematically measure alignment with human experts on university-level math proofs by contrasting course-specific rubrics against expert common knowledge criteria. By deploying a dual-evaluation matrix (7 judges x 5 solvers) against 1,000+ hours of human evaluation, we reveal that certain frontier evaluators like Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max, and Llama 4 Maverick exhibit significant positive bias (up to +0.18, +0.20, +0.30, +0.36 mean score inflation, respectively). Furthermore, we uncover a critical reasoning gap in the discrete domain: while Gemini 3.0 Pro achieves state-of-the-art performance (0.91 average human evaluation score), other reasoning models like GPT-5 Pro and Claude Sonnet 4.5 see their performance significantly degrade in discrete domains. Specifically, their average human evaluation scores drop to 0.72 and 0.63 in Discrete Math, and to 0.74 and 0.50 in Graph Theory. In addition to these research results, we also release QEDBench as a public benchmark for evaluating and improving AI judges. Our benchmark is publicly published at https://github.com/qqliu/Yale-QEDBench.

Figures

Figures reproduced from arXiv: 2602.20629 by the authors.

Figure 1
Figure 1. A side-by-side comparison of the 0.75 (Small Mistake) tier for the “Graph Expansion” problem. While both rubrics pe￾nalize similar errors, the Expert Rubric focuses on implicit logical gaps (e.g., monotonicity), while the Course Rubric focuses on explicit pedagogical derivations (e.g., deriving constraints). 4.1. Frontier Model Performance We evaluated five frontier models: Gemini 3.0 Pro, GPT-5 Pro, o3-deep-researc… view at source ↗
Figure 2
Figure 2. Pass Rates by Discipline. The pass rates (score ≥ 0.9) of frontier models across various mathematical disciplines. We observe that while models achieve high reliability in calculation￾heavy domains like ODEs and Probability, performance drops significantly in structure-heavy domains such as Combinatorics and Graph Theory. achieved only 27.3%. This suggests that while models excel at retrieving theorem templates, the… view at source ↗
Figure 4
Figure 4. Evaluator Strictness. Comparison of pass rates (score ≥ 0.9) across judges. While DeepSeek-V3 (72.2%) aligns most closely with the Human Consensus (67.7%), Llama 4 Maverick (90.2%) exhibits significant grade inflation. line derived from our expert evaluations. We assessed eval￾uators on three axes: Strictness, Domain Bias, and Agree￾ment. 1. The Strictness Gap. As shown in [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figures from the paper (16 more)
Figure 6
Figure 6. Figure 6: dissects the specific failure modes of automated evaluators by isolating False Positives (Hallucinated Rigor) from False Negatives (Harshness). Note that these reliability metrics are evaluated strictly on binary Pass Rates (where a score ≥ 0.9 is considered a pass), r…
Figure 7
Figure 7. Figure 7: Overall model performance on online vs. offline prob￾lems under both evaluation metrics. Error bars reflect the model￾problem pair sample split (Non=440, Noff=630). Neither metric reveals a significant advantage for problems with solutions avail￾able online. the benchm…
Figure 8
Figure 8. Figure 8: Rubric Insensitivity. Correlation bubble plots com￾paring GPT-5.2 Pro against Human Consensus for Expert (Left) and Course-Specific (Right) rubrics. The bubble size represents the density of solution pairs. Despite the additional constraints in the Course-Specific rubr…
Figure 9
Figure 9. Figure 9: Pass Rate Bias Heatmap. The difference between evaluator and human pass rates. The trends mirror the average score bias: discrete domains exhibit positive pass rate inflation (AI models passing more flawed proofs), whereas continuous analysis domains show stronger puni…
Figure 10
Figure 10. Figure 10: Average scores assigned by automated evaluators versus the human expert baseline (0.795). Consistent with the pass rate findings, we observe a systematic positive bias across most frontier models. scores of 0.878 and 0.855 respectively. • Closest Alignment: GPT-5.2 Pr…
Figure 11
Figure 11. Figure 11: Evaluator Bias Heatmap (Course-Specific Rubric). The delta between AI and Human mean scores (∆ = SAI − SHuman). While the overarching patterns mirror the Expert Rubric, introducing pedagogical constraints reveals subtle shifts in judge behavior: top reasoning models b…
Figure 12
Figure 12. Figure 12: Pass Rate Bias Heatmap (Course-Specific Rubric). The difference between AI and Human pass rates. The persistence of severe positive bias (red) in models like Llama 4 Maverick across discrete domains demonstrates “Rubric Insensitivity”: the model continues to pass flaw…
Figure 13
Figure 13. Figure 13: Judge Reliability (Course-Specific Rubric). When evaluated against strict pedagogical constraints using a binary Pass Rate threshold (score ≥ 0.9), the Harshness Rate (False Negatives) generally increases for logic-focused models like DeepSeek-V3, indicating a success…
Figure 14
Figure 14. Figure 14: Judge Alignment (Expert Rubric). Correlation between AI Judges (Y-axis) and Human Consensus (X-axis) on the expert rubric. GPT-5.2 Pro shows the tightest clustering along the y = x diagonal (r = 0.69), indicating high calibration. In contrast, Llama 4 Maverick (r = 0.…
Figure 15
Figure 15. Figure 15: Judge Alignment (Course-Specific Rubric). Comparison under strict pedagogical constraints. Despite the shift in instructions, the distributional geometry remains largely static for top-tier models, confirming the “Rubric Insensitivity” hypothesis. GPT-5.2 Pro maintain…
Figure 16
Figure 16. Figure 16: Rubric Insensitivity Heatmap. Left: Average scores assigned using the standard Expert Rubric. Right: Average scores assigned using the Course-Specific Rubric (which penalizes advanced machinery). The visual patterns are strikingly similar, confirming that prompt const…
Figure 17
Figure 17. Figure 17: LLM Evaluator vs. Solver Pass Rate Matrix (Course-Specific Rubric). Pass rates under the course-specific rubric, which penalizes the use of advanced machinery. The overall structure remains similar, confirming the Rubric Insensitivity hypothesis, though several judges…
Figure 18
Figure 18. Figure 18: LLM Evaluator vs. Solver Pass Rate Matrix (Expert Rubric). Pass rates (score ≥ 0.9) assigned by each AI Judge to each Solver’s solutions under the standard expert rubric. Llama 4 Maverick acts as a universal inflator, grading almost all solvers favorably, while DeepSe…
Figure 19
Figure 19. Figure 19: Performance gap (online−offline) by problem category and solver model. Blue cells denote higher offline scores; red cells denote higher online scores. The stochastic sign pattern across both panels is indicative of baseline difficulty variance rather than a systematic…
Figure 20
Figure 20. Figure 20: Per-category performance breakdown for online and offline problems. Each panel displays a faceted grid of categories, featuring grouped bars for each model. The absence of a consistent online advantage across models within any single category refutes the presence of s…
Figure 21
Figure 21. Figure 21: Leniency Analysis: AI Judge vs. Human Evaluator. A stacked distribution of grading verdicts across all evaluated solutions. Llama 4 Maverick is excessively lenient, whereas DeepSeek-V3 diverges towards strictness. GPT-5.2 Pro strikes the best balance of low leniency a…

Discussion (0). Sign in to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness

    cs.CL 2026-05 unverdicted novelty 7.0 of 10

    LLM proofs for hard math problems show large differences in quality metrics like conciseness and cognitive simplicity that correctness-only tests miss, along with trade-offs between quality and correctness.

  2. Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness

    cs.CL 2026-05 unverdicted novelty 7.0 of 10

    ProofRank benchmark shows substantial differences in LLM proof quality not captured by correctness, with trade-offs between quality metrics and accuracy.

  3. A Scalable Approach to Evaluating Moral Sensitivity in LLMs

    cs.CY 2026-07 conditional novelty 6.5 of 10

    Under morally irrelevant noise, eight LLMs preserve the semantic content of identified moral features above calibrated floors, despite significant changes in feature counts.

Reference graph

Works this paper leans on

51 extracted references · 12 linked inside Pith · cited by 2 Pith papers

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

  2. [2]

    Balunovi \'c , M., Dekoninck, J., Jovanovi \'c , N., Petrov, I., and Vechev, M. T. MathConstruct : Challenging LLM reasoning with constructive proofs. In International Conference on Machine Learning (ICML), 2025

    2025

  3. [3]

    W., Keutzer, K., and Gholami, A

    Bamba, U., Yang, H., Tiwari, R., Mahoney, M. W., Keutzer, K., and Gholami, A. Reward under attack: Evaluating the sensitivity of process reward models. In ICML 2025 Workshop on AI for Math, 2025

    2025

  4. [4]

    Analysis: An Introduction

    Beals, R. Analysis: An Introduction. Cambridge University Press, 2004

    2004

  5. [5]

    and Zastawniak, T

    Capi \'n ski, M. and Zastawniak, T. Probability Through Problems. Problem Books in Mathematics. Springer, 2001

    2001

  6. [6]

    Stop summation: Min-form credit assignment is all process reward model needs for reasoning

    Cheng, J., Qiao, R., Li, L., Guo, C., Wang, J., Xiong, G., Lv, Y., and Wang, F.-Y. Stop summation: Min-form credit assignment is all process reward model needs for reasoning. arXiv preprint arXiv:2504.15275, 2025

    arXiv 2025

  7. [7]

    U-MATH : A university-level benchmark for evaluating mathematical skills in large language models

    Chernyshev, K., Polshkov, V., Stepanov, V., Myasnikov, A., Artemova, E., Miasnikov, A., and Tilga, S. U-MATH : A university-level benchmark for evaluating mathematical skills in large language models. In Proceedings of the Fourth Workshop on Generation, Evaluation and Metrics (GEM), 2025

    2025

  8. [8]

    Training verifiers to solve math word problems

    Cobbe, K., Kosaraju, V., Bavarian, M., Chen, M., Jun, H., Kaiser, L., Plappert, M., Tworek, J., Hilton, J., Nakano, R., Hesse, C., and Schulman, J. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021

    arXiv 2021

Show all 51 references
  1. [9]

    Coddington, E. A. An Introduction to Ordinary Differential Equations. Prentice-Hall, 1961

    1961

  2. [10]

    The Lean theorem prover (system description)

    de Moura, L., Kong, S., Avigad, J., van Doorn, F., and von Raumer, J. The Lean theorem prover (system description). In International Conference on Automated Deduction (CADE), pp.\ 378--388. Springer, 2015

    2015

  3. [11]

    D., Nikolova, K., Georgiev, N., Kalinkova, V., and Ismoldayev, M

    Dekoninck, J., Petrov, I., Minchev, K., Balunovi \'c , M., Vechev, M., Marinov, M., Drencheva, M., Konova, L., Shumanov, M., Tsvetkov, K., Drenchev, N., Todorov, L. D., Nikolova, K., Georgiev, N., Kalinkova, V., and Ismoldayev, M. The open proof corpus: A large-scale study of ...

    2025

  4. [12]

    Graph Theory, volume 173 of Graduate Texts in Mathematics

    Diestel, R. Graph Theory, volume 173 of Graduate Texts in Mathematics. Springer, 5th edition, 2017

    2017

  5. [13]

    Douglass, S. A. Introduction to Mathematical Analysis. Addison-Wesley, 1996

    1996

  6. [14]

    Dummit, D. S. and Foote, R. M. Abstract Algebra. John Wiley & Sons, 3rd edition, 2003

    2003

  7. [15]

    Algorithms

    Erickson, J. Algorithms. Independently published, 2019. URL https://jeffe.cs.illinois.edu/teaching/algorithms/. 1st Edition

    2019

  8. [16]

    Test of time: A benchmark for evaluating LLMs on temporal reasoning

    Fatemi, B., Kazemi, M., Tsitsulin, A., Malkan, K., Yim, J., Palowitch, J., Seo, S., Halcrow, J., and Perozzi, B. Test of time: A benchmark for evaluating LLMs on temporal reasoning. arXiv preprint arXiv:2406.09170, 2024

    2024 arXiv

  9. [17]

    F., Denain, J.-S., Ho, A., Santos, E

    Glazer, E., Erdil, E., Besiroglu, T., Chicharro, D., Chen, E., Gunning, A., Olsson, C. F., Denain, J.-S., Ho, A., Santos, E. d. O., J \"a rviniemi, O., Barnett, M., Sandler, R., Sevilla, J., Ren, Q., Pratt, E., Levine, L., Barkley, G., Stewart, N., Grechuk, B., Grechuk, T., an...

    2024 arXiv

  10. [18]

    L., Knuth, D

    Graham, R. L., Knuth, D. E., and Patashnik, O. Concrete Mathematics: A Foundation for Computer Science. Addison-Wesley, 2nd edition, 1994

    1994

  11. [19]

    Guo, D., Liu, J., Fan, Z., He, Z., Li, H., Li, Y., Wang, Y., and Fung, Y. R. Mathematical proof as a litmus test: Revealing failure modes of advanced large reasoning models. arXiv preprint arXiv:2506.17114, 2025

    2025

  12. [20]

    Measuring mathematical problem solving with the MATH dataset

    Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., and Steinhardt, J. Measuring mathematical problem solving with the MATH dataset. In NeurIPS, 2021

    2021

  13. [21]

    A rosetta stone for AI benchmarks, 2025

    Ho, A., Denain, J.-S., Atanasov, D., Albanie, S., and Shah, R. A rosetta stone for AI benchmarks, 2025. URL https://epoch.ai/blog/a-rosetta-stone-for-ai-benchmarks. Epoch AI Blog

    2025

  14. [22]

    and Rosen, M

    Ireland, K. and Rosen, M. A Classical Introduction to Modern Number Theory, volume 84 of Graduate Texts in Mathematics. Springer, 2nd edition, 1990

    1990

  15. [23]

    Z., Sahai, S., and Leong, B

    Jain, S., Ahmed, U. Z., Sahai, S., and Leong, B. Beyond consensus: Mitigating the agreeableness bias in LLM judge evaluations. arXiv preprint arXiv:2510.11822, 2025

    2025

  16. [24]

    Probability Theory: A Comprehensive Course

    Klenke, A. Probability Theory: A Comprehensive Course. Springer, 2nd edition, 2013

    2013

  17. [25]

    No free labels: Limitations of LLM -as-a-judge without human grounding

    Krumdick, M., Lovering, C., Reddy, V., Ebner, S., and Tanner, C. No free labels: Limitations of LLM -as-a-judge without human grounding. arXiv preprint arXiv:2503.05061, 2025

    2025

  18. [26]

    Grading scale impact on LLM -as-a-judge: Human- LLM alignment is highest on 0-5 grading scale

    Li, W., Zhao, M., Dong, W., Cai, J., Wei, Y., Pocress, M., Li, Y., Yuan, W., Wang, X., Hou, R., Lou, K., Zeng, W., Yang, Y., Du, Y., and Wang, M. Grading scale impact on LLM -as-a-judge: Human- LLM alignment is highest on 0-5 grading scale. arXiv preprint arXiv:2601.03444, 2026

    2026

  19. [27]

    S., Zhang, H., Zhuang, V., Zaharia, M., and Min, S

    Ma, W., Cojocaru, A., Kolhe, N., Louie, B., Sharif, R. S., Zhang, H., Zhuang, V., Zaharia, M., and Min, S. Reliable fine-grained evaluation of natural language math proofs. arXiv preprint arXiv:2510.13888, 2025

    2025

  20. [28]

    Brains vs

    Mahdavi, H., Hashemi, A., Daliri, M., Mohammadipour, P., Farhadi, A., Malek, S., Yazdanifard, Y., Khasahmadi, A., and Honavar, V. Brains vs. bytes: Evaluating LLM proficiency in olympiad mathematics. arXiv preprint arXiv:2504.01995, 2025 a

    2025 arXiv

  21. [29]

    RefGrader : Automated grading of mathematical competition proofs using agentic workflows

    Mahdavi, H., Mahdavinia, P., Malek, S., Mohammadipour, P., Hashemi, A., Daliri, M., Farhadi, A., Khasahmadi, A., Mireshghallah, N., and Honavar, V. RefGrader : Automated grading of mathematical competition proofs using agentic workflows. arXiv preprint arXiv:2510.09021, 2025 b

    2025

  22. [30]

    Scaling generative verifiers for natural language mathematical proof verification and selection

    Mahdavi, S., Kisacanin, B., Toshniwal, S., Du, W., Moshkov, I., Armstrong, G., Liao, R., Thrampoulidis, C., and Gitman, I. Scaling generative verifiers for natural language mathematical proof verification and selection. arXiv preprint arXiv:2511.13027, 2025 c

    2025

  23. [31]

    and Ne s et r il, J

    Matou s ek, J. and Ne s et r il, J. An Invitation to Discrete Mathematics. Oxford University Press, 2nd edition, 2008

    2008

  24. [32]

    and Raghavan, P

    Motwani, R. and Raghavan, P. Randomized Algorithms. Cambridge University Press, 1995

    1995

  25. [33]

    S., and Montgomery, H

    Niven, I., Zuckerman, H. S., and Montgomery, H. L. An Introduction to the Theory of Numbers. John Wiley & Sons, 5th edition, 1991

    1991

  26. [34]

    Petrov, I., Dekoninck, J., Baltadzhiev, L., Drencheva, M., Minchev, K., Balunovi \'c , M., Jovanovi \'c , N., and Vechev, M. T. Proof or bluff? evaluating LLMs on 2025 USA math olympiad. arXiv preprint arXiv:2503.21934, 2025 a

    2025 arXiv

  27. [35]

    BrokenMath : A benchmark for sycophancy in theorem proving with LLMs

    Petrov, I., Dekoninck, J., and Vechev, M. BrokenMath : A benchmark for sycophancy in theorem proving with LLMs . arXiv preprint arXiv:2510.04721, 2025 b

    2025

  28. [36]

    ReasonBENCH : Benchmarking the (in)stability of LLM reasoning

    Potamitis, N., Klein, L., and Arora, A. ReasonBENCH : Benchmarking the (in)stability of LLM reasoning. arXiv preprint arXiv:2512.07795, 2025

    2025 arXiv

  29. [37]

    Yale-QEDBench : Code and dataset for quantifying the alignment gap in automated evaluation of university-level mathematical proofs

    QEDBench. Yale-QEDBench : Code and dataset for quantifying the alignment gap in automated evaluation of university-level mathematical proofs. https://github.com/qqliu/Yale-QEDBench, 2026

    2026

  30. [38]

    Sane, S. S. Combinatorial Techniques. Hindustan Book Agency, 2013

    2013

  31. [39]

    S., Sun, Z., Teichmann, J., Thomas, R

    Schmitt, J., B \'e rczi, G., Dekoninck, J., Feusi, J., Gehrunger, T., Appenzeller, R., Bryan, J., Canova, N., de Wolff, T., Gaia, F., van Garrel, M., Hashemi, B., Holmes, D., Lopez, A., Jaeck, V., J rgensen, M., Kelk, S., Kuhlmann, S., Kurpisz, A., Meroni, C., Metzler, I., Möl...

    2025 arXiv

  32. [40]

    o zl \"u kl \

    Se ler, K., Rong, Y., G \"o zl \"u kl \"u , E., and Kasneci, E. Benchmarking large language models for math reasoning tasks. arXiv preprint arXiv:2408.10839, 2024

    2024 arXiv

  33. [41]

    The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity

    Shojaee, P., Mirzadeh, I., Alizadeh, K., Horton, M., Bengio, S., and Farajtabar, M. The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity. arXiv preprint arXiv:2506.06941, 2025

    2025 arXiv

  34. [42]

    A Computational Introduction to Number Theory and Algebra

    Shoup, V. A Computational Introduction to Number Theory and Algebra. Cambridge University Press, 2nd edition, 2009

    2009

  35. [43]

    Stein, E. M. and Shakarchi, R. Complex Analysis, volume 2 of Princeton Lectures in Analysis. Princeton University Press, 2003

    2003

  36. [44]

    From calculation to adjudication: Examining LLM judges on mathematical reasoning tasks

    Stephan, A., Zhu, D., A enmacher, M., Shen, X., and Roth, B. From calculation to adjudication: Examining LLM judges on mathematical reasoning tasks. In Proceedings of the Fourth Workshop on Generation, Evaluation and Metrics (GEM), 2025

    2025

  37. [45]

    Ordinary Differential Equations and Dynamical Systems, volume 140 of Graduate Studies in Mathematics

    Teschl, G. Ordinary Differential Equations and Dynamical Systems, volume 140 of Graduate Studies in Mathematics. American Mathematical Society, 2012

    2012

  38. [46]

    S., Naidu, S., Hegde, C., LeCun, Y., Goldstein, T., Neiswanger, W., and Goldblum, M

    White, C., Dooley, S., Roberts, M., Pal, A., Feuer, B., Jain, S., Shwartz-Ziv, R., Jain, N., Saifullah, K., Dey, S., Agrawal, S., Sandha, S. S., Naidu, S., Hegde, C., LeCun, Y., Goldstein, T., Neiswanger, W., and Goldblum, M. LiveBench : A challenging, contamination-limited LL...

    2024 arXiv

  39. [47]

    D., Leng, C., and Liu, F

    Zhang, Y., Kuzborskij, I., Lee, J. D., Leng, C., and Liu, F. DAG-Math : Graph-guided mathematical reasoning in LLMs . In Advances in Neural Information Processing Systems (NeurIPS), 2024

    2024

  40. [48]

    The lessons of developing process reward models in mathematical reasoning

    Zhang, Z., Zheng, C., Wu, Y., Zhang, B., Lin, R., Yu, B., Liu, D., Zhou, J., and Lin, J. The lessons of developing process reward models in mathematical reasoning. arXiv preprint arXiv:2501.07301, 2025

    2025 arXiv

  41. [49]

    One token to fool LLM -as-a-judge

    Zhao, Y., Liu, H., Yu, D., Kung, S., Chen, M., Mi, H., and Yu, D. One token to fool LLM -as-a-judge. arXiv preprint arXiv:2507.08794, 2025

    2025 arXiv

  42. [50]

    P., Zhang, H., Gonzalez, J

    Zheng, L., Chiang, W.-L., Sheng, Y., Zhuang, S., Wu, Z., Zhuang, Y., Lin, Z., Li, Z., Li, D., Xing, E. P., Zhang, H., Gonzalez, J. E., and Stoica, I. Judging LLM -as-a-judge with MT -bench and chatbot arena. In NeurIPS, 2023

    2023

  43. [51]

    Unmasking reasoning processes: A process-aware benchmark for evaluating structural mathematical reasoning in LLMs

    Zheng, X., Zhai, W., Wang, W., Yang, B., Li, W., Luo, R., Sun, H., Wang, Y., Li, Z., Wang, M., Du, Y., Lin, G., Wang, Y., Xu, X., Mo, Y., Ren, X., Wei, H., and Xu, Z. Unmasking reasoning processes: A process-aware benchmark for evaluating structural mathematical reasoning in L...

    2026

Pith tools

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