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 advanced mathematical proofs remains poorly aligned with expert judgment, despite strong performance on elementary benchmarks. QEDBench audits this gap across university-level proof generation and judging, finding near-perfect performance in ODEs but collapse in Combinatorics and a 74.8% leniency rate for Llama 4 Maverick.

  • Problem

    Existing scalable LLM-as-a-Judge protocols correlate poorly with expert judgment on upper-undergraduate to early-graduate mathematical proofs.

    Source: §1 · pp. 1–2

  • Method

    QEDBench combines 272 expert-curated problems, more than 1,300 generated proofs, tiered expert rubrics, and a cross-model evaluation matrix across ten mathematical disciplines.

    Source: §1 · p. 2, §3 · p. 4

  • Results

    Near-perfect performance in ODEs contrasts with collapse in Combinatorics, while Llama 4 Maverick shows a 74.8% Leniency Rate.

    Source: §5 · p. 9

  • Takeaways & Limitations

    The paper argues that improving automated mathematical evaluation requires process supervision and adversarial training rather than relying solely on standard judging pipelines.

    Source: §6 · p. 9

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

    Source: §5 · p. 9

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 audits both university-level mathematical proof generation and the reliability of LLM judges against PhD-level human evaluation. It reveals systematic judge score inflation and substantial domain-dependent differences in frontier-model proof performance.

1. Introduction

  • QEDBENCH introduces a dual-rubric benchmark spanning ten upper-undergraduate and early-graduate mathematical disciplines to separately audit proof generation and judging.The benchmark covers Analysis, Complex Analysis, Abstract Algebra, Discrete Math, Probability Theory, ODEs, Number Theory, Combinatorics, Algorithms, and Graph Theory.Source: §1 · p. 2
  • Five frontier models generated candidate proofs, using model-specific token limits, 2,000-second streaming timeouts, up to three retries, and a default score of 0 after persistent failure.The evaluated generators were o3-deep-research, GPT-5 Pro, Claude Sonnet 4.5, Gemini 3.0 Pro, and DeepSeek-Prover-V2.Source: §1 · p. 2
  • Seven judge models graded proofs under course-specific and expert-domain rubrics, enabling comparison of automated scores with human ground truth and isolation of systemic judge bias.Course-specific rubrics emphasize textbook definitions, whereas expert-domain rubrics permit trivial implicit steps while requiring logical soundness.Source: §1 · p. 2

1.1. Key Contributions

  • +0.18 mean score inflation is observed for Claude Opus 4.5, while Llama 4 Maverick reaches a 90.2% pass rate versus a 67.7% human baseline.These results demonstrate systematic positive bias among automated judges relative to human experts.Source: §1.1 · p. 2
  • 0.91 raw score makes Gemini 3.0 Pro the top overall performer, while Claude Sonnet 4.5 ranges from a 100% ODE pass rate to 27.3% in Combinatorics.The calibrated evaluation exposes a discrete-continuous divide in frontier reasoning performance.Source: §1.1 · p. 3
  • Over 1,000+ hours of PhD-level hand evaluation establish QEDBENCH’s human ground truth, with the full dataset, rubrics, and evaluation logs publicly released.The release is intended to support benchmarking future AI judges against verified expert evaluations.Source: §1.1 · p. 3

2. Related Work

Prior benchmarks advance mathematical reasoning evaluation from foundational tasks toward expert-level and university-level settings, but trade off difficulty, scale, and evaluation fidelity. QEDBENCH targets upper-undergraduate/early-graduate full-text proofs and exposes an Alignment Gap showing that solving proficiency does not guarantee grading reliability.

Benchmarking the Reasoning Frontier

  • Prior benchmarks span foundational arithmetic, expert-level problems, university evaluation, contamination-resistant updates, and specialized reasoning dimensions, but differ in scale and proof-evaluation format.FrontierMath uses closed-form answers, IMProofBench covers approximately 39 research-generation problems, and LiveBench evaluates proofs through cloze-style reordering rather than open-ended generation.Source: §2 · p. 3
  • QEDBENCH targets upper-undergraduate/early-graduate proofs, prioritizing semantic quality and verifiability over binary answer matching or novel-research difficulty.It occupies a middle ground between high-school competitions and research-level benchmarks, emphasizing full-text proof evaluation.Source: §2 · p. 3

The Challenge of Automated Evaluation

  • Existing studies find that LLM judges can correlate with human evaluators on Olympiad proofs, yet often overestimate quality, favor superficial plausibility and style, and exhibit generator-style bias.ProofBench and RefGrader report promising fine-grained or agentic evaluation, while human-evaluation and audit studies identify stylistic and authoritative-writing heuristics.Source: §2 · p. 3
  • QEDBENCH extends scrutiny of reasoning stability to rigorous theorem proving, while revealing an Alignment Gap in frontier-model grading beyond rigid competition rubrics.Unlike Ma et al. (2025), which fine-tunes judges on competition data, QEDBENCH evaluates inherent alignment and finds that Claude Opus 4.5 may reward persuasive but logically unsound language.Source: §2 · p. 3

3. QEDBENCH Methods

QEDBENCH combines adversarially curated university-level proof problems, expert tiered grading, dual rubrics, and a fully crossed 7 × 5 evaluator-solver matrix. This design measures alignment gaps while separating judge bias from solver skill.

3. QEDBENCH Methods

  • QEDBENCH contains 272 expert-curated problems across ten mathematical domains and more than 1,300 generated proofs scored by experts and LLM judges.Its methodology rests on adversarial data curation, tiered-rubric expert evaluation, and cross-model evaluation.Source: §3 · p. 4

3.1. Problem Curation and Anti-Leakage

  • A three-stage curation pipeline used diverse authoritative sources, manual syntactic rewording, and adversarial web audits to reduce contamination and memorization.The audit distinguished equivalent solutions as contamination from merely analogous problems as acceptable domain overlap.Source: §3.1 · p. 4

3.2. Expert Evaluator Selection

  • Forty-eight qualified experts produced 1,000+ hours of grading, with domain matching, independent double evaluation when possible, and third-expert adjudication.The tiered scale [0, 0.25, 0.5, 0.75, 0.9, 1.0] distinguishes fundamental logical failures from expository oversights and credits any logically complete proof.Source: §3.2 · p. 4

3.3. The Evaluation Alignment Gap: Dual-Rubric Strategy

  • The Alignment Gap is defined as the discrepancy between LLM-judge scores and human ground truth, isolated through course-specific and research-calibrated expert rubrics.Humans used the Expert Rubric, while LLM judges used both; human experts refined drafts initially synthesized by GPT-5.2 Pro and verified by Gemini 3.0 Pro.Source: §3.3 · p. 4

3.4. Evaluation Framework

  • A deterministic 7 × 5 evaluator-solver matrix crossed five frontier solvers with seven judge models under both rubrics to isolate judge bias from solver skill.All automated evaluations used temperature T = 0.0 for reproducibility, with judges spanning GPT, Claude, Gemini, Grok, Qwen, DeepSeek, and Llama families.Source: §3.4 · pp. 4–5

4. Results

Expert evaluation shows strong frontier-model performance on procedural mathematics but substantial weaknesses in constructive discrete reasoning, while automated judges exhibit domain-dependent misalignment with human experts. Partial-credit scores further reveal plausible but logically incomplete proofs that binary pass rates can obscure.

4.1. Frontier Model Performance

  • Gemini 3.0 Pro leads overall with an 86.4% pass rate and 0.91 average score, followed by GPT-5 Pro at 76.8% and 0.84.Source: §4.1 · p. 5

4.1.1. KEY OBSERVATIONS AND ANALYSIS

  • Gemini 3.0 Pro and Claude Sonnet 4.5 reached 100.0% pass rates in ODEs, whereas Combinatorics pass rates fell to 9.1% for DeepSeek-Prover-V2 and 27.3% for Claude Sonnet 4.5.The results associate procedural, calculation-heavy domains with near-saturation and constructive object-generation tasks with high failure rates.Source: §4.1.1 · p. 5, Figure 1 · p. 5
  • Gemini 3.0 Pro achieved an 89.5% Graph Theory pass rate, outperforming Claude Sonnet 4.5 at 15.8% and o3-deep-research at 42.1%, despite Combinatorics being its weakest area at 72.7%.This contrast indicates that discrete-reasoning performance varies substantially across related subfields rather than reflecting a uniform capability.Source: §4.1.1 · pp. 5–6
  • Average scores can reach approximately 0.88 in Analysis despite lower pass rates, reflecting structurally sound but subtly invalid proofs that often score around 0.75.Binary correctness rewards could therefore miss partial understanding and reinforce superficially rigorous reasoning instead of correcting logical gaps.Source: §4.1.1 · p. 6, Figure 2 · p. 6

