PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Santiago Gonzalez, Alireza Amiri Bavandpour, Peter Ye, Edward Zhang, Ruslans Aleksejevs, Todor Antić, Polina Baron, Sujeet Bhalerao, 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çın, Jun Yan, Ji Zeng, Arman Cohan, Quanquan C. Liu

arXiv:2602.20629v3cs.LG

TL;DR

Automated evaluation of university-level mathematical proofs remains poorly aligned with expert judgment. QEDBENCH measures this gap using dual rubrics and a 7 × 5 judge–solver matrix, revealing domain-specific solver weaknesses and judge bias. The benchmark supports calibration against more than 1,000 hours of expert evaluation.

  • Problem

    Existing automated proof evaluation is scalable but correlates poorly with expert judgment, while verified approaches have high annotation costs.

  • Method

    QEDBENCH uses dual course-specific and expert rubrics, five frontier solvers, seven judges, and expert-refined human ground truth to quantify alignment.

  • Results

    Models perform strongly on procedural domains but can collapse on constructive discrete proofs, while judges exhibit systematic and domain-dependent alignment gaps.

  • Takeaways & Limitations

    Reliable mathematical evaluation requires auditing judges separately from solvers and calibrating them against expert standards rather than relying on surface plausibility.

  • Takeaways & Limitations

    The study uses static expert ground truth, focuses on English-language reasoning, and may undercount valid non-standard proofs despite multi-expert adjudication.

Abstract

from arXiv · show

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.

1. Introduction

QEDBENCH targets the reliability of automated evaluation for university-level mathematical proofs, separating proof generation from judge alignment through dual rubrics and a crossed evaluator–solver design.

  • QEDBENCH audits LLM judges and proof-generation capabilities across ten upper-undergraduate and early-graduate mathematical disciplines.
  • The study generates solutions with five frontier models and evaluates them using expert-engineered course-specific and expert-domain rubrics.
  • Seven judge models grade the solutions under both rubrics, enabling alignment-gap measurement by comparing 7 × 5 evaluation matrices with human ground truth.
  • The benchmark addresses whether off-the-shelf LLMs verify abstract proofs, handle constructive reasoning, and respect undergraduate pedagogical constraints.
  • QEDBENCH releases a calibrated proof-evaluation standard with more than 1,000 hours of expert evaluation, dual rubrics, and evaluation logs.

2. Related Work

QEDBENCH occupies a middle ground between competition benchmarks and research-level mathematics by emphasizing semantic quality and verifiable university-level proofs.

  • Prior work has advanced mathematical benchmarking toward expert and research levels while attempting to unify heterogeneous metrics.
  • QEDBENCH targets upper-undergraduate and early-graduate curricula, making full-text proofs harder than high-school competitions but more verifiable than novel research.
  • Analyses of large reasoning models suggest that apparent improvements may reflect pattern matching, while reasoning traces can remain unstable.
  • LLM-as-a-Judge systems and specialized evaluators have shown promise on Olympiad-style problems, motivating further scrutiny beyond competition mathematics.
  • QEDBENCH provides a counter-weight to competition-centric benchmarks by showing that solving proficiency does not guarantee grading reliability in abstract mathematics.

3. QEDBENCH Methods

QEDBENCH combines curated university-level proof problems, expert human ground truth, dual rubrics, and a fully crossed 7 × 5 judge–solver evaluation matrix.

  • The benchmark contains 272 expert-curated problems across ten mathematical domains and more than 1,300 generated proofs with expert scores and annotations.
  • Problems undergo source-diversity selection, manual syntactic rewording, and adversarial web audits to reduce contamination and memorization.
  • The audit obtained high-confidence solution-availability annotations for 214 problems, while 58 were excluded because classification was ambiguous.
  • Forty-eight expert evaluators contributed more than 1,000 hours of grading, with assignments matched to publication domains.
  • Human evaluations use a tiered Expert Rubric ranging from 0 to 1.0 to distinguish fundamental logical failures from expository oversights.
  • The dual-rubric strategy contrasts definition-focused course grading with an expert rubric that penalizes hidden fallacies and circular reasoning.
  • Human experts refine rubric drafts, while LLM judges evaluate proofs under both rubrics in a deterministic 7 × 5 matrix designed to isolate judge bias from solver skill.

4. Results

Results show strong performance on procedural domains but major weaknesses in constructive discrete reasoning, alongside substantial domain- and judge-specific alignment failures.

  • Overall performance: Gemini 3.0 Pro achieves an 86.4% overall pass rate and 0.91 average score, leading the evaluated frontier solvers.
  • Constructive reasoning: 100.0% pass rates in ODEs contrast with 9.1% for DeepSeek-Prover-V2 and 27.3% for Claude Sonnet 4.5 in Combinatorics.
  • Discrete reasoning: Gemini 3.0 Pro reaches 89.5% in Graph Theory but 72.7% in Combinatorics, while Claude Sonnet 4.5 reaches 15.8% in Graph Theory.
  • Partial credit: Binary pass rates can hide partial conceptual understanding, which matters for training signals and distinguishing near-miss proofs from fully rigorous solutions.
  • Partial credit: Analysis models often average approximately 0.88 despite lower strict pass rates, reflecting structurally sound proofs with subtle fatal gaps.
  • Judge strictness: Llama 4 Maverick passes 90.2% against a 67.7% human baseline, whereas DeepSeek-V3 is closest at 72.2%.
  • Alignment gap: Evaluator bias is domain-dependent: Llama 4 Maverick and Qwen 2.5 Max show +0.36 and +0.30 in Combinatorics, while DeepSeek-V3 and Grok 4 show −0.14 and −0.15 in Complex Analysis.
  • Alignment gap: GPT-5.2 Pro most closely matches human evaluators across the widest range of domains, but Algorithms shows punitive biases for Gemini 3 Pro (−0.05) and Grok 4 (−0.07).

3. Decomposing Error Modes: Leniency vs. Rigidity.

QEDBENCH separates evaluator leniency from rigidity and shows that automated judges can both approve flawed proofs and reject valid ones. Rubric constraints also produce limited alignment changes, while solver models frequently violate pedagogical requirements by retrieving advanced machinery.

  • Leniency: 74.8% Leniency Rate marks Llama 4 Maverick as the most permissive judge relative to human ground truth.The benchmark defines reliability using binary pass rates, with scores ≥0.9 counted as passes.
  • Rigidity: 12.3% Harshness Rate makes DeepSeek-V3 the strictest auditor, while its Leniency Rate remains 39.6%.Its rejection of valid solutions indicates difficulty generalizing beyond standard proof templates.
  • Reliability ceiling: 38.0% Leniency Rate leaves GPT-5.2 Pro below a reliability ceiling despite being the strongest evaluator.The result highlights persistent difficulty aligning automated judgments with human mathematical evaluation.
  • Rubric insensitivity: Pearson correlation changes from r = 0.69 under the Expert Rubric to r = 0.67 under the Course-Specific Rubric.Mean Absolute Error changes from 0.13 to 0.14, indicating rubric insensitivity for GPT-5.2 Pro.
  • Pedagogical alignment: Models frequently retrieve advanced machinery or hallucinate constraints instead of constructing proofs from undergraduate definitions.Examples include assuming an arbitrary graph is finite to terminate an induction and receiving credit for persuasive structure despite broken dependencies.
  • Constraint violations: Human experts found a wider penalty gap than automated judges when stricter Course-Specific rubrics penalized advanced theorems without derivation.Solver-model scores still declined universally under the stricter rubric, including Gemini 3.0 Pro from 0.957 to 0.926 and Claude Sonnet 4.5 from 0.883 to 0.866.

5. Discussion

The discussion argues that QEDBENCH exposes domain-dependent reasoning and judge-alignment failures that prompt engineering alone does not resolve. It also states important scope limitations concerning ground truth, language, proof diversity, and rubric construction.

  • Domain dependence: Near-perfect ODE performance contrasted with combinatorics collapse indicates that mathematical reasoning is not monolithic.The paper characterizes this contrast as template retrieval in continuous domains versus constructive state search in finite structures.
  • Evaluator failure: 74.8% Leniency Rate for Llama 4 Maverick and 38.0% for GPT-5.2 Pro expose the Sycophancy Trap in proof evaluation.The paper uses this term for rewarding authoritative-looking LATEX structure despite broken logical dependencies.
  • Rubric engineering: Rubric Insensitivity limits prompt engineering as a sufficient fix because evaluation behavior is bounded by internal representations of mathematical rigor.The discussion points instead toward process supervision or fine-tuning as future improvement directions.
  • Limitations: The study uses static expert ground truth, focuses on English-language reasoning, and may undercount valid non-standard proofs.Human rubric revision and regression analysis found only negligible same-family self-preference effects.

6. Conclusion