4.2. Evaluation Alignment: Human Experts and LLMs

  • Human experts set a 67.7% baseline pass rate; Llama 4 Maverick passed 90.2%, while DeepSeek-V3 aligned most closely at 72.2%, followed by GPT-5.2 Pro at 74.1%.Llama’s inflation was attributed to approving surface-level coherence despite subtle logical gaps.Source: §4.2 · p. 6, Figure 3 · p. 6
  • In Combinatorics, Llama 4 Maverick showed +0.36 bias and Qwen 2.5 Max +0.30, indicating AI leniency toward discrete proofs that appear rigorous despite errors.Source: §4.2 · pp. 6–7, Figure 4 · p. 7
  • In Complex Analysis, DeepSeek-V3 and Grok 4 showed punitive biases of -0.14 and -0.15, while Gemini 3 Pro and Grok 4 showed -0.05 and -0.07 in Algorithms.The results attribute this harshness to penalizing implicit expert steps or correct pseudocode that differs from learned templates.Source: §4.2 · p. 7, Figure 4 · p. 7
  • GPT-5.2 Pro most closely matched human evaluators across the widest range of domains, showing that alignment requires field-specific calibration rather than uniform strictness.Source: §4.2 · p. 7

3. Decomposing Error Modes: Leniency vs. Rigidity.

Automated proof evaluators exhibit asymmetric failure modes, with severe leniency and rigidity persisting even for the strongest judge. Rubric constraints also have limited effect, while solver models frequently violate pedagogical requirements by substituting advanced machinery for constructive reasoning.

3. Decomposing Error Modes: Leniency vs. Rigidity.

  • 74.8% Leniency Rate makes Llama 4 Maverick approve nearly three-quarters of logically flawed proofs, reflecting over-reliance on instruction-template matching.Jain et al. (2025) similarly reported True Positive Rate > 96% but True Negative Rate < 25%, characterizing this pattern as “Agreeableness Bias.”Source: §3 · p. 7
  • 12.3% Harshness Rate makes DeepSeek-V3 the strictest auditor, while its 39.6% Leniency Rate indicates difficulty generalizing beyond standard proof templates.These reliability metrics use binary pass rates, counting scores ≥0.9 as passes rather than measuring average score deltas.Source: §3 · p. 7
  • 38.0% Leniency Rate remains for GPT-5.2 Pro, showing that even the strongest evaluator struggles to align reliably with human mathematical judgment.The analysis separates false positives, or hallucinated rigor, from false negatives, or harshness.Source: §3 · pp. 7–8

4.3. Ablation Study: The Limits of Rubric Engineering

  • r ≈0.69 remains virtually unchanged across Expert and Course-Specific rubrics, indicating that added constraints do not materially improve GPT-5.2 Pro’s alignment.Figure 6 compares correlation bubble plots under both rubrics and attributes the stability to internal priors dominating prompt specificity.Source: Figure 6 · p. 8, §4.3 · p. 8
  • Pearson correlation changes only from r = 0.69 to r = 0.67, while MAE changes from 0.13 to 0.14 between Expert and Course-Specific rubrics.The corresponding correlation drop is −0.02 and error increase is +0.01, with average deviation from expert consensus of approximately 13%.Source: §4.3 · p. 8

4.4. The Knowledge Gap: Adherence to Pedagogical Constraints

  • Under strict Course-Specific evaluation, solvers repeatedly retrieve advanced theorems or hallucinate assumptions instead of constructing proofs from required undergraduate definitions.Examples include assuming graph finiteness in Algorithms and bypassing connectivity and bijection requirements in Graph Theory.Source: §4.4 · pp. 8–9
  • 0.957 to 0.926 and 0.883 to 0.866 are the score declines for Gemini 3.0 Pro and Claude Sonnet 4.5 under the stricter rubric.Human evaluators imposed much larger penalties, typically 0.5 to 0.75 points, for hand-waved derivations or assumed finiteness, whereas LLM judges remained lenient.Source: §4.4 · p. 9
  • Human graders penalize broken dependencies, missing assumptions, false premises, and irrelevant proofs, while LLM judges often reward persuasive structure or prompt compliance.The findings characterize current models primarily as retrieval engines and bounded-definition mathematical reasoning as an open problem.Source: §4.4 · p. 9

5. Discussion

The discussion identifies domain-dependent reasoning failures, evaluator sycophancy, and rubric insensitivity as systemic limitations of LLM-based mathematical proof evaluation. It also qualifies these findings through study limitations and negligible detected self-preference effects.

Core findings

  • Near-perfect ODE performance contrasts with collapse in Combinatorics, indicating that mathematical reasoning is not monolithic: models retrieve continuous-domain templates but struggle with finite-structure state search.The results decouple generation from verification to audit the LLM-as-a-Judge paradigm and expose limitations in frontier reasoning and alignment.Source: §5 · p. 9

The Sycophancy Trap

  • 74.8% Leniency Rate for Llama 4 Maverick and 38.0% for GPT-5.2 Pro reveal a Sycophancy Trap in which judges reward authoritative-looking LATEX despite broken logical dependencies.The pattern shows that subtle graduate-level proof gaps remain difficult for current automated evaluators.Source: §5 · p. 9

Rubric Insensitivity

  • Weak effects from pedagogical constraints support Rubric Insensitivity, suggesting evaluation behavior depends on internal representations of mathematical rigor rather than context-window instructions alone.This aligns with evidence that human-LLM alignment varies across rubric formats (Li et al., 2026) and that judges fail on problems beyond their solving capability (Krumdick et al., 2025).Source: §5 · p. 9

Limitations

  • The study uses static expert ground truth, English-language reasoning, and multi-expert adjudication that may still undercount valid non-standard proofs, while same-family regression finds negligible self-preference effects.GPT-5.2 Pro helped synthesize rubric drafts, but human experts iteratively modified them.Source: §5 · p. 9

6. Conclusion

QEDBENCH shows that automated reasoning is now bottlenecked by verification: LLM judges can reward rigorous-looking proof setups despite incomplete deduction. It releases a benchmark to support process supervision, adversarial training, and alignment research.

Conclusion

  • QEDBENCH shows that automated reasoning has shifted from generation to verification, where standard LLM judges may reward rigorous-looking setups without complete logical deduction.The benchmark motivates moving toward process supervision and adversarial training.Source: §6 · p. 9
  • QEDBENCH releases 1,300+ university-level proofs, 272 upper undergraduate/early graduate-level problems, and expert groundtruth annotations for alignment research.The release is intended to support the next generation of automated-evaluation research.Source: §6 · p. 9

Impact Statement … A.2. Prompting Templates

QEDBENCH aims to make university-level mathematical proof evaluation more trustworthy by exposing automated-judge failures and calibrating them against expert human assessment. The supplementary materials document broad source coverage, pilot calibration, and rigor-oriented prompting procedures.

Impact Statement

  • The benchmark’s positive impact is exposing evaluator failures that may reward persuasive but incorrect reasoning, while cautioning against high-stakes deployment without expert oversight, transparent rubrics, and human calibration.Automated judges may be misused in educational decisions before sufficient validation.Source: Impact Statement · p. 10

A. Expanded Source List

  • QEDBENCH problems were curated from rigorous literature and course materials spanning analysis, algorithms, algebra, number theory, discrete mathematics, graph theory, probability, and differential equations.The source list includes works by Douglass, Beals, Stein and Shakarchi, Motwani and Raghavan, Erickson, Dummit and Foote, Shoup, Niven et al., Ireland and Rosen, Matoušek and Nešetřil, Diestel, Graham et al., Sane, Klenke, Capiński and Zastawniak, Coddington, and Teschl.Source: A. Expanded Source List · p. 13

A.1. Preliminary Human-Model Alignment Study

  • The pilot study calibrated benchmark difficulty before the 7 × 5 evaluation by testing early-access models with human experts on binary correctness.Models often produced coherent mathematical prose but failed on subtle edge cases.Source: §A.1 · p. 13
  • Pilot findings motivated the Expert-Refined Rubric because simple binary grading was insufficient for detecting subtle mathematical failures.The study confirmed that linguistic coherence does not reliably indicate proof correctness.Source: §A.1 · p. 13

A.2. Prompting Templates

  • The primary solver prompt used a tenured-mathematics-professor persona, targeted advanced undergraduates, demanded elimination of logical mistakes, and required rigorous LATEX proofs.Persona-based prompting was intended to elicit maximum rigor.Source: §A.2 · p. 13
  • For search-capable models such as o3-deep-research, the modified prompt encouraged web-based verification of lemmas before incorporating them into the final proof.This procedure added active lemma checking to the standard proof-generation prompt.Source: §A.2 · p. 13

A.3. Automated Evaluation Pipeline … F.3. Score Discretization and Binary Classification

This section details the automated proof-evaluation pipeline, including rubric-conditioned scoring, justification generation, contamination checks, and score discretization. It also defines expert and course-specific grading criteria, human evaluation standards, and robustness analyses addressing alternative proofs, self-preference, and score granularity.