QEDBENCH identifies verification, rather than generation, as the bottleneck in automated reasoning and releases a benchmark for studying evaluator alignment. Its materials combine university-level proofs, problems, and expert annotations.

  • Core conclusion: Verification, rather than generation, is the bottleneck in automated reasoning according to QEDBENCH.The benchmark shows that LLM-as-a-Judge systems can reward rigorous-looking setups without complete logical deduction.
  • Benchmark release: QEDBENCH comprises 1,300+ university-level proofs, 272 upper undergraduate/early graduate-level problems, and expert groundtruth annotations.The released benchmark is intended to support alignment research on automated judges.

Impact Statement

The impact statement frames QEDBENCH as a tool for making mathematical benchmarking more trustworthy by exposing evaluator failure modes. It also highlights risks from deploying insufficiently validated judges in high-stakes educational decisions.

  • Positive impact: QEDBENCH’s primary positive impact is exposing evaluator failures that can reward persuasive but incorrect mathematical reasoning.The paper presents this exposure as a way to make mathematical benchmarking more trustworthy.
  • Potential risks: Automated judges pose risks in high-stakes educational decisions before sufficient validation.The paper argues for expert oversight and transparent rubrics in such deployments.
  • Benchmark scope: The benchmark draws problems from rigorous mathematical literature and course materials spanning analysis, algorithms, algebra, number theory, discrete mathematics, graph theory, probability, and differential equations.The listed source areas establish the breadth of the curated problem collection.
  • Evaluation design: A pilot study found linguistically coherent solutions often failed on subtle edge cases, supporting expert-refined rubrics over simple binary grading.Early-access models were evaluated by human experts before the large-scale 7 × 5 evaluation.

A.3. Automated Evaluation Pipeline

The pipeline preprocesses model outputs, injects problem-specific rubrics into deterministic two-step judging prompts, and checks contamination against exact or equivalent online solutions. Human expert rubrics then calibrate judge behavior against proof-quality standards.

  • Preprocessing: The evaluation script strips markdown wrappers and manually repairs malformed LATEX before judging.These steps isolate raw LATEX and ensure compatibility with standard compilers.
  • Rubric-conditioned judging: Judges receive the problem rubric and solver output, return a numerical score as JSON, then generate a separate plain-text justification.The two-step design separates scoring from post-hoc rationalization.
  • Contamination detection: The contamination check searches for exact or equivalent solutions, requiring matching mathematical objects, parameters, and constraints.Analogous, special-case, more-general, or merely similar problems do not count as contamination.
  • Contamination detection: The contamination agent must verify problem identity or faithful rephrasing, report notation mappings when needed, and return structured JSON with match and source fields.The system prompt directs comprehensive searches across papers, textbooks, lecture notes, forums, repositories, and archives.
  • Human ground truth: Expert evaluation uses rubrics that distinguish course-specific pedagogical compliance from expert-level logical correctness.The course-specific rubric penalizes advanced machinery, while the expert-domain rubric permits trivial implicit steps for specialists.
  • Rubric example: For the graph-path problem, a complete proof maintains reachable sets of size at least n/2 using expansion and inclusion–exclusion, then reconstructs a path by backtracking.The key bound is |U_i+1| ≥ (n/2 + αn) + (1 −α)n −n = n/2.
  • Rubric example: The rubric scores minor omissions below full credit but treats failed invariants, unjustified greedy steps, and major conceptual gaps as substantive errors.Examples include omitting α ≤1/2, mishandling rounding, or applying expansion to sets of unsupported sizes.
  • Calibration findings: Same-family effects are negligible after controls, while critique-enabled judges can identify flaws yet still assign passing or overly generous scores.The largest same-family effect is Gemini’s +0.0332, and the observed failure is interpreted as calibration and decision alignment rather than absent reasoning space.

F.4. Formatting and Proof-by-Intimidation Bias

The study tests whether judges reward mathematical presentation independently of correctness and reports formatting susceptibility, deterministic grade inflation, and boundaries of formal verification and benchmark scale.

  • F.4. Formatting and Proof-by-Intimidation Bias: LATEX density is used as a proxy for visual mathematical complexity that can make broken reasoning appear rigorous.The analysis correlates proof length and LATEX density with assigned judge scores.
  • F.4. Formatting and Proof-by-Intimidation Bias: Table 3 encodes correlations between LATEX density and evaluator scores; positive values indicate susceptibility to proof-by-intimidation.The table’s stated comparison concerns formatting density versus assigned scores.
  • F.4. Formatting and Proof-by-Intimidation Bias: Qwen 2.5 Max and Llama 4 Maverick show positive formatting correlations, whereas GPT-5.2 Pro has a slight negative, statistically nonsignificant correlation.The pattern supports greater susceptibility for the former judges and greater robustness for GPT-5.2 Pro.
  • F.5. Calibration Settings: The benchmark uses deterministic temperature T = 0.0 judging without stochastic self-consistency or sampling-based calibration.Grade inflation persists under deterministic, rubric-conditioned, and binary prompts.
  • F.6. Formal Verification and Symbolic Checking: Lean 4 formal verification was considered but can reward proofs of mismatched statements and shift evaluation toward Lean programming proficiency.These confounds motivate expert human annotation as the current benchmark’s ground truth.
  • F.7. Benchmark Scale: QEDBENCH is smaller than short-answer datasets because specialist annotation is costly, but it contributes 272 proof problems and more than 1,300 generated proofs.It also includes expert scores, qualitative error annotations, and 7 × 5 multi-rubric judge evaluations.

G. Evaluator Bias: Pass Rate Analysis

Pass-rate analysis compares automated and human acceptance at a score threshold and finds domain-dependent inflation, especially persistent leniency in discrete subjects.

  • Binary pass-rate analysis: Pass-rate bias is defined as Δ = Pass Rate_AI − Pass Rate_Human, complementing average-score bias with a binary measure.The threshold for a passing score is ≥0.9.
  • Domain patterns: Discrete domains show positive pass-rate inflation, while continuous analysis domains show stronger punitive bias for some evaluators.The heatmap compares evaluator and human pass rates across domains.
  • Domain patterns: Llama 4 Maverick remains consistently lenient in combinatorial subjects, confirming that the alignment gap is not an artifact of partial-credit scoring.The same pattern appears under strict binary acceptance or rejection.

H. Evaluator Strictness: Average Score Analysis

Average-score and course-specific analyses reveal widespread grade inflation, persistent discrete-domain leniency, and uneven adaptation to explicit pedagogical constraints across judges.

  • Average-score analysis: 0.795 is the human expert consensus baseline for average scores, against which seven automated judges are compared.Average-score analysis captures partial-credit nuance beyond binary pass rates.
  • Average-score analysis: 0.901 is Llama 4 Maverick’s average score, a +0.106 bias over the human baseline and the largest observed inflation.The paper associates this behavior with rewarding superficial plausibility over logical rigor.
  • Average-score analysis: 0.878 and 0.855 are the average scores assigned by Qwen 2.5 Max and Gemini 3.0 Pro, respectively, indicating moderate inflation.Both scores exceed the human consensus baseline.
  • Average-score analysis: 0.830 is GPT-5.2 Pro’s average score, corresponding to a +0.035 bias and the closest alignment with human ground truth.The study therefore uses GPT-5.2 Pro as the primary filter for larger-scale benchmarks.
  • Course-specific rubric: The course-specific rubric penalizes advanced machinery and enforces undergraduate pedagogical boundaries when computing score and pass-rate heatmaps.Figures 9 and 10 compare these constrained results with expert-rubric analyses.
  • Course-specific rubric: Llama 4 Maverick and Qwen 2.5 Max retain nearly identical leniency in discrete domains under both rubrics, indicating rubric insensitivity.Their plausible-sounding structural reasoning continues to receive excessive credit despite stricter instructions.
  • Course-specific rubric: DeepSeek-V3 and GPT-5.2 Pro become more punitive in continuous domains, consistent with operationalizing restrictions on advanced machinery.The shift can bring them closer to, or beyond, human strictness on pedagogical compliance.
  • Reliability metrics: 16.1% is DeepSeek-V3’s Course-Specific Harshness Rate, up from 12.3%, while Llama 4 Maverick’s Leniency Rate remains 72.1%.GPT-5.2 Pro reaches a 34.4% Leniency Rate and 11.0% Harshness Rate under the constrained rubric.

K. Distributional Analysis of Judge Alignment