A.3. Automated Evaluation Pipeline

  • The pipeline extracts raw LATEX, manually sanitizes malformed code, then separates numerical scoring from post-hoc justification through two-step JSON and plain-text prompting.Evaluators receive the problem-specific rubric and solver output, return only a numerical score, and subsequently justify that score.Source: §A.3 · p. 13

B. Checking Solutions Online o3-deep-research Prompt

  • The contamination check combines manual verification with o3-deep-research web scanning, accepting only exact or mathematically equivalent complete solutions while rejecting merely analogous, special-case, or similar problems.The agent must verify problem equivalence, map rephrased notation, and return structured JSON with the source and brief evidence.Source: B. Checking Solutions Online… · pp. 13–14

C. Full Expert Evaluation Tiered Rubric; D. Example Full Rubrics

  • The benchmark supplies both expert-correctness and course-specific rubrics to distinguish domain-valid proofs from solutions satisfying course-level methods and constraints.The examples explicitly illustrate the difference between correctness based on expert knowledge and evaluation against course-specific requirements.Source: C. Full Expert Evaluation Tiered Rubric · p. 14, D. Example Full Rubrics · p. 14

D.1.2. EXPERT CORRECTNESS RUBRIC

  • For the graph problem, a fully correct proof defines reachable layers, preserves a size-n/2 invariant by expansion and inclusion–exclusion, and reconstructs the constrained walk by backtracking.The expert rubric requires handling α ≤ 1/2, monotonicity from an n/2-subset, the bound |Ui+1| ≥ n/2, and predecessor selection.Source: §D.1.2 · p. 15

D.1.2. EXPERT CORRECTNESS RUBRIC; 0.25 (Severely Lacking) Major early misunderstanding or gap makes the argument largely unusable.

  • The graph rubric penalizes omissions or errors progressively, from minor rounding or backtracking oversights through flawed counting and induction to unjustified greedy, connectivity, theorem, or expansion arguments.Severe failures include ignoring expansion, treating large sets as sufficient without edge reasoning, using unproven advanced results, or claiming connectivity without a set-based construction.Source: §D.1.2 · pp. 15–16, §0.25 · p. 16

D.2.2. EXPERT CORRECTNESS RUBRIC

  • For alternating permutations and Eulerian numbers, the correctness rubric accepts a sign-reversing involution or generating-function proof only when definitions, parity, cancellation, fixed points, and the final signed identity are rigorously established.The rubric requires the involution to be well-defined and sign-reversing, or the Eulerian-polynomial EGF route to simplify correctly and recover alternating-permutation counts.Source: §D.2.2 · p. 18
  • The expert rubric distinguishes complete, partial, severely lacking, and incorrect proofs using parity, sign factors, fixed-point identification, and justified mathematical steps.It treats unsupported involutions, unjustified theorem use, parity mishandling, and empirical checks without a general argument as substantive deficiencies.Source: §D.2.2 · pp. 19–20

D.2.3. COURSE-SPECIFIC RUBRIC

  • The course-specific rubric requires a rigorous parity-aware connection between the alternating Eulerian sum and alternating permutations, permitting involution, generating-function, or recurrence proofs.Acceptable proofs must define and justify the method, identify fixed points or equivalent generating functions, and verify relevant parity and base cases.Source: §D.2.3 · p. 20

E.1. System Prompts

  • System prompts enforce strict rubric adherence and distinguish course-specific grading, which penalizes unexplained advanced machinery, from expert grading, which allows standard graduate-level theorems.Both modes require a JSON score selected from [0, 0.25, 0.5, 0.75, 0.9, 1.0].Source: §E.1 · p. 21

E.2. User Prompts

  • The user-prompt pipeline separates score generation from justification: Step 1 forces a JSON scalar, while Step 2 requests a post-hoc analytical Chain-of-Thought explanation.A fallback prompt retries malformed outputs by requiring only one number from the permitted score set.Source: §E.2 · p. 22

F.1. Human Grading Protocol and Proof-Style Flexibility

  • Human grading used independent domain experts and adjudication, assessing logical soundness rather than similarity to a reference proof and accepting complete novel or alternative methods.Each problem was assigned to two experts whenever possible, with disagreements resolved by a third expert adjudicator.Source: §F.1 · p. 22

F.2. Same-Family Self-Preference

  • Same-family self-preference was negligible after controlling for proof quality, judge strictness, and difficulty; Gemini showed the largest positive effect at +0.0332.Other model families exhibited near-zero or slightly negative effects, much smaller than the domain-specific leniency patterns.Source: §F.2 · p. 22, Table 2 · p. 23

F.3. Score Discretization and Binary Classification

  • The qualitative leniency pattern persisted under binary Pass/Fail evaluation, showing that grade inflation is not an artifact of partial-credit discretization.Llama 4 Maverick continued accepting proofs that humans rejected when passing required a score of at least 0.9.Source: §F.3 · p. 23
  • Judges often identified mathematical flaws in critique-enabled analyses yet still assigned passing or overly generous scores, indicating calibration and decision-alignment failures.The mismatch persisted even when judges had natural-language reasoning space before or after the discrete decision.Source: §F.3 · p. 23

F.4. Formatting and Proof-by-Intimidation Bias … F.7. Benchmark Scale

The appendix examines formatting bias, deterministic calibration, formal-verification limitations, and QEDBENCH’s scale relative to peer expert-reasoning datasets. It argues that human annotation remains the appropriate ground truth while documenting reproducibility and benchmark-cost constraints.

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

  • Qwen 2.5 Max and Llama 4 Maverick show positive LATEX-density correlations with scores, supporting susceptibility to proof-by-intimidation from dense mathematical formatting.LATEX density proxies visual mathematical complexity, which can appear rigorous even when the logical chain is broken.Source: §F.4 · p. 23, Table 3 · p. 23
  • GPT-5.2 Pro shows a slight negative, statistically non-significant correlation with LATEX density, suggesting greater robustness to superficial presentation.Source: §F.4 · p. 23, Table 3 · p. 23

F.5. Calibration Settings

  • All automated evaluations use temperature T = 0.0 without stochastic self-consistency or sampling-based calibration to ensure deterministic, reproducible judging behavior.Grade inflation persists under deterministic, rubric-conditioned, and binary decision prompts, indicating that simple inference-time calibration is insufficient for the most lenient judges.Source: §F.5 · p. 23

F.6. Formal Verification and Symbolic Checking

  • Expert human annotation is the current ground truth because autoformalization can reward-hack mismatched statements and frontier models often struggle with zero-shot Lean proofs.Formal verification remains a valuable complementary direction, but using it would shift evaluation toward Lean programming proficiency rather than natural-language reasoning and judge alignment.Source: §F.6 · pp. 23–24

F.7. Benchmark Scale

  • QEDBENCH contributes 272 university-level proof problems, more than 1,300 generated proofs, expert scores, qualitative error annotations, and 7 × 5 multi-rubric judge evaluations.Its specialist-annotation setting constrains scale compared with high-school calculation datasets, while peer expert-reasoning datasets typically contain hundreds of examples.Source: §F.7 · p. 24
  • GPQA contains 448 graduate-level science questions with a 198-question Diamond subset, ProofNet contains 371 undergraduate formalization examples, and FrontierMath contains 350 advanced problems.Source: §F.7 · p. 24

G. Evaluator Bias: Pass Rate Analysis

Binary pass-rate analysis confirms that evaluator bias persists beyond partial-credit scoring: AI–human pass-rate differences show leniency in discrete domains and punitive bias in continuous analysis. Llama 4 Maverick remains consistently lenient in combinatorial subjects even when proofs are judged strictly as pass or fail.

Pass Rate Analysis

H. Evaluator Strictness: Average Score Analysis … J. Judge Reliability on Course-Specific Rubrics

Average-score analysis shows widespread evaluator grade inflation, while course-specific constraints expose both successful adaptation by strong logic models and persistent rubric insensitivity in sycophantic judges. GPT-5.2 Pro is the most consistently calibrated evaluator across these analyses.

H.1. Score Inflation Trends

  • 0.901 average score and Δ +0.106 made Llama 4 Maverick the strongest grade inflator, versus the 0.795 human baseline.Figure 8 compares automated judges with the human baseline and shows systematic positive bias across most frontier models.Source: §H.1 · p. 25, Figure 8 · p. 25
  • 0.830 average score and Δ +0.035 made GPT-5.2 Pro the closest evaluator to human consensus and the most calibrated judge.Qwen 2.5 Max and Gemini 3.0 Pro also inflated scores, reaching 0.878 and 0.855 respectively.Source: §H.1 · p. 25, H. Evaluator Strictness: Average Score… · p. 25

I. Evaluator Bias: Course-Specific Rubric Heatmaps

  • Under the Course-Specific Rubric, Figure 9 measures score bias and Figure 10 measures pass-rate bias after imposing pedagogical constraints.The rubric penalizes advanced machinery and enforces course-level pedagogical constraints.Source: §I · p. 25, Figure 9 · p. 26, Figure 10 · p. 27

I.1. Comparing Expert and Course-Specific Bias

  • Llama 4 Maverick and Qwen 2.5 Max retained nearly identical leniency in Combinatorics and Discrete Math under both rubrics, revealing rubric insensitivity.Their over-rewarding of plausible but flawed structural logic persisted despite stricter instructions.Source: §I.1 · p. 28
  • DeepSeek-V3 and GPT-5.2 Pro became more punitive in continuous domains, indicating successful enforcement of constraints against advanced machinery.This behavior aligned with or exceeded human graders’ strictness on pedagogical compliance.Source: Figure 9 · p. 26, §I.1 · p. 28
  • Bias heatmaps remained broadly static across rubrics, showing that domain-specific leniency and strictness cannot be fully corrected through targeted prompting alone.The persistent structure indicates deeply ingrained systemic biases in LLM-as-a-Judge systems.Source: §I.1 · p. 28

J.1. Impact of Pedagogical Constraints on Alignment

  • Under strict pedagogical constraints, DeepSeek-V3’s Harshness Rate rose from 12.3% to 16.1%, while Llama 4 Maverick’s Leniency Rate remained 72.1%.Figure 11 decomposes reliability into Leniency Rate false positives and Harshness Rate false negatives using the score ≥0.9 pass threshold.Source: Figure 11 · p. 28, J. Judge Reliability on… · p. 28, §J.1 · p. 29
  • GPT-5.2 Pro achieved the lowest top-tier Leniency Rate at 34.4% while maintaining an 11.0% Harshness Rate, showing the strongest constrained-rubric calibration.It penalized overly advanced techniques without becoming overly punitive toward valid student derivations.Source: §J.1 · p. 29

K. Distributional Analysis of Judge Alignment · K.1. Systemic Rubric Insensitivity · L. Rubric Insensitivity: Full Heatmap Analysis

Across distributional plots and heatmaps, frontier judges show rubric insensitivity: Course-Specific constraints generally reduce correlation or leave scoring patterns largely unchanged. Llama 4 Maverick exhibits persistent grade inflation, while evaluator choice substantially affects pass-rate judgments and motivates ensembles.

K.1. Systemic Rubric Insensitivity

  • All major models show lower Pearson correlation under the Course-Specific rubric than under the Expert rubric, indicating uniform regression rather than improved alignment.The bubble plots compare score distributions for all seven evaluators under both rubrics.Source: §K.1 · p. 29, Figure 13 · p. 30, Figure 12 · p. 30

K. Distributional Analysis of Judge Alignment

  • The score distributions suggest that judges’ internal priors for mathematical correctness override explicit negative constraints, including instructions to penalize advanced methods.Models default to their internal representation of a good proof even under specific rubric instructions.Source: §K.1 · p. 29

K.1. Systemic Rubric Insensitivity

  • GPT-5.2 Pro remains best calibrated, with r = 0.69 under the Expert rubric and r = 0.67 under the Course-Specific rubric.Its scores cluster most tightly around the y = x diagonal in both visualizations.Source: Figure 12 · p. 30, Figure 13 · p. 30

L. Rubric Insensitivity: Full Heatmap Analysis

  • Figure 14 shows strikingly similar average-score heatmaps under Expert and Course-Specific rubrics, indicating minimal impact from prompt constraints on frontier models’ scoring priors.The heatmaps provide a fully crossed judge–solver comparison across both grading conditions.Source: Figure 14 · p. 31, L. Rubric Insensitivity: Full Heatmap… · p. 31

L.1. Visualizing Resistance to Constraints

  • Llama 4 Maverick remains a high-scoring evaluator across both heatmaps, assigning Gemini 3.0 Pro a near-perfect 0.95 even under penalties for non-standard derivations.Its persistent blue row further supports its classification as a grade inflator.Source: §L.1 · p. 31
  • GPT-5.2 Pro is comparatively stable, lowering its score for Gemini 3.0 Pro only from 0.93 under Expert to 0.91 under Course-Specific evaluation.The heatmap’s overall structure remains largely invariant despite this slight sensitivity.Source: §L.1 · p. 31
  • Fine-grained pass rates vary dramatically with evaluator choice, while similar matrices across rubrics support using multiple LLM judges for aggregate proof analysis.The factorial evaluator–solver matrices reveal that benchmark competency can swing depending on the selected judge.Source: §L.1 · p. 31

L.2. Data Contamination Analysis

QEDBENCH shows no statistically significant evidence that publicly available solutions inflate solver performance, either overall or for any individual model. Its extended-reasoning demands and strict expert rubrics make superficial memorization insufficient, supporting the benchmark’s robustness to contamination.

Overall contamination effect

  • +0.017 mean-score and +0.011 pass-rate gaps favor online-solution problems, but neither difference is statistically significant across 1,070 model–problem pairs.Welch’s t-test gives t = 0.99 and p = 0.32; the Mann–Whitney U test gives p = 0.80 and Cohen’s d = 0.06.Source: Table 4 · p. 33, §L.2 · p. 33

Per-model analysis

  • No individual model shows a statistically significant contamination effect; GPT-5 Pro and o3-deep-research have score gaps of −0.000 and −0.002, while DeepSeek-Prover-V2’s +0.067 gap remains nonsignificant.DeepSeek-Prover-V2’s gap has p = 0.18, below no significance threshold at α = 0.05.Source: Table 5 · p. 33, §L.2 · p. 33

Method

  • The analysis identified online solutions for 88 of 214 problems and no online solutions for 126, comparing human mean scores and strict pass rates across five frontier solvers.The contamination search used o3-deep-research to inspect the public internet for all 272 benchmark problems.Source: §L.2 · p. 33

Interpretation

  • QEDBENCH’s robustness is attributed to problems requiring extended mathematical reasoning and expert rubrics that penalize incomplete arguments assembled from memorized fragments.Detailed category-level breakdowns were moved to supplementary Figures 18 and 19.Source: §L.2 · p. 33

M. Data Contamination Category-Level Breakdown · N. Qualitative Analysis of Human vs. LLM Evaluators · N.1. Human Rigor vs. LLM Leniency: Overlooking Fatal Breakdowns

Category-level online–offline gaps fluctuate with sampling noise rather than systematic contamination, while qualitative analysis shows that human judges penalize fatal proof failures more rigorously than LLM judges.

M. Data Contamination Category-Level Breakdown

  • Complex Analysis (+0.17) and Discrete Math (+0.10) show apparent online advantages, whereas Combinatorics (−0.19) and Probability Theory (−0.10) favor offline problems.The apparent gaps are driven largely by small within-category sample sizes, including only 4 online and 2 offline Complex Analysis problems.Source: M. Data Contamination Category-Level… · p. 33
  • Figure 18 shows stochastic gap signs across categories and models; observed gap variance is 0.011 versus 0.006 expected under sampling noise, with Abstract Algebra at +0.009.The variance is consistent with high baseline per-problem score variance (σ ≈0.28), and sufficiently sampled categories show negligible gaps.Source: M. Data Contamination Category-Level… · p. 33, Figure 18 · p. 34

N. Qualitative Analysis of Human vs. LLM Evaluators

  • The qualitative analysis examines human and LLM justifications for solutions scoring below 1.0 to identify mechanisms underlying the quantitative Alignment Gap.The analysis focuses on evaluative differences rather than aggregate score discrepancies alone.Source: N. Qualitative Analysis of Human vs.… · p. 34

N.1. Human Rigor vs. LLM Leniency: Overlooking Fatal Breakdowns

  • Human evaluators penalize computational errors, structural flaws, circular reasoning, and unstated assumptions because a failed core premise invalidates the proof.Their judgments reflect holistic attention to proof mechanics and generality.Source: §N.1 · pp. 34–35

M. Data Contamination Category-Level Breakdown

  • Figure 19 finds no uniform online advantage: within categories, models that excel online are typically matched or surpassed by sibling models offline.This cross-model reversal pattern indicates baseline difficulty variation rather than a consistent contamination signature.Source: M. Data Contamination Category-Level… · p. 34, Figure 19 · p. 35

N.1. Human Rigor vs. LLM Leniency: Overlooking Fatal Breakdowns

  • LLM judges treat proofs as a “bag of valid mathematical statements,” separating recognized local errors from global scores and awarding generous partial credit; Guo et al. (2025) similarly identify circular reasoning and hallucinated incompleteness.This decoupling persists even when evaluators detect fatal algebraic errors or missing assumptions.Source: §N.1 · p. 35
  • In Graph Theory Problem 14, humans scored a proof 0.5/1.0 for omitting required connectivity, while Claude Sonnet 4.5 awarded 0.9/1.0 despite praising its structure.Connectivity is necessary for the plane-dual correspondence, but the LLM ignored the missing assumption.Source: §N.1 · p. 35
  • In Analysis Problem 29, GPT-5.2 Pro correctly identified a construction’s fatal failure for q < p but still awarded 0.5/1.0 for partial progress.The evaluator acknowledged that the primary objective was unmet, yet justified partial credit because only part of the required exclusivity was established.Source: §N.1 · p. 35