Density-weighted comparisons show that frontier judges remain largely insensitive to rubric changes, with evaluator behavior dominated by internal scoring priors. Llama 4 Maverick is the clearest grade-inflation outlier, while GPT-5.2 Pro remains comparatively aligned.

  • Rubric Insensitivity: Every major model decreased its Pearson correlation when switching from the Expert to the Course-Specific rubric.The comparison is described as a uniform regression in alignment under stricter pedagogical constraints.
  • Llama Anomaly: r ≈0.50 is Llama 4 Maverick’s lowest-cohort correlation, with scores concentrated above the human-consensus diagonal.The distribution indicates systematic rewards for solutions that human experts reject.
  • Judge Stability: GPT-5.2 Pro maintains robust alignment at r = 0.67 under the Course-Specific rubric.Its score for Gemini 3.0 Pro decreases only slightly, from 0.93 under the Expert rubric to 0.91 under the Course-Specific rubric.
  • Heatmap Evidence: The two rubric conditions produce largely invariant average-score heatmaps, despite explicit penalties for advanced machinery.The patterns support the conclusion that internal scoring priors dominate prompt-specific constraints.
  • Pass-Rate Dynamics: Evaluator choice can dramatically change a solver’s apparent competency, supporting ensemble judging rather than reliance on one LLM judge.The structural similarity between rubric-specific pass-rate matrices also supports rubric insensitivity.

L.2. Data Contamination Analysis

QEDBENCH’s contamination analysis finds no statistically significant performance advantage for problems with online solutions. Aggregate and per-model comparisons remain consistent with parity rather than systematic memorization effects.

  • Dataset Split: 214 problems received high-confidence availability annotations: 88 had online solutions and 126 did not.The annotations were obtained by searching the public internet with o3-deep-research.
  • Aggregate Comparison: The online-minus-offline mean-score gap is +0.017, while the corresponding pass-rate gap is +0.011.The online group exhibited only marginally higher performance on both measures.
  • Aggregate Comparison: Neither mean scores nor strict pass rates differ significantly between problems with and without online solutions.Table 4 aggregates the comparison across all five solvers and 1,070 model-problem pairs.
  • Per-Model Analysis: No individual solver shows statistically significant performance deviance across the availability split.DeepSeek-Prover-V2 has the largest positive gap, +0.067, but it remains within statistical noise with p = 0.18.
  • Conclusion: QEDBENCH shows no statistically significant evidence that data contamination is a primary driver of benchmark performance.The benchmark’s extended reasoning requirements and expert rubrics are presented as design features supporting this robustness.

M. Data Contamination Category-Level Breakdown

Category-level analyses find no consistent online advantage: apparent gaps fluctuate across categories and models, while well-sampled categories approach parity. The same breakdown also contextualizes broader evaluator failures involving structural proof reasoning.

  • Sampling Variance: Complex Analysis shows a +0.17 gap and Discrete Math a +0.10 gap, but small within-category samples limit their interpretation.The Complex Analysis comparison contains only 4 online and 2 offline problems.
  • Category-Level Contamination: Category-level online-minus-offline gaps oscillate in sign across models and categories rather than forming a uniform contamination pattern.The observed stochastic sign pattern is attributed to baseline difficulty variance and sampling noise.
  • Sampling Variance: The observed category-gap variance is 0.011, close to the expected structural noise of 0.006 given σ ≈0.28.In Abstract Algebra, with 21 online and 20 offline problems, the gap is only +0.009.
  • Human Rigor: Human evaluators penalize structural logical flaws, circular reasoning, and unstated assumptions that compromise proof generality.Their evaluations treat a failed core premise as invalidating the proof.
  • Per-Category Breakdown: Figure 19 shows no consistent online advantage within any single category across solver models.Where one model performs better online, sibling models often show parity or the reverse pattern.
  • LLM Leniency: LLM judges can identify local errors yet detach them from global scoring, awarding generous partial credit for mathematically coherent but irrelevant or incomplete work.This behavior is illustrated by lenient scoring of a proof that failed its primary objective.

N.2. The LLM Sycophancy Trap: Rewarding Empty and Irrelevant Proofs

The qualitative analysis identifies a sycophancy trap in which LLM judges reward authoritative-looking or logically coherent text despite fatal errors, irrelevance, impossible constructions, or false premises. Human evaluation instead tracks the complete logical dependency from hypotheses to conclusions.

  • Concept: The Sycophancy Trap is evaluators’ systematic reward of authoritative-sounding formatting and plausible structure despite catastrophic logical flaws.The paper distinguishes this mathematical-evaluation usage from the broader alignment-literature meaning of sycophancy.
  • Irrelevant Proofs: LLM judges routinely award partial credit to irrelevant proofs, while human experts assign 0.0 to mathematically rigorous solutions addressing another theorem.An unrelated NP-hardness reduction received 0.25/1.0 from GPT-5.2 Pro.
  • Prompt Compliance: LLM judges penalize mathematically correct corrections to false premises because they prioritize satisfying the stated task over rejecting an invalid equivalence.DeepSeek-V3 awarded 0.75/1.0 despite acknowledging a valid counterexample to one requested direction.
  • False Theorems: Nearly every frontier judge awarded 0.9/1.0 to hallucinated proofs of a false Abstract Algebra statement that human evaluators scored 0.0.The example involved falsely treating K[x, y] as a principal ideal domain.
  • Impossible Constructions: Llama 4 Maverick awarded 0.9/1.0 to an impossible Venn-diagram construction, despite the cited impossibility theorem.Gemini 3.0 Pro Preview recognized the impossibility but still assigned 0.5/1.0.
  • Evaluation Architectures: The gap reflects different reasoning architectures: humans trace unbroken logical implication, whereas current LLM judges decouple local coherence from global validity.The paper concludes that global dependency tracking and objective mathematical correctness remain unresolved requirements for autonomous judging.