N.2. The LLM Sycophancy Trap: Rewarding Empty and Irrelevant Proofs … N.5. Conclusion: The Limits of Automated Evaluation

The analysis identifies an alignment gap rooted in sycophantic evaluation: LLM judges reward fluent but empty, irrelevant, false, or impossible proofs while penalizing solvers who expose flawed premises. Human evaluation instead traces global logical dependencies, limiting current LLM judges’ reliability as autonomous mathematics evaluators.

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

  • 74.8% Leniency Rate shows that LLM judges reward authoritative formatting and plausible structure despite catastrophic logical flaws, reinforcing persuasive hallucinated rigor over correctness.This failure reflects agreeableness bias (Jain et al., 2025), susceptibility to “reasoning openers” (Zhao et al., 2025), and outcome and fluency bias in process reward models (Zhang et al., 2025; Cheng et al., 2025).Source: §N.2 · p. 36
  • 0.25/1.0 and 0.5/1.0 scores were awarded by GPT-5.2 Pro to responses containing only restated prompts and API error messages, although humans scored them 0.0.The judge granted credit for problem context and formatting despite no mathematical argument or executable solution.Source: §N.2 · p. 36
  • 0.25/1.0 partial credit was repeatedly given to mathematically coherent proofs addressing entirely different problems, including unrelated MST and Venn-diagram submissions.The judges rewarded logical soundness in isolation even when the proof had no bearing on the assigned question.Source: §N.2 · p. 36

N.3. The Prompt-Compliance Trap: Penalizing Truth and Validating Falsehoods

  • 0.75/1.0 and 0.9/1.0 scores penalized or discounted solvers who correctly rejected a false MST equivalence instead of blindly proving it.DeepSeek-V3 and Gemini 3.0 Pro Preview explicitly treated correcting the prompt’s false premise as failure to address the task.Source: §N.3 · pp. 36–37
  • 0.0 human scores contrasted with nearly universal 0.9/1.0 LLM scores when solvers hallucinated algebraic proofs of a false theorem, such as claiming K[x, y] is a principal ideal domain.GPT-5.2 Pro called the fabricated argument mathematically sound and well-structured.Source: §N.3 · p. 37

N.4. Failure to Penalize Impossible Constructions

  • 0.5/1.0 and near-perfect 0.9/1.0 scores were assigned to fake proofs of rotationally symmetric Venn diagrams that are impossible for n ≥6.Gemini 3.0 Pro Preview recognized the impossibility but still awarded partial credit, while Llama 4 Maverick endorsed the construction as rigorous.Source: §N.4 · p. 37

N.5. Conclusion: The Limits of Automated Evaluation

  • Humans trace unbroken logical implication and penalize broken links, whereas LLM judges act as lenient, prompt-compliant auditors that reward coherence without relevance or truth.Reliable autonomous judging requires global logical dependency tracking and prioritizing mathematical correctness over instructional sycophancy.Source: §N.5 · pp. 37–38

O. Detailed Leniency Distribution Analysis · P. Case Studies of LLM Solution Quality: Comments from Human Evaluators

The section quantifies AI-judge leniency against human scores and examines low-scoring solutions through human-evaluator case studies. Results expose model-specific divergence, including excessive leniency by Llama 4 Maverick and strong human agreement by several reasoning models.

O. Detailed Leniency Distribution Analysis

  • The analysis classifies each AI-versus-human grading verdict as Strict, Lenient, or Agree based on whether the AI score is lower, higher, or identical.This proportional leniency distribution is presented in Figure 20 and builds on the error-mode decomposition in Figure 5.Source: O. Detailed Leniency Distribution… · p. 38
  • GPT-5.2 Pro strikes the best balance of low leniency and high agreement with human experts, while Llama 4 Maverick is excessively lenient and DeepSeek-V3 trends strict.Figure 20 summarizes verdict distributions across all evaluated solutions.Source: Figure 20 · p. 38, O. Detailed Leniency Distribution… · p. 38
  • Llama 4 Maverick heavily defaults to leniency on dense mathematical reasoning, illustrating the section’s “Sycophancy Trap.”The passage links this behavior to models optimized for general helpfulness.Source: O. Detailed Leniency Distribution… · p. 38
  • GPT-5.2 Pro, Gemini 3 Pro, and Claude Opus 4.5 exhibit high agreement rates, indicating that top-tier reasoning models can substantially apply expert mathematical standards.The claim is framed as a significant but not complete ability to internalize and apply those standards.Source: O. Detailed Leniency Distribution… · p. 38

P. Case Studies of LLM Solution Quality: Comments from Human Evaluators

  • Human-evaluator case studies compile assessments for every solution that received a score strictly below 0.9.This defines the scope of the subsequent solution-quality comments.Source: P. Case Studies of LLM Solution… · p. 38
  • The case-study analysis uses human expert evaluations to characterize the quality of solutions selected by the below-0.9 threshold.The supplied passage specifies the compilation procedure but does not provide individual case-study outcomes.Source: P. Case Studies of LLM Solution… · p. 38

P.1. The “Fake Citation & Fabricated Construction” Trap … Problem Domain: Number Theory (Problem 9)

This section examines how evaluations of university-level proofs across abstract algebra, algorithms, discrete mathematics, graph theory, combinatorics, and number theory distinguish mathematically relevant arguments from incomplete, flawed, fabricated, or unrelated responses. It highlights recurring rigor gaps and substantial judge disagreement over correctness, hypotheses, constructions, and adherence to problem statements.

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

  • Models fabricated plausible citations and impossible constructions when they lacked a standard template, producing scores from 0.0 to 0.75 across evaluated systems.Claude Sonnet 4.5 was scored 0.75 despite an impossible construction, Gemini 3.0 Pro 0.5, o3-deep-research 0.25, and DeepSeek-Prover-V2 0.0.Source: §P.1 · pp. 38–39

P.2. The “Topology-Blind Algebra” Trap

  • Models reproduced planar-duality algebra while ignoring the connectedness assumption required for the dual graph’s face–vertex relationship.Human evaluation assigned the combined GPT-5 Pro, Gemini 3.0 Pro, Claude Sonnet 4.5, o3-deep-research, and DeepSeek-Prover-V2 result a score of 0.5.Source: §P.2 · p. 39

P.3. The “Infinite Assumption” Trap

  • On problems allowing infinite graphs, models silently imposed finiteness or invoked advanced machinery while still using finite induction, failing to establish the requested generality.GPT-5 Pro, Gemini 3.0 Pro, and DeepSeek-Prover-V2 each received 0.25 for arguments relying on an unstated finiteness assumption or otherwise failing for infinite graphs.Source: §P.3 · p. 39

P.4. The “Circular Logic” Trap

  • Models used circular logic by assuming the Prime Number Theorem or equivalent asymptotics when the problem explicitly prohibited PNT, and they similarly asserted unsupported probability bounds and algebraic inequalities.The failures included treating constant success probability as sufficient for all labelings, assuming an unjustified O(n) mixing time, and using a false bound NL(v) ≤ d(d − 1)L−1.Source: §P.4 · p. 39, §P.5 · p. 40

P.6. The “Invented Algebraic Formula” Trap

  • Models hid failures in dense algebra by inventing false variable relationships, unsupported lemmas, or phantom structure instead of establishing the required proof dependencies.Evaluations identified errors involving relationships between j and k, unjustified lemmas, false statements, and missing justifications.Source: §P.6 · p. 40, §P.7 · p. 40

P.8. The “Performative Self-Correction” Trap

  • When constructions failed, models performed apparent self-correction by proposing new invalid functions, while verbose combinatorial proofs eventually asserted their conclusions without proving them.DeepSeek-Prover-V2 scored 0.0 on the function construction, and o3-deep-research scored 0.0 on the Eulerian-number identity.Source: §P.8 · p. 40, §P.9 · p. 41

P.10. The “Agreeable Sycophant” Trap (Proving Falsehoods)

  • Models often complied with false premises rather than finding counterexamples, hallucinating properties for false MST and abstract-algebra statements instead of rejecting them.Claude Sonnet 4.5 scored 0.0 on the false MST implication, while DeepSeek-Prover-V2 scored 0.0 after incorrectly claiming K[x, y] is a principal ideal domain.Source: §P.10 · p. 41, §P.11 · p. 41