O. Detailed Leniency Distribution Analysis

Figure 20 compares AI judges’ verdicts with human evaluations, distinguishing strict, lenient, and agreeing judgments. The distribution highlights excessive leniency in Llama 4 Maverick, strictness in DeepSeek-V3, and strong balance in GPT-5.2 Pro.

  • Verdict Classification: AI verdicts are classified as Strict when lower than human scores, Lenient when higher, or Agree when they match exactly.The analysis compares each AI judge’s score directly with the corresponding human expert score.
  • Judge Distributions: Llama 4 Maverick is excessively lenient across the evaluated solutions.Its grading distribution is described as heavily favoring lenient verdicts.
  • Judge Distributions: DeepSeek-V3 diverges toward strictness in its grading verdict distribution.Its distribution contrasts with Llama 4 Maverick’s leniency.
  • Judge Distributions: GPT-5.2 Pro achieves the best balance of low leniency and high agreement with human experts.The figure identifies this balance as the strongest alignment pattern among the compared judges.
  • Interpretation: The distribution illustrates a “Sycophancy Trap” in which helpfulness-optimized models default to leniency on dense mathematical reasoning.The paper contrasts Llama 4 Maverick’s leniency with higher agreement from GPT-5.2 Pro, Gemini 3 Pro, and Claude Opus 4.5.

P.1. The “Fake Citation & Fabricated Construction” Trap

Across several university-level proof problems, models produced plausible but invalid arguments by fabricating constructions, ignoring assumptions, or forcing false conclusions. Human evaluations identified recurring failures involving hallucinated references, unsupported generality, and unresolved logical gaps.

  • Fabricated citations and constructions: Models fabricated plausible-sounding references and constructions when they lacked a valid textbook template or proof strategy.Human evaluators described hallucinated papers, impossible constructions, and fabricated proofs in multiple difficult problems.
  • Hidden assumptions in graph proofs: Models memorized planar-duality templates but ignored connectivity requirements and silently assumed graph finiteness.Human evaluations penalized proofs that added finiteness assumptions or failed to establish the required properties for plane duals.
  • Premise contamination: Several models assumed the Prime Number Theorem despite a problem requirement forbidding it, effectively embedding the desired conclusion in the premises.Human evaluators scored GPT-5 Pro and Claude Sonnet 4.5 down for relying on PNT when the problem explicitly indicated it should not be assumed.
  • Hallucinated technical machinery: In constructive and discrete arguments, models replaced missing reasoning with hallucinated probability theorems, false inequalities, or dense algebraic relationships.These failures appeared in Cover Times, traversal sequences, regular-graph counting, and other discrete proof tasks.
  • Unresolved proof execution: Models often exposed incomplete reasoning through invalid self-corrections, unhandled cases, or unsupported assertions that the requested theorem had been proved.A human evaluator noted that Claude Sonnet 4.5 never addressed q < p before jumping to a conclusion in an Lp construction problem.
  • Failure to challenge false premises: Models also attempted to prove mathematically false statements instead of detecting the contradiction or supplying a counterexample.Examples included false MST implications, invalid algebraic claims about K[x, y], and unsupported structural arguments.
  • Local rigor gaps: Even when broad proof structures were correct, evaluations identified missing justifications for isomorphisms, notation, semidirect-product conclusions, and other local deductions.These omissions reduced scores despite substantial correct structure in the surrounding arguments.
  • Local rigor gaps: A group-theoretic proof received 0.5 because it lacked the conditions needed to conclude an internal semidirect product and omitted details in several cases.The evaluation specifically noted the need to establish G = PQ and P ∩ Q = {1}, alongside clearer case analysis.
Loading 2602.20629v3…