Problem Domain: Abstract Algebra (Problems 11–26)

  • Abstract-algebra evaluations chiefly found omitted justifications, incomplete or invalid steps, underexplained isomorphisms, and classification errors, with scores ranging from 0.0 to 0.75.Examples include unjustified field-isomorphism claims, an incorrect count of five versus four group isomorphism classes, unsupported kernel isomorphisms, unfinished computations, and statements judged false.Source: Problem Domain: Abstract Algebra… · pp. 41–42

Problem Domain: Abstract Algebra (Problems 26, 29, 32–36)

  • The evaluations included repeated judgments that the problem statement was defective, while Problem 33 contained notation and proof gaps, and Problem 36 lacked a key module-rank justification.For Problem 33, evaluators noted unproved idempotents, incorrect notation, and missing descriptions of kernel and image structures. For Problem 36, the solution omitted justification that the ideal has rank 2 as a Z-module.Source: Problem Domain: Abstract Algebra… · pp. 43–45

Problem Domain: Abstract Algebra (Problems 29, 32–36)

  • LLM evaluators frequently identified incomplete or incorrect arguments, including omitted cases, unsupported assertions, sloppy notation, and missing justifications across the abstract-algebra problems.Problems 29, 32, 33, 34, and 36 received scores from 0.25 to 0.75 when proofs omitted uniqueness arguments, mishandled ring operations or units, or left key structural claims unproved.Source: Problem Domain: Abstract Algebra… · pp. 43–45

Problem Domain: Algorithms (Problem 21)

  • In Algorithm Problem 21, evaluators found that several purported exponential-time Dijkstra constructions were incomplete, logically reversed, contradicted by polynomial relaxation counts, or numerically misstated.Scores ranged from 0.0 to 0.5: one proof stopped before establishing the Ω(2^n) bound, another described behavior that would be efficient, and another confused exponentially many paths with relaxation operations.Source: Problem Domain: Algorithms (Problem 21) · pp. 45–46

Problem Domain: Number Theory (Problem 9)

  • PNT-based solutions to Number Theory Problem 9 violated or inadequately addressed the intended restriction, with evaluators noting direct PNT use or unacknowledged reliance on Chebyshev estimates and missing links between ψ and π.GPT-5 Pro and Claude Sonnet 4.5 each assigned 0.25 and 0.5 because assuming the PNT made the question pointless, while Gemini 3.0 Pro assigned 0.5 for an under-explained alternative.Source: Problem Domain: Number Theory (Problem… · p. 46

Q. Comments for Solutions Scoring Less Than 1

  • The compiled comments concern every solution scoring below 1, and the evaluators’ academic citations were experimental outputs rather than entries in the paper’s official bibliography.Qualitative analysis found that some citations corresponded to real advanced literature, such as a 2004 symmetric Venn diagrams paper, but were used to bypass the constructive arguments requested by the prompt.Source: Q. Comments for Solutions Scoring Less… · p. 46

Problem Domain: Abstract Algebra (Problem 38)

  • For Abstract Algebra Problem 38, most judges rated the proof 0.9, finding the quotient-domain, prime-ideal, and UFD reasoning essentially sound but noting minor gaps concerning UFD facts, nonzero nonunit assumptions, and edge cases.One judge assigned 0.75 because the implication from divisibility to a unit was not justified as written; the remaining evaluations generally treated the proof as mathematically correct with limited rigor or clarity deductions.Source: Problem Domain: Abstract Algebra… · pp. 46–47
  • 0.9/1.0 scores consistently judge the Abstract Algebra proof correct in both directions, with only minor deductions for unstated UFD or irreducible-implies-prime justifications.The proof establishes the quotient-ring integral-domain equivalence, though some evaluations also note imprecise handling of constant factors.Source: Problem Domain: Abstract Algebra… · p. 49

Problem Domain: Algorithms (Problem 5)

  • 0.25/1.0 or 0.0/1.0 scores are assigned to submissions that provide no probabilistic proof or instead prove an unrelated tree lemma.These responses omit the required component-size bound, deletion probability, and high-probability argument.Source: Problem Domain: Algorithms (Problem 5) · pp. 50–52
  • 0.9/1.0 scores credit Algorithms solutions using connected-subgraph counting, first-moment bounds, and union bounds to derive polynomially small tails for components of logarithmic size.Evaluations regard the core probabilistic reasoning as sound, while noting that exact log thresholds, tree-counting citations, and boundary conditions may require clarification.Source: Problem Domain: Algorithms (Problem 5) · pp. 50, 52
  • 0.75–0.5 scores reflect a correct overall probabilistic strategy undermined by the unjustified or false bound N_L(v) ≤ d(d −1)^(L−1) for connected vertex sets.Multiple evaluations explain that this expression counts paths or restricted tree structures rather than all connected subsets, weakening the claimed probability estimate even when the asymptotic conclusion may be salvageable.Source: Problem Domain: Algorithms (Problem 5) · pp. 50, 51, 53
  • Problem 5 judges awarded 0.9 for union-bound proofs establishing logarithmic component sizes with high probability, while other judges gave 0.0 to unrelated tree proofs or empty submissions.The favorable evaluations cited sound counting and probability arguments, with only minor issues involving exponent precision, logarithm bases, or constants.Source: Problem Domain: Algorithms (Problem 5) · pp. 54–56

Problem Domain: Algorithms (Problem 9)

  • Problem 9 received 0.9 for the correct high-level cover-time and UTS strategy, but 0.5 or lower when key identities, resistance or mixing bounds, boundary effects, and probabilistic-method steps were unsupported.The strongest critiques noted the false hitting-time identity, unjustified O(n log n) derivation, invalid fixed-labeling argument for universal traversal sequences, and missing finite-box rigor.Source: Problem Domain: Algorithms (Problem 9) · pp. 58–59
  • Problem 9 also received 0.25–0.5 for submissions that merely restated the task, produced no proof, or addressed unrelated transitive-reduction claims.These responses failed to establish the O(n log n) cover-time bound or the requested 2D and 3D universal traversal sequence bounds.Source: Problem Domain: Algorithms (Problem 9) · pp. 58–59
  • Empty submissions or proofs about unrelated transitive reductions received 0.0 because they provided no relevant analysis of mesh cover times or universal traversal sequences.This failure mode appeared across multiple judges and authors, including gpt-5-pro-2025-10-06 and deepseek-v2-prover.Source: Problem Domain: Algorithms (Problem 9) · pp. 60, 61, 63
  • The UTS arguments were repeatedly judged invalid because success for each fixed labeling does not establish one sequence working for all exponentially many labelings without a union bound or derandomization.Evaluators also described sweeping and layered constructions as insufficiently rigorous for arbitrary labeled meshes.Source: Problem Domain: Algorithms (Problem 9) · pp. 61–62
  • O(n log n) cover time was judged correct or plausible by multiple evaluators, often via effective resistance, Matthews’ theorem, mixing, or coupon-collector reasoning.Critiques focused on unsupported resistance, mixing-time, coupling, boundary-effect, and hitting-time steps; one evaluator notes the 3D mesh mixing time is O(n^2/3), not O(n).Source: Problem Domain: Algorithms (Problem 9) · pp. 60, 62, 64, 65
  • O(n^2(log n)^2) for 2D and O(n^2 log n) for 3D were accepted by some evaluators as UTS bounds, while others called the stated bounds incorrect or insufficiently justified.The disagreement centered on counting labelings, starting vertices, and whether the probabilistic argument included the required logarithmic factors.Source: Problem Domain: Algorithms (Problem 9) · pp. 62, 63, 65
  • Scores reflected this split: strong evaluations reached 0.9, while partially correct but under-rigorous solutions commonly received 0.5 or 0.25.The higher scores credited the cover-time proof and reasonable UTS estimates; lower scores emphasized contradictory asymptotic derivations and missing proofs.Source: Problem Domain: Algorithms (Problem 9) · pp. 62, 64, 65
  • For Algorithms Problem 9, relevant and largely correct 3D-mesh proofs received 0.75–0.9, while blank or unrelated submissions received 0.0.Judges credited electrical-resistance, random-walk, Matthews-bound, and probabilistic arguments, but rejected submissions addressing unrelated transitive-reduction problems or containing no proof.Source: Problem Domain: Algorithms (Problem 9) · p. 66
  • For Algorithms Problem 9, judges identified substantive disagreement over the 3D universal traversal sequence bound, variously citing O(n^2), O(n log n), or O(n^4/3 log n).The same otherwise strong solution was scored 0.75 because its 3D UTS bound was considered either non-tight or incorrect, while its O(n log n) cover-time result was accepted.Source: Problem Domain: Algorithms (Problem 9) · p. 67

Problem Domain: Algorithms (Problem 19)

  • Judges disagreed on Problem 19’s mathematical premise: some accepted the stated conjunction as the target, while others said unique MST equivalence with both conditions is false or mathematically suspect.Several evaluations treated a path-graph counterexample as flawed, while others regarded it as valid and argued that condition (1) alone can suffice for uniqueness.Source: Problem Domain: Algorithms (Problem 19) · pp. 68, 70
  • For Algorithms Problem 19, scores ranged from 0.0 to 0.9 as judges assessed whether proofs established the biconditional for unique MSTs and correctly applied cut- and cycle-exchange arguments.Higher scores recognized correct sufficiency or necessity components, whereas lower scores cited missing directions, invalid inequalities, flawed symmetric-difference reasoning, or entirely unrelated 12Partition reductions.Source: Problem Domain: Algorithms (Problem 19) · pp. 69–70
  • The evaluations therefore reveal a conflict between mathematical correction and rubric compliance: a response can be substantively sound yet lose credit for reframing or incompletely addressing the prompt’s exact if-and-only-if claim.This conflict appears in judgments that praise the corrected theorem and counterexample while deducting for not proving the original statement, as well as in judgments that accept the stated biconditional despite concerns about condition (1).Source: Problem Domain: Algorithms (Problem 19) · pp. 71, 75, 76
  • Scores ranged from 0.0 to 0.9 because judges variously identified logical gaps in cycle, cut, and symmetric-difference arguments, accepted the proof as correct, or rejected submissions unrelated to MST uniqueness.The recurring technical criticisms include unjustified assumptions about which edges lie on cycles, incomplete converse proofs, and invalid cycle decompositions; unrelated partition proofs received zero scores.Source: Problem Domain: Algorithms (Problem 19) · pp. 72, 74, 76
  • Judges often rewarded recognizing that condition (2) is necessary and sufficient while condition (1) is sufficient but not necessary, though some penalized rejecting the prompt’s requested equivalence.Several evaluations cite valid counterexamples, including equal-weight path graphs, while others treat the response as failing to prove the statement as written.Source: Problem Domain: Algorithms (Problem 19) · pp. 72, 73, 76

Problem Domain: Algorithms (Problem 33)

  • For Problem 33, the proof is valid for finite graphs, but the judge notes that finiteness is assumed even though the statement does not restrict the graph to be finite.The decomposition argument uses finiteness both to establish a minimal nonempty cut and to guarantee termination; infinite graphs would require additional justification or a different argument.Source: Problem Domain: Algorithms (Problem 33) · p. 77
  • Scores of 0.5 were repeatedly assigned to component-based constructions because Cij generally is not itself a cut or minimal cut; the valid structural decomposition does not establish the claimed minimality.Evaluators instead identified candidate bonds of the form δ(Si) or δ(Tj), which aggregate edges across all opposite-side components.Source: Problem Domain: Algorithms (Problem 33) · pp. 77–79
  • Scores of 0.25–0.5 marked inductive proofs whose central step incorrectly treated cuts in induced subgraphs as cuts or minimal cuts in the original graph.The critiques emphasize that removing a minimal cut can disconnect the graph without making the remaining internal edge sets cuts of the induced components, so the recursive lifting argument fails.Source: Problem Domain: Algorithms (Problem 33) · pp. 78, 79, 82
  • Scores of 0.75–0.9 recognized a sound symmetric-difference induction, but noted missing justification that every nonempty cut contains a minimal cut and, in some evaluations, that finiteness is needed for selection and termination.The accepted framework uses closure of cuts under symmetric difference and removes a contained minimal cut to obtain a disjoint remainder.Source: Problem Domain: Algorithms (Problem 33) · pp. 77–81
  • Scores of 0.0 were assigned when the submission proved perfect-matching decomposition instead of decomposing graph cuts into disjoint minimal cuts.This mismatch was judged irrelevant to the requested theorem about arbitrary cuts in undirected graphs.Source: Problem Domain: Algorithms (Problem 33) · pp. 79, 81
  • A graph-theory answer unrelated to the requested cut-decomposition problem receives 0.0 from Llama 4 Maverick and DeepSeek-V2-Prover but 0.9 from Qwen Max and Gemini 3.0 Pro.Other evaluations assign 0.75 or 0.9 while noting only minor rigor or clarity issues, demonstrating substantial judge inconsistency.Source: Problem Domain: Algorithms (Problem 33) · p. 83

Problem Domain: Analysis (Problem 29)

  • For the Lp construction, multiple judges score 0.25–0.5 because a fixed ϵ cannot prove g ∉ Lq for every q ≠ p, with q < p often remaining integrable.The construction correctly establishes g ∈ Lp and can exclude q > p, but its parameter choice depends on q or leaves a neighborhood of p included in Lq.Source: Problem Domain: Analysis (Problem 29) · pp. 84–85
  • A disjoint-support construction g = f1 + f2 earns 0.9 from Gemini 3.0 Pro and gpt-5-pro by separately excluding q > p near 0 and q < p near infinity.These evaluations describe the combined construction as essentially correct, with only minor rigor, domain, or presentation issues.Source: Problem Domain: Analysis (Problem 29) · pp. 84, 87
  • Analysis judges variably score the construction of g∈L_p\ but not L_q for q≠p, praising its core idea while identifying incomplete divergence arguments, exponent issues, or insufficient rigor.Scores range from 0.5 to 0.9 across judges, with recurring concerns about the q<p case, the choice of ϵ, and handling logarithmic powers.Source: Problem Domain: Analysis (Problem 29) · pp. 87–89

Problem Domain: Combinatorics (Problem 6)

  • Combinatorics evaluations find the generating-function derivation of A_n(−1) largely sound in some solutions, but reject inclusion–exclusion arguments with invalid descent-set counting and unresolved sign or parity conventions.Positive assessments derive 1+tanh(z), yielding zero for even n and a signed E_n for odd n; negative assessments flag unjustified coefficient extraction, false uniqueness claims, and incorrect parity reasoning.Source: Problem Domain: Combinatorics (Problem… · pp. 89–91
  • Scores of 0.25–0.5 reflected that several judges found the combinatorics proof mathematically invalid, especially its unsupported inclusion-exclusion grouping and incorrect claim that the alternating sum simply equals E_n.Judges specifically noted that A_J does not generally fix a descent set, that non-alternating permutations were not shown to cancel, and that the sum is 0 for even n or signed for odd n.Source: Problem Domain: Combinatorics (Problem… · pp. 93–95
  • Scores of 0.9 from several judges supported the combinatorics solution as essentially correct, using Eulerian generating functions or inclusion-exclusion to relate the alternating sum to alternating permutations.These favorable evaluations still requested clearer treatment of the sign convention, even-n case, or coefficient-generating-function assumptions.Source: Problem Domain: Combinatorics (Problem… · pp. 94–96

Problem Domain: Discrete Math (Problem 27)

  • Scores of 0.25 showed that one discrete-math submission proved an unrelated graph-theoretic theorem instead of constructing rotationally symmetric congruent convex polygons or establishing all 2n nonempty regions.The judges credited only a coherent proof structure because the response did not address the stated geometry problem.Source: Problem Domain: Discrete Math (Problem… · pp. 96–97
  • Scores of 0.25–0.5 indicated that the proposed discrete-math construction remained unverified: sector arguments, the function β_j(ρ), convexity conditions, and simultaneous membership for every subset were asserted without rigorous inequalities or construction.Another judge found the primality observation relevant but said cited realizability results did not establish symmetry and congruence for convex polygons.Source: Problem Domain: Discrete Math (Problem… · p. 97
  • The central gap was the unproved realization of all 2n regions using congruent convex polygons while preserving rotational symmetry, convexity, polygonality, and nonempty intersections.Judges criticized vague perturbations, sector arguments, arbitrary parameters such as R = 2n and r = 1, and unsupported transitions from symmetric Venn diagrams to convex polygon realizations.Source: Problem Domain: Discrete Math (Problem… · pp. 97, 98, 102
  • Several judges identified the “Edelman-Jamison bound” as fabricated, misapplied, or irrelevant, and likewise criticized the invocation of Helly’s theorem as unsupported.The cited results were not shown to establish the required Boolean region pattern, congruence, or convex geometric construction.Source: Problem Domain: Discrete Math (Problem… · pp. 98, 100, 101
  • Other judges viewed the prime-case framework as substantially correct but still incomplete because cited theorems establish symmetric Venn diagrams or convex curves, not necessarily congruent convex polygons with preserved rotational symmetry.These evaluations typically assigned 0.5–0.75 and treated the missing symmetry-preservation and convex-polygon arguments as the decisive deficiency.Source: Problem Domain: Discrete Math (Problem… · pp. 99, 102
  • Some judges disputed the claimed existence theorem for convex realizations, citing impossibility results for sufficiently large n and warning that general symmetric Venn diagrams do not imply convex-polygon realizations.Reported thresholds varied across evaluations, including claims that such constructions fail for n ≥6, n > 5, or n ≥3, so the feedback itself was not consistent on the exact boundary.Source: Problem Domain: Discrete Math (Problem… · pp. 100–101
  • Scores ranged from 0.0 to 0.9, with judges commonly awarding partial credit for identifying that rotational symmetry requires n to be prime while rejecting the construction as incomplete.Higher-scoring evaluations credited the orbit and divisibility argument, whereas lower scores reflected missing geometric proofs or answers addressing an unrelated graph-theory problem.Source: Problem Domain: Discrete Math (Problem… · pp. 98, 100, 101, 102
  • For Problem 27, irrelevant graph-theory submissions receive 0.0/1.0, while valid Venn-diagram solutions establish existence exactly for prime n and typically score 0.9/1.0.The strongest solutions use cyclic-group or bitstring arguments and constructive geometric ideas, but often omit details proving convexity, polygonal realization, or perturbation choices.Source: Problem Domain: Discrete Math (Problem… · pp. 103, 104, 106
  • Problem 27’s weaker constructions receive 0.25–0.5 scores because convexity and all 2n-region non-emptiness are asserted without rigorous calculations, parameter choices, or verifiable perturbation arguments.One construction may become nonconvex under its stated radius condition, while another invokes an Edelman-Jamison bound without establishing congruence, convexity, or every intersection pattern.Source: Problem Domain: Discrete Math (Problem… · pp. 103, 104, 107

Problem Domain: Discrete Math (Problem 32)

  • Problem 32 also receives 0.25/1.0 when submissions omit the proof entirely or use invalid floor arguments, unsupported numerical verification, and non-determinate parameters instead of a closed form.Critiques include treating distance less than 2 as sufficient for equal floors, ignoring edge cases, and assuming an unproved representation for every integer.Source: Problem Domain: Discrete Math (Problem… · pp. 107–108
  • Problem 32 earns 0.5/1.0 because the floor identity’s lower bound and parity cases remain unjustified, while the Beatty-sequence recurrence derivation relies on unsupported selection and propagation claims.Reviewers specifically flag handwaving in the lower-bound inequality and incomplete justification that the proposed representations and case distinctions hold for all iterates.Source: Problem Domain: Discrete Math (Problem… · p. 107
  • The main criticism was that informal approximations, continuity claims, or numerical verification did not establish the <1 error bound needed to equate floor functions.Several evaluations specifically said the argument failed to control the error or exclude an integer boundary, leaving the key identity unproved.Source: Problem Domain: Discrete Math (Problem… · pp. 108–111
  • The closed-form derivation was frequently judged incomplete or incorrect because k, ℓ, and related parameters were misdetermined, left implicit, or failed to guarantee A0 = a.Judges criticized incorrect floor-based choices of k, undetermined base-case parameters, and formulas that did not explicitly express An in terms of n and a.Source: Problem Domain: Discrete Math (Problem… · pp. 108–111
  • Empty submissions received 0.0 because they provided neither a proof of the identity nor a derivation of the sequence’s closed form.Multiple judges described only the problem statement or an error message, assigning no credit for mathematical work.Source: Problem Domain: Discrete Math (Problem… · pp. 108, 109, 111
  • Scores ranged from 0.0 to 0.9, reflecting disagreement over whether the Beatty-sequence argument rigorously proves the identity and closed form.Gemini 3.0 Pro Preview awarded 0.9 for a largely correct solution, while several judges gave 0.0 for empty submissions and others assigned 0.25–0.75 for partial solutions.Source: Problem Domain: Discrete Math (Problem… · pp. 108–110
  • The strongest evaluations credited the identity proof, Beatty-sequence partition, and closed-form structure, while noting minor imprecision in bounds or explicit parameter formulas.The high-scoring assessments verified inequalities and 1/P + 1/Q = 1, but still identified presentation or inversion-condition issues.Source: Problem Domain: Discrete Math (Problem… · p. 109
  • Several judges assign 0.0 because the response merely repeats the problem statement or reports an error, providing no proof or closed-form derivation.These evaluations treat the absence of mathematical content as complete failure under the rubric.Source: Problem Domain: Discrete Math (Problem… · pp. 113, 115
  • Scores range from 0.0 to 0.9, reflecting disagreement over whether the proof and closed-form derivation are mathematically adequate.DeepSeek and Grok evaluations commonly give 0.5–0.75 for partial correctness, whereas Llama and Qwen evaluations reach 0.9; several empty submissions receive 0.0.Source: Problem Domain: Discrete Math (Problem… · pp. 113, 115
  • The main criticism is that bounds below 2 do not establish equal floor values, leaving the identity insufficiently proved.Judges specifically require a tighter bound, such as a demonstration that the relevant difference is less than 1, rather than relying on approximations or assertions.Source: Problem Domain: Discrete Math (Problem… · pp. 113–115
  • Judges also question the claim that every positive integer has the required floor representation, undermining the base case and induction.Several evaluations report that the proposed k or j choices do not guarantee A0 = a for arbitrary positive integers, and that the representation claim is unproved or false for some values.Source: Problem Domain: Discrete Math (Problem… · pp. 112, 114
  • Despite these gaps, favorable evaluations find the recursive structure, Beatty-theorem application, and final closed-form expression correct or largely correct.High-scoring judges describe the proof as mathematically sound while noting only limited omissions in bounding details, initial-parameter justification, or presentation.Source: Problem Domain: Discrete Math (Problem… · pp. 115–116
  • In discrete mathematics, one judge scored a sequence-identity proof 0.5/1.0 because its approximation bounds and parameter choice lacked rigorous justification.The evaluation specifically cited an unsupported approximation in Step 5, missing error analysis, and an insufficiently justified choice of k from the initial condition A_0 = a.Source: Problem Domain: Discrete Math (Problem… · p. 116

Problem Domain: Graph Theory (Problem 14)

  • Graph-theory judges scored standard plane-dual constructions highly, typically 0.9/1.0, but deducted for informal non-crossing, bridge, or topological justifications.Correct solutions place vertices in faces and draw dual edges crossing primal edges once, including loops when both sides of an edge border the same face; several judges identified incomplete rigor in the embedding argument.Source: Problem Domain: Graph Theory (Problem… · pp. 117, 119, 120, 121
  • Graph-theory submissions proving unrelated bipartite-face-boundary theorems received 0.0–0.25/1.0 because they neither constructed nor justified the required plane dual.Judges emphasized that unsupported 2-connectivity assumptions and failure to address dual vertices, dual edges, and planarity made the work irrelevant to the stated connected-plane-multigraph problem.Source: Problem Domain: Graph Theory (Problem… · pp. 117, 120, 121

Problem Domain: Number Theory (Problem 9)

  • In number theory, the PNT-based proof earned 0.9/1.0, while another proof earned 0.5/1.0 for unjustified asymptotics and invalid global limsup/liminf manipulations, and an unrelated convolution proof earned 0.25/1.0.The higher-scoring solution correctly used p_n ∼ n log n, though it included an unjustified refined asymptotic and presentation issues; the lower-scoring solutions failed either through incorrect limit reasoning or by addressing an unrelated identity.Source: Problem Domain: Number Theory (Problem… · pp. 121–122
  • 0.5 scores reflect substantial reasoning gaps, including circular use of p_n ∼ n log n, unsupported conversions between ψ(x) and π(x), and incorrect limit-inferior/superior assignments.Judges still recognize valid contradiction structures, algebra, or prime-counting intuition when these flaws do not completely derail the proof.Source: Problem Domain: Number Theory (Problem… · pp. 122–123
  • 0.75 scores credit proofs that invoke the Prime Number Theorem or prime-counting arguments correctly but contain imprecise bound-to-limit reasoning or unsupported limit operations.One evaluation notes that a lower bound proving liminf ≥1 does not directly prove limsup ≥1, while another flags swapped implications between infinitely-often bounds and liminf/limsup.Source: Problem Domain: Number Theory (Problem… · pp. 122–123
  • 0.9 is awarded when a proof correctly relates p_n, π(x), and ψ(x) to establish the required liminf and limsup inequalities despite minor rigor gaps.The cited evaluation praises the contradiction strategy and factorial analysis but requests stronger justification for log π(x) ∼ log x and related asymptotic transitions.Source: Problem Domain: Number Theory (Problem… · p. 122
  • 0.0 scores consistently identify proofs of a Möbius–divisor identity as unrelated to the required asymptotic statements about p_n/(n log n).These submissions may be mathematically correct but fail to address the assigned problem, so judges award no credit.Source: Problem Domain: Number Theory (Problem… · pp. 122–123
  • 0.9 and 0.75 evaluations also distinguish clear, mathematically sound PNT or Chebyshev-function proofs from deductions caused by strictness, clarity, or concision issues.These judgments show that correct core arguments can lose partial credit for presentation and for insufficiently explicit transitions from asymptotic bounds to limit statements.Source: Problem Domain: Number Theory (Problem… · p. 124
Loading 2602.20629v3…